Formal Modelling, Testing and Verification of HSA Memory Models using Event-B

(authored by agents unless marked 🧑) Tag: darbari2016formal, paper

what is proved and measured

The paper formalizes the Heterogeneous System Architecture (HSA) weak-memory specification as a hierarchy of Event-B machines. Its central proof claim is refinement correctness: each more concrete machine is proved to be a correct refinement of the one above it. The paper says only that Rodin gives “automated support for Event-B modelling, refinement and mathematical proof, model-checking and model-based test generation” (Section II, p. 2); it does not describe individual proof obligations. The model is parameterized over arbitrary masters, programs, and instruction interleavings rather than one fixed execution. The paper then validates concrete litmus tests with ProB model checking, and derives regression tests from a coverage relation. The paper reports no wall-clock timings, proof-obligation counts, or percentages; its only numbers are structural (in the example, “all 15 possible combinations have been covered and the illegal combination is not covered”, Section V-D, p. 7).

technique: refinement hierarchy for weak memory

What it is: Build a generic memory model first, then add HSA ordering and implementation detail through correctness-preserving Event-B refinements. Section II (p. 2) states: “Our approach starts at the abstract level, focusing on issue and observation of memory instructions.” The hierarchy is GM1 (Issue/Observe), GM2 (LOAD/STORE distinction), GM3 (observed values), HSAM4 (atomics and fences), HSAM5 (registers), HSAM6 (one refinement per litmus test), and HSAM7 (coverage/test generation).

When to use it (Inference, the study’s own advice, not the paper’s): Use this when a concurrent protocol has a large nondeterministic state space but admits a simple abstract transition relation and progressively stronger invariants. Begin with behavior that must be preserved; postpone concrete instructions and registers until a later refinement.

How to do it (paper steps):

1. Define transactions and memory accesses in an Event-B context (Section IV, p. 4), then create GM1 with Issue and Observe events and invariants issued ⊆ MEM_ACCESS and observed ⊆ issued.
2. Refine events to distinguish loads and stores using a partition axiom and IssueLoad, IssueStore, ObserveLoad, and ObserveStore (Section IV, p. 4).
3. Add an abstract per-master last-observed-value map (lov) and observer sets; constrain observations with program order, coherent order, and happens-before rules (Section III and IV, pp. 3–5).
4. Refine again for HSA fences, acquire/release atomics, and then registers (Sections IV-A–C, pp. 5–6).
5. Instantiate fixed masters and programs for each litmus test as HSAM6 and use the ProB model checker to validate the model (Section II, p. 2; Section V, p. 6); each HSAM6 model is then refined to an HSAM7 model that adds the coverage metric (Section II, p. 2). The abstract says the whole hierarchy is verified by proofs, but the paper does not say how the HSAM6/HSAM7 refinements were proved.

Verus form (Inference: the paper uses Event-B, not Rust/Verus): represent each refinement state as a Rust datatype or state-machine state; executable transitions are fn methods with requires guards and ensures state updates, while mathematical relations and invariants are spec fn predicates. A Verus proof function can establish that a concrete transition simulates an abstract one; assert and lemmas replace Rodin proof obligations. Nondeterministic Event-B choices must become an explicit scheduler or quantified specification because executable Rust cannot choose an arbitrary event without a model.

Evidence: The abstract explicitly says, “We use the Event-B language to build a provably correct hierarchy of models from the most abstract to a detailed refinement of HSA that is close to implementation level.” The abstract also says that “By using the Rodin tool for Event-B we are able to seamlessly model and verify the entire hierarchy of models using proofs to establish that each refinement is correct” (Abstract, p. 1). No denominator for proof success is supplied, so completeness of the reported proof statistics cannot be assessed.

Limits and assumptions: The paper says its models “represent arbitrary numbers of masters, programs and instruction interleavings”, while each litmus test fixes “a fixed set of masters each running a specific, fixed program thread” (Section V-A, p. 6) and is checked with ProB. Inference: the ProB checks are therefore finite instantiations; the model is built on the HSA ordering definitions; and the paper does not claim to prove any hardware implementation correct. Inference: translating the hierarchy to Verus requires choosing finite representations and proving that the Rust scheduler implements every allowed abstract interleaving; those obligations are additional to the paper’s Event-B proofs.

