FlashProtocol: a TLA+ model of the FLASH cache-coherence protocol#216
Draft
lemmy wants to merge 5 commits into
Draft
FlashProtocol: a TLA+ model of the FLASH cache-coherence protocol#216lemmy wants to merge 5 commits into
lemmy wants to merge 5 commits into
Conversation
- Introduced a new TLA+ module `FlashWithMutex` that implements a one-action-per-rule translation of the FLASH directory-based cache coherence protocol. - Added a configuration file `MCFlashWithMutex.cfg` defining constants and invariants for the module. - Created a new module `MCFlashWithMutex` that extends `FlashWithMutex`, setting up the environment for multi-core scenarios. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Rework the FLASH translation from a rule-by-rule transcription into idiomatic TLA+, and note where the TLA+ model departs conceptually from the CMurphi original: - Imperative rule bodies (sequential assignments, undefine, for-loops) become a single declarative next-state relation on primed variables; each Murphi state field maps to one Sta record field, updated with EXCEPT rather than mutated in place. - Enumerated rulesets over a scalarset collapse into parameterised actions quantified with \E over the constant sets. In particular the shared/exclusive (Get/GetX) rule pairs merge into single actions (PI_Remote, NI_Remote_Nak, ABS_NI_Remote_Nak_src, ABS_NI_Remote_Nak_src_dst), as GermanWithMutex does for SendReq. - Murphi's undefined values / abstract node become explicit TLA+ sentinels (Undefined, Other) as model values. - The scalarset-order-dependent ghost LastOtherInvAck (a pure history variable) is dropped rather than modelled. Equivalence between the idiomatic model and its rule-by-rule origin is proved with TLAPS: each merged action is shown (by definitional unfolding) equal to the disjunction of the two actions it replaced, which combine to give Next <=> NextOld. The model remains strongly bisimilar to the CMurphi specification (EQUIVALENT at NODE/DATA = 1x1, 1x2, 2x1). Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
…ent steps - Introduced a new `System` definition to encapsulate concrete protocol steps. - Added an `Environment` definition to summarize abstract environment interactions. Prepares the spec for a direct parameterized TLAPS proof by isolating System actions from Environment actions. This refactoring was proved correct with TLAPS; the proof was carried out by Opus 4.8. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The translation originally mirrored CMurphi's `Sta : STATE` as a single record variable, updated field-by-field through nested EXCEPT. Decompose it into one top-level variable per field (Proc, Dir, MemData, ...). This is more idiomatic TLA+: each action reads and updates only the variables it touches, UNCHANGED and the type invariant become per-variable, and the state is easier to inspect in traces and tooling. Unlike the preceding System/Environment refactoring, this change was not proved correct with TLAPS. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
In the PutX branch reached with ~Dir.Dirty /\ elsifCond /\ ~Dir.Local the flat spec left Proc unchanged, whereas the record-based baseline specification invalidates the home cache line (CacheState = "CACHE_I", CacheData = Undefined). Mirror the record behavior so the flat and record encodings agree. This divergence was found by proving per-action equivalence between the flat and record specs with a patched TLAPS. Model checking with TLC did not surface the difference: no reachable state or invariant distinguished the two encodings. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
New spec directory
specifications/FlashProtocolwithFlashWithMutex.tlaand its TLC model, a translation of the FLASH directory-based cache-coherence protocol from Murphi (flashWithMutex.m, CMPOther-node abstraction,Env_o = TRUE). Companion tospecifications/GermanProtocol: same provenance and same method, one level up in protocol complexity.Method
The spec started as an AI-synthesized close 1:1 transcription of the Murphi model: one action per rule, one variable per state field, identical field names and enum spellings (
"CACHE_I","UNI_Get", ...). Conformance was then checked, not assumed: CMurphi's graph export and TLC's state-graph dump are compared by an external tool, which decides state-respecting strong bisimulation -- same behaviours step for step, not merely the same properties.From there the transcription is made idiomatic by individual refactorings, one per commit (declarative actions instead of transcribed assignment order, rulesets over a scalarset as
\E-quantified parameterised actions,Get/GetXaction flavours merged, the state record flattened into per-field variables, ...). Each is proved behaviour-preserving with TLAPS --Next <=> R_Next, per action, under the gluing that relates the two variable sets -- so the bisimulation established for the transcription carries over and need not be re-run.Conformance
All configurations EQUIVALENT (strongly bisimilar):
The full Murphi model (
NODE_NUM = 3, DATA_NUM = 2, symmetry reduction off) is out of reach for a materialised bisimulation; the above exercise every rule and both the node and the data dimension. TLC additionally checksTypeOKand the three safety invariants transcribed from the Murphiinvariants (CacheStateProp,CacheDataProp,MemDataProp); the spec is safety-only, no fairness.Provenance
Murphi source from Divjyot Sethi's
ProtocolDeadlockFiles(https://github.com/dsethi/ProtocolDeadlockFiles/), published with Sethi, Talupur, Malik, "Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom", ATVA 2014, whose FLASH model derives from Chou, Mannava, Park, "A Simple Method for Parameterized Verification of Cache Coherence Protocols", FMCAD 2004. Full chain and attribution in the directory README, as inspecifications/GermanProtocol. The translation and the TLAPS proofs are agentic (AI-produced) and labelled as such.