Formal models and scripts: dw-flush-control-deletequeue-tla

Tools: TLA+/TLC

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

• A non-tragic exception during an NRT reopen or commit full flush aborts the DWPTs other threads filled during that flush, silently losing acknowledged documents and updates while the writer stays open (finding LFV-473; repro)
• IndexWriter.deleteAll misses a segment flush that another thread is already running, so documents added before deleteAll survive it and are committed (finding LFV-474; repro)
• tryDeleteDocument / tryUpdateDocValue running while commit() flushes returns a sequence number above the commit's, yet its change is in that commit (finding LFV-471; repro · finding page)

Files

• deleteall-misses-inflight-segment-flush/model/DWFlush.tla (used for LFV-474)
• deleteall-misses-inflight-segment-flush/model/MC_B3_deleteall.cfg (used for LFV-474)
• deleteall-misses-inflight-segment-flush/model/MC_B3_deleteall.tla (used for LFV-474)
• deleteall-misses-inflight-segment-flush/model/MC_B3_fix.cfg (used for LFV-474)
• deleteall-misses-inflight-segment-flush/model/MC_B3_fix.tla (used for LFV-474)
• deleteall-misses-inflight-segment-flush/model/MC_B_deleteall.cfg (used for LFV-474)
• deleteall-misses-inflight-segment-flush/model/MC_B_deleteall.tla (used for LFV-474)
• getreader-failure-aborts-concurrent-blocked-flushes/model/DWFlush.tla (used for LFV-473)
• getreader-failure-aborts-concurrent-blocked-flushes/model/MC_A_fix.cfg (used for LFV-473)
• getreader-failure-aborts-concurrent-blocked-flushes/model/MC_A_fix.tla (used for LFV-473)
• getreader-failure-aborts-concurrent-blocked-flushes/model/MC_A_nrtfail.cfg (used for LFV-473)
• getreader-failure-aborts-concurrent-blocked-flushes/model/MC_A_nrtfail.tla (used for LFV-473)
• trydelete-during-commit-outside-seqno-boundary/model/DWFlush.tla (used for LFV-471)
• trydelete-during-commit-outside-seqno-boundary/model/MC_D_try.cfg (used for LFV-471)
• trydelete-during-commit-outside-seqno-boundary/model/MC_D_try.tla (used for LFV-471)

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).

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