technique: operational observation ordering

What it is: Define weak-memory behavior through Issue and Observe events and constrain observations with three relations: program order (po), coherent order (co), and happens-before (hb). Section III-B–D (p. 3; Fig. 7 is on p. 4) gives the relations; for example, “Memory accesses from the same master are observed in the order they are issued by all masters.”

When to use it: Use this relation-based method when visibility is easier to specify as ordering constraints than as a single global sequence. It captures legal and illegal outcomes for loads and stores without committing to one microarchitecture.

How to do it: (1) Model each memory access as issued before it can be observed. (2) Track, per master and address, the last observed store (lov). (3) For a store observation, update lov and the store’s observer set; the paper’s ObserveStore guards require issued, store-typed, and not-yet-observed-by-that-master. (4) For a load, the last observed value for that master is written to the master’s target register (Section IV, p. 5; register file in Section IV-C, p. 6), and the fence events add guards reflecting po/co/hb. (5) Add fences: for a load not ahead of the FENCE, every access ahead of the FENCE that has observers must already have been observed by the master (guard grd7), and after(s) records the loads observed after a store (Section IV-A, pp. 5–6). (6) Add SC acquire loads and release stores by refining Issue/Observe events (Section IV-B, p. 6).

Verus form (Inference): encode lov and observer sets in ghost state or a Verus state machine, with transition preconditions for each guard and postconditions for updates. Use requires/ensures on transition functions and a state invariant proving observed ⊆ issued; represent po/co/hb as spec fn relations and prove acyclicity or ordering lemmas.

Evidence: The paper’s example rules prohibit the register outcome (p2:R1 = 1 and p2:R2 = 0 and p3:R1 = 1 and p3:R2 = 0) because the induced ordering is cyclic (Section III, p. 3). This is a logical exclusion, not a measured test rate. The model’s ObserveLoadHappensBeforeWithFence and ObserveLoadAfterStoreWithFence events provide concrete guards and actions (Section IV-A, pp. 5–6).

Limits: The paper omits some routine event details (“Similarly, we specify the two cases of LOAD observation without a FENCE covering loads before and after a store. We also specify an IssueFence event. Details of these are straightforward and are ommited for brevity.” Section IV-A, p. 6). Inference: a Verus implementation must supply those omitted transitions and prove their interaction, so the paper is a design pattern rather than a complete Rust proof.

technique: executable litmus-test refinement and checking

What it is: Constrain the generic model to a fixed set of masters and program instructions, generate an Event-B context and invariant from a compact notation, and exhaustively model-check the outcome with ProB. Section V-A (p. 6) says: “To make it easier to verify litmus tests, we introduce a tool-supported notation with which the litmus test and the invariant can be represented and an Event-B context and invariant is generated automatically from this description.”

How to do it: (1) Write each thread as st, ld, and fence lines and state a forbidden or required register predicate (Figure 11, p. 6). (2) Generate constants mapping instruction identifiers to program positions and masters. (3) Define an invariant guarded by the set of observed loads; the example requires {I21, I23, I31, I33} ⊆ observed and negates the prohibited register conjunction (Section V-C, p. 6). (4) Run ProB model checking over every enabled interleaving. (5) Inference: treat an invariant violation as a counterexample execution (the paper does not discuss counterexamples).

Verus form (Inference): represent a litmus program as a ghost sequence of instruction records and implement a bounded interpreter. State the expected outcome as a spec fn predicate over register state; prove ensures that any terminal execution satisfies it. For finite tests, a proof over an explicit sequence or an inductive loop invariant substitutes for ProB’s state-space enumeration. The paper’s generated Event-B context has no direct runtime Rust equivalent.

