TLA+: liveness with threads that call forever (A13 follow-up); fix F280 (signal max 1 permit) - #228

Summary

Follow-up to roadmap A13: the liveness with threads that call forever. The A13 liveness needed finite programs, and the guess in TODO was that a thread calling forever would need fair locks. That was wrong in both directions:

• A finite stream with a closer: every call of every thread returns although threads call forever, with fair scheduling only (weak fairness per thread, writer and closer) and no lock fairness.
  • TLC, bounded models of the abstraction and of the detailed model.
  • TLAPS, for the abstraction and any number of threads, writers and closers, under a fairness by role (see "Limits").
• An endless writer and no close: TLC finds a reader that starves even with every thread step strongly fair. It gets bufferLock every round and finds the bytes taken by the other reader, so a fair lock would not help. The contract promises no fairness between readers (F278).
• The detailed model needs weak fairness only: Fairness in StreamBuffer.tla is weak for the readers now (was strong); every model of the current code checks with it.

No change to production code.

How

• Calls forever without changing the models.
  • StreamBufferWaitForever.tla extends StreamBufferWait.tla with a ghost Refill of the call budget. Every run with threads calling forever is a run of it; the extra runs, where threads stop, only add behaviours. The existing safety, refinement and liveness proofs stay as they are.
  • StreamBufferForever.tla does the same for the detailed model: a thread that is done calls again.
  • A ghost Shift lowers w and t together, so an endless writer fits a finite state space.
• The proof (StreamBufferWaitForeverLiveProof.tla, 1,322 obligations; StreamBufferWaitForeverEnabled.tla, 633). It uses a measure per thread r, a natural number:
  • Every step but a return of r keeps the measure or lowers it, and a step that keeps it moves neither r nor a lock holder nor a writer or closer.
  • In every state where r has not stopped, a fair step lowers it: r itself, the holder of the lock r waits for, a signaler, or a closer at close.
  • The measure is bounded by a constant, so one induction gives the property from every state.
• The fairness by role (FairRole): r itself, the holder of bufferLock, the holder of waitLock, a signaling writer or closer, and a closing closer. Each follows from weak fairness per thread, because a holder stays the holder while its step is possible. TLC checks that implication in bounded models (WaitForeverMeasure2). tlapm cannot derive it for a symbolic set of threads, so the proof assumes FairRole.

Results (local, 2026-11-13)

• check.sh: 32 models (16 new), each with its expected outcome; 594 s on 4 cores. The forever models of the abstraction have up to 838,813 states, those of the detailed model up to 294,862 (3 readers).
• TLC negative controls, each failing for the right reason:
  • fairness for the system as a whole only: a thread is never scheduled again;
  • no closer: a record reader waits forever for its second byte;
  • a probe that forever runs exist.
• TLAPS negative controls, each making exactly the expected obligation fail:
  • a FALSE lemma;
  • a weight of the measure too small: the arithmetic fails;
  • the stage of decide raised to that of lock: the step that takes bufferLock fails;
  • the closer's fairness removed.
• TLC mutations of the measure (before the proof): a stage that does not drop at bufferLock, the measure without the buffered bytes, and the measure without the stale lock holders all fail MeasureSteps.
• proof.sh with all nine modules: 2,866 s on 4 cores (WSL, tlapm ff40755, the CI's pinned commit). The refinement proof still proves with the new fairness: 2,656 obligations.
• A6 trace validation unchanged: 33/33 accepted, every control as before.

CI

• tla-model: runs check.sh with the new models; timeout 60 → 75 min.
• tlaps-proofs: runs the two new proofs; timeout 90 → 120 min.
• Both jobs run only scheduled or dispatched, so they first run at the next scheduled run after the merge.

Limits

• The TLAPS proof is about the abstraction. Liveness does not carry over by the refinement, so the detailed model's forever liveness rests on TLC's bounded models.

• The proof assumes FairRole. That it follows from fairness per thread is argued above and checked by TLC in bounded models.

• tlapm 1.6.0-pre quirks the proof works around (README):

  • a lemma cannot be instantiated at a term inside ENABLED (probably tlapm#75);
  • expanding ENABLED crashes in a context with a certain unused CASE definition.

  Both are reproduced in minimal modules in TODO.md and not reported yet.

Also: bug-hunt finding F280 (external signals, "max 1 permit")

An external review reported that a semaphore registered with addSignal can get two permits: signalModification() runs after bufferLock is released, and its check for no permit and its release() were two steps. I reproduced it: two concurrent writes left 2 permits.

• Fix: releaseMaxOnePermit, used for all three signal kinds.
  • Under a short signalLock, a thread checks for no permit and claims the semaphore (releasingSignals, an ArrayDeque searched by identity: OpenJML RAC refuses IdentityHashMap).
  • It releases outside the lock.
  • A thread that finds the claim notes its signal (signaledWhileReleasing). After its release, the claimant releases again if the note is there and the permit is gone. Otherwise it drops the claim, also when release() throws.
  • signalLock is never held during release() or while waiting for bufferLock.
  • CodeRabbit found in review that the first version, which skipped a signal that found the claim, could lose one. The claimant released, the observer took the permit and waited again, a second write found the claim and skipped, and the claim was dropped: no permit, unread bytes. Fixed as above, with a test and a TLA+ mode for it.
• The trim signals alone were not racy: they are released under bufferLock.
• Tests:
  • Two deterministic race tests: red before the fix (2 permits), green after.
  • A release() that throws.
  • trim_writeFromTrimStartSignal_startsNoNestedTrim: with the double release gone, PIT no longer saw the isTrimRunning guard of shouldTrim. This test kills that mutant (2 trim starts instead of 1).
  • jcstress SignalMaxOnePermitRace: two writers and a close, exactly one permit.
• Model and proof: StreamBufferSignal.tla, with MaxOne and NoLostSignal.
  • TLC finds the reported race in the code before F280 (SignalNone2, 2 permits).
  • TLC finds CodeRabbit's trace in the first fix (SignalSkip2, a lost signal).
  • SignalReplay3 checks clean.
  • TLAPS (StreamBufferSignalProof.tla, 28 obligations) proves both properties for any number of signalers. With the first fix assumed, exactly the check and clear steps fail.
• More tests: the observer takes the permit while the release is under way (red against the first fix: 0 permits), and two signals with one under way.
• Local: mvn verify 360 tests; PIT 272/272 (100 %); OpenJML RAC (WSL, as the CI job) 348 tests; jcstress default mode, 122 of 122 cases passed, the new test included (before the CodeRabbit fix).
• Docs: BUGHUNT-FOUND.md (F280), CHANGELOG, both READMEs, CLAUDE.md, the Javadoc of addSignal. Not covered, as the Javadoc says: a semaphore registered with two buffers, or released by its observer.

🤖 Generated with Claude Code

https://claude.ai/code/session_01S8cAMbADd1y9p36iFrVkAd

Summary by CodeRabbit

• Bug Fixes
  • Fixed a concurrency issue in semaphore notifications so simultaneous or nested signals don’t exceed the one-permit limit or lose signals. This guarantee applies when only this buffer releases the semaphore.
• Tests
  • Added coverage for concurrent writes, closing, trim callbacks, and release failures.
• Documentation
  • Expanded concurrency and formal-verification notes, including when reads are guaranteed to return and when readers may starve.
• Chores
  • Updated verification checks and CI time limits.