GermanProtocol

German Protocol Deadlock Example

The TLA+ specifications in this directory are agentic translations — produced by an AI coding agent — and adaptations of the Murphi German cache-coherence protocol (see Provenance below). Each TLA+ specification is checked to describe the same system as its Murphi counterpart — not just that they satisfy the same properties, but that they exhibit exactly the same behavior, step for step.

Specifications

• GermanData.tla models the concrete protocol with cache and message data.
• GermanControl.tla is its data-forgetting control-state abstraction.
• GermanCMPWithMutex.tla applies the CMP abstraction: Other summarizes omitted nodes, and the mutex-derived noninterference guard keeps that abstraction sound.

Their checked refinement order is:

GermanData => GermanControl => GermanCMPWithMutex

The MC* modules and configurations run TLC, including the two refinement checks. The AP* modules and configurations provide Apalache type annotations and bounded safety checks. The names describe each TLA+ model's role; the original Murphi filenames are retained in the provenance below.

What "equivalent" means here

Murphi and TLA+ share essentially the same underlying semantics: each defines a system as a set of behaviors — sequences of states generated by nondeterministically firing guarded transitions (Murphi rules, TLA+ actions) from a set of initial states. This common operational semantics is what renders the two specifications comparable, and it permits each to be interpreted as the same kind of structure — a labeled transition system (LTS): a set of states (each a valuation of the model's variables), a set of initial states, and transitions between states, every transition labeled by the action that produced it.

The two models are declared equivalent iff their LTSs are strongly bisimilar — i.e. there exists a relation pairing states of one side with states of the other such that:

• every initial state on each side is paired with an initial state on the other;
• paired states agree on their observable variable valuations; and
• for every labeled transition one side can take, the other can take a transition with the same label into an again-paired state.

When no bisimulation exists, the check produces a counterexample rather than a bare yes/no.

How the tools fit together

Neither model checker checks any properties or decides equivalence. Each only exhaustively explores its own model and emits its LTS; an independent comparator then decides bisimilarity.

• CMurphi: exhaustively explores the Murphi model's reachable state space — a breadth-first search with the symmetry/multiset reductions turned off — and uses its built-in graph export to emit an LTS of every reachable state and every fired transition.
• TLC: exhaustively enumerates the TLA+ model's reachable states and uses its state-graph dump hook to emit an LTS of the states and their labeled transitions.
• The comparator (a Python program) reads both LTSs (converted into one shared format), aligns them into the shared vocabulary, decides whether they are strongly bisimilar, and reports the verdict.

Limitations

Only finite models can be exported and compared (the usual model-checking constraint). Bisimilarity requires the action granularity to align — each Murphi rule must correspond to a TLA+ action — and paired states must share the same observable valuation, so the result is a state-respecting strong bisimulation. Tractability is bounded by state-space explosion: both sides' complete reachable graphs must be enumerated, exported, and compared, so the models must stay small enough for each full graph to be materialized. Finally, this approach compares only the behavior of the two models; it does not check that their correctness properties (invariants) are themselves equivalent.

Provenance

The TLA+ specification in this directory was created by translating and adapting one or more of the Murphi specifications from:

Divjyot Sethi, ProtocolDeadlockFiles, GitHub repository. https://github.com/dsethi/ProtocolDeadlockFiles/

That repository was published as supplementary Murphi source code for:

Divjyot Sethi, Muralidhar Talupur, and Sharad Malik, “Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom,” Automated Technology for Verification and Analysis (ATVA 2014), LNCS 8837, pp. 330–347. DOI: 10.1007/978-3-319-11936-6_24

The Murphi files in that repository include variants such as germanNoMutex.m, germanWithMutex.m, and germanBuggy.m. These variants are used in the ATVA 2014 work to study deadlock freedom, including a deliberately buggy version that demonstrates a deadlock.

The underlying German protocol model is older than the Sethi–Talupur–Malik artifact. The ATVA 2014 paper identifies its German protocol code as being based on the Murphi model from:

Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park, “A Simple Method for Parameterized Verification of Cache Coherence Protocols,” Formal Methods in Computer-Aided Design (FMCAD 2004), LNCS 3312, pp. 382–398. DOI: 10.1007/978-3-540-30494-4_27

That paper attributes the protocol itself to Steven M. German by personal communication. Steven German's own tutorial on the protocol is available here:

Steven German, "Tutorial on the German Cache Coherence Protocol." https://users.cs.utah.edu/~ganesh/presentations/fmcad04_tutorial2/german/steven-tutorial.pdf

In summary, the provenance of this TLA+ example is:

Steven M. German protocol benchmark
    -> Chou, Mannava, and Park Murphi model, FMCAD 2004
        -> Sethi, Talupur, and Malik Murphi deadlock examples, ATVA 2014
            -> this TLA+ translation/adaptation

Attribution

Please cite the original Murphi artifact and the related publications when reusing this example in research, teaching, or derivative artifacts:

1. Divjyot Sethi, Muralidhar Talupur, and Sharad Malik, “Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom,” ATVA 2014.
2. Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park, “A Simple Method for Parameterized Verification of Cache Coherence Protocols,” FMCAD 2004.
3. Divjyot Sethi’s ProtocolDeadlockFiles repository: https://github.com/dsethi/ProtocolDeadlockFiles/
4. Steven German, “Tutorial on the German Cache Coherence Protocol”: https://users.cs.utah.edu/~ganesh/presentations/fmcad04_tutorial2/german/steven-tutorial.pdf

Licensing

The TLA+ files in this directory should be distributed under the license used by examples.tlapl.us, unless otherwise stated.

Because this example was derived from Murphi source code in an external repository, users should also review the licensing and attribution requirements of the upstream artifact before redistributing modified versions.