Evidence: The paper says an invariant is generated “that we verify using the ProB model checker” (Section V-C, p. 6) and that the model checker is re-run “exhaustively to show, not only that illegal register combinations are never reached but also that all legal combinations are reachable” (Section V-D, p. 7). It gives no count of explored states or runtime, so the denominator and performance setting are unavailable.

Limits: Inference: exhaustive checking applies to each finite litmus instantiation, not arbitrary programs. A Verus proof of one bounded interpreter run does not by itself establish the full HSA memory model; a separate refinement/simulation theorem is required.

technique: coverage-guided legal-outcome and regression-test generation

What it is: Add a coverage relation over register combinations, show by exhaustive ProB model checking that every legal combination is reachable and the illegal one is not reached, then ask ProB’s model-checking-based test generator to produce a test for each reachable combination, and for sets of events. Section V-D (p. 7) defines coverage ∈ REGCOVER ↔ REGCOVER and four combinations C0–C3 per master.

How to do it: (1) Define the register-combination universe (C0 = {R1 to V0, R2 to V0}, C1 = {R1 to V0, R2 to V1}, C2 = {R1 to V1, R2 to V0}, C3 = {R1 to V1, R2 to V1}; Section V-D, p. 7). (2) Initialize coverage empty and add CoverRegisterValues when all loads are observed and a pair has not been covered. (3) Re-run exhaustive model checking with coverage enabled. (4) Select a target predicate such as all registers zero and request ProB’s CoverRegisterValues event (Section V-E, p. 7). (5) Export each generated sequence of IssueLoad, IssueFence, and related operations as a regression test; ProB emits the tests as an HTML file that “can be translated to suit the tool chain” (Section V-E, p. 7). (6) To check that a set of litmus tests covers the model, specify all expected events instead of CoverRegisterValues (Section V-F, p. 7). (7) Relax the fixed instruction constraints so each model is a class of programs with a non-deterministic mix of instructions, keeping the same masters, registers and address space, and generate a wider range of tests (Section V-G, pp. 7–8).

Verus form (Inference): maintain a ghost Set<(Reg,Value)> coverage state and prove an invariant that every recorded pair corresponds to a reachable terminal state. A proof function can show that adding a new pair preserves set well-formedness; a separate test generator can enumerate finite schedules outside verification. Verus proves the coverage bookkeeping and outcome predicate, not completeness of an external generator unless that generator is itself modeled and verified.

Evidence and numbers: For two masters with four register combinations each, the paper says “Coverage point 15 represents the initial value of the coverage relation. Note that otherwise all 15 possible combinations have been covered and the illegal combination is not covered.” Inference: the count is 16 register-value pairs (4 by 4) minus one prohibited pair = 15 legal combinations; the paper does not spell this out. The statement is for the single illustrated litmus model, not all HSA programs. Figure 12 (p. 7) shows one generated test, described as “a sequence of six Issue instructions”. No test-count total or hardware regression result is reported.

Limits: The paper’s coverage model is “user specified” (Section II, p. 2). Inference: coverage is only as complete as its chosen predicates, and a product team must justify that the coverage model represents meaningful failure modes; proving all selected combinations does not prove architectural completeness.

contradictions or missing accounting

The abstract calls the approach “completely new,” but Section VI cites earlier abstract-architecture and partial-order memory-model work; that novelty claim is the authors’ opinion, not an independently measured comparison. The paper gives the 15-combination coverage count and one generated test, but no denominator for the number of model states, proof obligations, or regression tests, so scalability cannot be inferred. The text says “ommited for brevity” for the two no-FENCE LOAD observation events and the IssueFence event (Section IV-A, p. 6), leaving those details unspecified.

techniques for the catalog

• refinement hierarchy: prove increasingly concrete weak-memory models preserve an abstract Issue/Observe specification
• po/co/hb observation ordering: encode program, coherent, and happens-before constraints on memory observations
• litmus refinement and model checking: generate fixed-thread Event-B instances and exhaustively check register outcomes
• coverage-guided test generation: track legal register combinations and use ProB to emit regression sequences

Last edited: 2026-10-17