FlashProtocol: a TLA+ model of the FLASH cache-coherence protocol - #216
Open
lemmy wants to merge 15 commits into
Open
FlashProtocol: a TLA+ model of the FLASH cache-coherence protocol#216lemmy wants to merge 15 commits into
lemmy wants to merge 15 commits into
Conversation
lemmy
force-pushed
the
mku-flash
branch
2 times, most recently
from
July 26, 2026 00:11
97eb4bf to
23cfb01
Compare
lemmy
force-pushed
the
mku-flash
branch
3 times, most recently
from
July 27, 2026 17:25
f9441e0 to
90775ce
Compare
lemmy
marked this pull request as ready for review
July 27, 2026 19:11
- 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>
Both fields transcribed Murphi's `array [NODE] of boolean` as characteristic
functions in [NODE -> BOOLEAN]: membership read as Dir.ShrSet[p], insertion
and removal went through EXCEPT on a nested index, and emptiness tests were
quantifications over NODE. Make them subsets of NODE instead, so membership
is p \in Dir.ShrSet, the updates are \cup and \, and the guards become
Dir.ShrSet = {}, Dir.ShrSet \subseteq {src} and Dir.InvSet \ {src} # {}.
NI_ShWb needs care: ShWbMsg.Proc ranges over ABS_NODE, and the NODE-indexed
array silently dropped it when it was Other. The set version therefore adds
{ShWbMsg.Proc} \cap NODE, keeping ShrSet a subset of NODE.
Proved behaviour-preserving with TLAPS: per action, Next and Init are
equivalent to those of the previous, array-based encoding, under the gluing
that maps each set to its characteristic function. Unlike the record
flattening this changes the state space rather than re-bundling it, so the
equivalence is relative to the Dir conjunct of TypeOK -- the encoding is a
bijection on well-typed directories only. TLC is unchanged at 1231/414 states
for NODE/DATA = 1/1 and 4,533,240/929,572 at 2/2.
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Five actions -- PI_Local_GetX_PutX, NI_Local_GetX_PutX, NI_InvAck and the ABS_ flavours of the latter two -- transcribed Murphi's if/elsif/else as a LET binding each branch's next-state values and an IF chain that repeated the branch condition once per updated variable, so a single branch was spread across a dozen conjuncts. Restate each action as a disjunction of sub-actions that carry their own guard: every branch is now a straight-line list of assignments and each condition appears once. The LET-bound InvP and Cond3 were the same predicate in three actions; hoist it to InvNodes(exclude), the nodes to invalidate less Home and the requester. Likewise NoOtherSharers(req) for the elsif guard, shared by the concrete and abstract flavours, and ProcHomeInvalid resp. ProcHomeInvalidMarked for Home's dropped line. IF survives only where it picks a field value rather than a branch. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to those of the previous form, which stated the branches as IF chains over LET-bound helpers. Both forms have the same variables, so the restructuring is purely propositional and needs no gluing; the only hypothesis is the Dir conjunct of TypeOK, since rewriting IF c THEN a ELSE b as guarded disjuncts requires c \in BOOLEAN and every branch condition is a Boolean Dir field. TLC is unchanged at 1231/414 states for NODE/DATA = 1/1 and 4,533,240/929,572 at 2/2. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Every action spelled its frame condition out as a tuple of up to 20 individual variables, so a one-line update carried three lines of UNCHANGED and adding a variable meant touching all 56 definitions. Group the variables that no action ever changes on its own and name the groups: lastWrVars for the write-tracking ghosts CurrData, LastWrVld and LastWrPtr, pendVars for the pending request's PendReqSrc, PendReqCmd and Collecting, and fwdVars for FwdCmd and FwdSrc. An action that does change one member spells that group's other members out, so no precision is lost; the lists shrink from 881 names to 673. The groups are not chosen by eye: lastWrVars is exactly a class of the partition of the variables by the set of actions whose frame mentions them, so it costs nothing, and pendVars and fwdVars are usable in 42 resp. 30 of the 56 definitions. A netVars for the six message variables was rejected -- it would apply to only 9, since the actions change messages one at a time. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to those of the previous form, which listed the group members individually. The two forms share their variables and every guard and update is the same formula, so unlike the set encoding and the disjunct split this equivalence needs no hypothesis whatever: it reduces to UNCHANGED of a tuple holding a group being UNCHANGED of the tuple with the group spliced in. TLC is unchanged at 1231/414 states for NODE/DATA = 1/1 and 4,533,240/929,572 at 2/2. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The three record who wrote and who acked last: LastWrVld whether any write has happened, LastWrPtr the writing node, LastInvAck the node whose ack closed the last invalidation round. Nothing reads them. No guard, no other variable's update and no invariant mentions them, in flashWithMutex.m either, where they are equally vestigial -- CacheStateProp, CacheDataProp, MemDataProp, Lemma_1 to Lemma_5 and the Progress1_* invariants all ignore them. They are written by Store, ABS_Store, NI_InvAck and ABS_NI_InvAck and by nothing else. Delete them, together with their TypeOK and Init conjuncts; lastWrVars keeps only CurrData and so dissolves back into that variable. The data properties do rest on history, but on CurrData and PrevData, which record what was written rather than by whom and are kept: CacheDataProp reads both and MemDataProp reads CurrData. Dropping LastInvAck empties a branch of ABS_NI_InvAck. Murphi's rule branches on whether concrete invalidation acks are still outstanding, and that branch assigns only LastInvAck and LastOtherInvAck, both of which this translation omits, so ABS_NI_InvAck_More was left holding every one of the 18 variables unchanged. It was an explicit stuttering step, which a TLA+ spec never needs: Spec uses [Next]_vars and is stuttering-invariant by construction. With only the closing branch left there is nothing to disjoin, so ABS_NI_InvAck_Last is inlined and its guard joins the other guards. Next keeps all 49 actions; only the two sub-action definitions go. Since the three refine the state without constraining it, deleting them quotients the reachable graph rather than preserving it: TLC goes from 414 to 78 distinct states for NODE/DATA = 1/1 and from 929,572 to 131,976 at 2/2, generated states from 4,533,240 to 636,852. The projection onto the surviving 18 variables, and with it every invariant, is unchanged. Of that drop in generated states, 13,384 are the ABS_NI_InvAck self-loops that were computed and then discarded. Proved with TLAPS against the previous form, which carried the three. The variable set shrinks, so the two Next relations cannot be equivalent; what is proved per action is that the old action is the new one conjoined with its constraint on the three, and that every old step is a new step. That constraint never appears in a guard, so it cannot affect whether the action is enabled, and it is a conjunction of equalities fixing all three from the unprimed state, so the old step matching a new one exists and is unique -- the forgetful map is a functional bisimulation, not merely a projection. For 45 of the 49 actions the three are simply left unchanged. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
CurrData and PrevData are what is left of the model's history variables now that the write-only ghosts are gone, and neither is self-explanatory at its declaration: CurrData is read by the ABS_* actions as well as by the data properties, so it is not merely auxiliary, while PrevData is read by nothing but CacheDataProp's Collecting case. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Every update of UniMsg, InvMsg, RpMsg, WbMsg, ShWbMsg and NakcMsg assigns all of the record's fields, as do six of the Proc updates and three of the Dir ones. Written as a field-wise EXCEPT, such an update preserves the record type only by inheritance from the old value, and a forgotten field silently keeps whatever was there before -- a stale .Data on a UNI_Nak, say. Replace those 57 updates by record literals: the function-valued ones become [UniMsg EXCEPT ![src] = [Cmd |-> ..., Proc |-> ..., Data |-> ...]], and since WbMsg, ShWbMsg and NakcMsg are plain records, their 20 updates drop the EXCEPT altogether. Fields follow TypeOK's order. Partial updates of Proc and Dir keep their EXCEPT, where carrying the other fields over is the point. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to the previous field-wise form. The equivalence needs TypeOK, and needs it only of the record being updated -- [r EXCEPT !.a = x, !.b = y] and [a |-> x, b |-> y] agree exactly when r has the fields a and b and no others. One bridge lemma per record shape discharges that; the values written need no hypothesis, which is the point of the change. TLC is unchanged at 241/78 states for NODE/DATA = 1/1 and 650,236/131,976 at 2/2. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
At NODE/DATA = 1/1 the invariants say almost nothing. CacheStateProp quantifies over pairs p, q in NODE with p # q and there is no such pair, so it is vacuous. MemDataProp compares MemData with CurrData, which TypeOK confines to a singleton DATA, so it holds in every state. CacheDataProp degenerates into a definedness check, since the only way a cached copy can differ from CurrData is by being Undefined. Home is moreover the only node, so every action guarded by src # Home, dst # Home or src # dst is disabled and the concrete remote paths are exercised only through the Other abstraction. Widen MCFlashWithMutex.cfg to two nodes and two data values, where the pairs exist and a stale datum is distinguishable: 650,236 states, 131,976 distinct, depth 34, 9s. That stays well inside the 30s budget below which CI checks a model exhaustively. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Add APFlashWithMutex.tla, a wrapper that INSTANCEs FlashWithMutex with annotated CONSTANTS and VARIABLES, leaving the spec itself free of tool-specific annotations. Undefined stands for a missing node, a missing datum and a missing command alike, so NodeU, DataU and UniU force NODE, DATA and the command enums into a single Apalache type. Str is the only one that also covers the command spellings, which rules out uninterpreted types for nodes and data. fwdVars == <<FwdCmd, FwdSrc>> pairs two equally typed components, which Snowcat cannot tell apart from a two-element sequence. The group is shadowed in the wrapper by an annotated copy of the same body; SANY warns about the duplicate definition, as it does for the same trick in APDisruptor_SPMC. APFlashWithMutex.cfg checks the four safety properties of MCFlashWithMutex.cfg at NODE/DATA = 2/2. Apalache 0.58.3 reports no error up to computation length 5 in 3m36s, past the 30s budget, so CI smoke-tests the model instead of running it to completion. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
NODE and DATA translate Murphi scalarsets. A scalarset is not merely a set
whose elements happen to be interchangeable; interchangeability is the type's
defining property, and Murphi acts on it by canonicalizing every state before
hashing it. The model was declaring the model values but not the symmetry, so
TLC was exploring the full graph while Murphi explored the quotient. That is
the one thing EQUIV-MANUAL 7.5 tells translators not to do: SYMMETRY must
union all scalarset types, "matching Murphi's symmetry exactly, or the
reachable-state counts (and the checker's quotient) will differ". Declaring it
brings the model into conformance rather than trading fidelity for speed.
Symmetry is sound here: Spec and each checked invariant are preserved by every
permutation in the symmetry set. Home is a variable rather than a distinguished
constant, so it permutes with the remaining state, and the new assumptions
Other \notin DATA and NODE \cap DATA = {} ensure that no permutation moves
Other or Undefined. Only invariants are checked, so the usual restriction on
SYMMETRY with temporal properties does not apply.
The assumptions matter because violating them fails silently. With one model
value shared between NODE and DATA, TLC reports no error: without SYMMETRY it
finds the same 131,976 distinct states at depth 34; with SYMMETRY it finds
109,447 distinct states, three distinct initial states instead of one, and
depth 42. Symmetry reduction cannot increase the depth of the state graph.
The quotient is exactly the one Murphi computes. Under NODE/DATA = 2/2 the
group is S2 x S2, of order four, and both tools divide by four on the nose:
TLC goes from 131,976 distinct states to 32,994, and Murphi from 1,205,832 to
301,458 under exhaustive canonicalization (-sym1). Neither ratio is
approximate and neither has fixpoints, which is the evidence that the
Permutations set declared here is Murphi's symmetry group and not some
coarser or finer relation. Depth is unchanged at 34 and runtime drops from
nine seconds to four.
The manifest's totalStates moves further than the quotient alone accounts for,
from 650,236 to 159,216. The recorded figure was stale: dropping the
ABS_NI_InvAck stuttering branch took the pre-symmetry generated count to
636,852 without the manifest being updated. Only distinctStates divides by the
group order exactly; generated counts depend on the exploration order, which
canonicalization perturbs.
The absolute counts still differ between the two tools, and are meant to.
Murphi's state carries the write-only ghosts LastWrVld, LastWrPtr, LastInvAck
and LastOtherInvAck; this translation drops the first three and the comparator
projects LastOtherInvAck away through ignorePaths. So the count to compare
across tools is the quotient factor, not the state total.
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
The Murphi rules cite five lemmas by name to justify their guards: these are the side conditions that make the `Other`-node abstraction sound, not properties a user cares about. The translation carried the rules but not the lemmas, leaving the citations as unchecked claims. Each Murphi lemma reads `forall h : NODE do h = Home -> ...` and so instantiates h only to Home, which the translations write directly. All five hold, under TLC at NODE/DATA = 2/2 and under Apalache up to computation length 5. They also strengthen the suite: mutants that stall the protocol or loosen a guard slip past the three data properties but violate the lemmas. Co-authored-by: Claude Opus 5 <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
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.