Formal models and scripts: query-cache-correctness
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
- LatLonShape/XYShape newSlowDocValuesBoxQuery reports Weight#isCacheable() == true although it reads the shape from binary doc values, so after an in-place doc-values update the query cache keeps returning the old matches (finding LFV-308; repro · finding page)
- LongRange/DoubleRange#getQuery(fastMatchQuery, valueSource) reports its Weight as cacheable without asking the fast-match query, so after an in-place doc-values update the query cache keeps returning the old matches (finding LFV-320; repro · finding page)
- LateInteractionFloatValuesSource#isCacheable always returns true although it reads the multi-vectors from binary doc values, so after an in-place update of a LateInteractionField the query cache keeps returning the old matches of a FunctionMatchQuery or DoubleRange query over it (finding LFV-336; repro · finding page)
Files
facet-range-query-ignores-fastmatch-cacheability/model/MC_QueryCacheDV.tla(used for LFV-320)facet-range-query-ignores-fastmatch-cacheability/model/MC_partial.cfg(used for LFV-320)facet-range-query-ignores-fastmatch-cacheability/model/QueryCacheDV.tla(used for LFV-320)late-interaction-values-source-cacheable-after-dv-update/model/MC_QueryCacheDV.tla(used for LFV-336)late-interaction-values-source-cacheable-after-dv-update/model/MC_const.cfg(used for LFV-336)late-interaction-values-source-cacheable-after-dv-update/model/QueryCacheDV.tla(used for LFV-336)shape-docvalues-query-cacheable-after-dv-update/model/MC_QueryCacheDV.tla(used for LFV-308)shape-docvalues-query-cacheable-after-dv-update/model/MC_const.cfg(used for LFV-308)shape-docvalues-query-cacheable-after-dv-update/model/QueryCacheDV.tla(used for LFV-308)
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.