Formal models and scripts: study-search-concurrency-model

Tools: TLA+/TLC, Python

These are the working models and scripts this part of the hunt used. Some encode the code as it is (a counterexample is the expected result), others a fixed or correct variant; read the header comment of each file. Paths inside them were replaced by placeholders such as $LUCENE (a Lucene checkout) and $WORK.

Findings

• IndexSearcher#count hangs forever when Weight#count throws, for example on a query timeout, on a segment split into intra-segment partitions (finding LFV-045; repro · finding page)
• Reusing a TotalHitCountCollectorManager after a failed search silently returns count 0 or hangs (finding LFV-053; repro · finding page)
• LRUQueryCache's 16 hard partitions give a 0% hit rate with the class-javadoc configuration (main only) (finding LFV-054; repro · finding page)
• A timed-out search reports its partial hit count as TotalHits.Relation.EQUAL_TO (finding LFV-077; repro)
• TaskExecutor#invokeAll returns while a task is still running if the caller is interrupted (finding LFV-056; repro · finding page)

Files

• models/CountBarrier.tla
• models/LRUCache.tla
• models/LRUCacheM1.tla
• models/MC_CountBarrier.tla
• models/MC_LRUCache.tla
• models/MC_LRUCacheM1.tla
• models/MC_TaskExec.tla
• models/MC_TopKAcc.tla
• models/MC_TopKAccM1.tla
• models/MC_TopKAccM2.tla
• models/MC_TopKAccM3.tla
• models/TaskExec.tla
• models/TopKAcc.tla
• models/TopKAccM1.tla
• models/TopKAccM2.tla
• upstream/grep.py

How to run

• TLA+ with TLC: java -cp tla2tools.jar tlc2.TLC -config <Model>.cfg <Model>.tla (a counterexample trace is the finding when the model encodes the current code).
• Python: python3 <file>.py; scripts that import z3 need the z3-solver package.

Snapshot of 2026-11-04. AI-assisted; not yet triaged by a human Lucene committer. Feedback: open an issue in lucene-ai-bug-hunt.