PaperlayerView exact revision on arXiv

Source-linked AI summary

Software Verification for Weak Memory via Program Transformation

Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig

arXiv:1207.7264v1cs.LOcs.SE

TL;DR

Weak-memory architectures permit behaviors that SC-based verification may miss, and existing weak-memory methods can be limited in model coverage. The paper transforms programs so SC tools can verify them against weak-memory models; experiments demonstrate practical verification, including bugs and fixes in PostgreSQL code, while scalability remains an open challenge.

  • Problem

    Many verification methods assume SC and may miss weak-memory bugs, while existing weak-memory approaches can be model-specific or unable to handle Power/ARM write-atomicity relaxation.

    Source: §1 · p. 1

  • Method

    The paper transforms programs to simulate weak-memory behaviors on SC, using a generic machine with buffers and a queue and architecture-specific protocols.

    Source: §3 · p. 5, §3.1 · p. 5

  • Results

    Experiments demonstrate practicability, confirming a PostgreSQL bug and validating its fix while identifying an additional idiom that will be a bug on future Power machines.

    Source: §6 · pp. 14–15

  • Takeaways & Limitations

    The transformation lifts SC verification tools to a wide range of weak-memory models, from x86 to Power.

    Source: §6 · p. 14

    The weak-memory verification problem remains far from solved, particularly because of scalability.

    Source: §6 · p. 15

Abstract

from arXiv · show

Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. We propose a sound transformation of the program to verify, enabling SC tools to perform verification w.r.t. weak memory. We present experiments for a broad variety of models (from x86/TSO to Power/ARM) and a vast range of verification tools, quantify the additional cost of the transformation and highlight the cases when we can drastically reduce it. Our benchmarks include work-queue management code from PostgreSQL.

1 Introduction

Weak-memory behavior can escape verification when tools assume Sequential Consistency, while existing weak-memory approaches may be model-specific or miss Power/ARM write-atomicity relaxation. The paper proposes a sound program transformation to reuse SC tools across weak-memory models and evaluates it with varied tools, models, and examples.

1 Introduction

  • Most existing verification work assumes SC, while weak-memory approaches often target one model or cannot handle Power/ARM write-atomicity relaxation.The verification problem is also described as non-primitive recursive for TSO and undecidable for RMO-like models.Source: §1 · p. 1
  • The transformation simulates weak-memory behaviors while executing on SC, allowing an SC C-program analyzer to be used without building one tool per architecture.The method augments programs with arrays that simulate buffering and caching scenarios.Source: §1 · p. 1
  • The paper contributes a Coq-proved generic abstract machine and supports x86/TSO, PSO, RMO, and Power alongside eight program analyzers.Its implementation includes Blender, CheckFence, ESBMC, MMChecker, Poirot, SatAbs, Threader, and CImpact.Source: §1 · p. 2
  • Evaluation includes 555 generated litmus tests, published TSO examples, and a PostgreSQL excerpt with a Power-specific bug.The paper reports systematic implementation checks against the theory and verifies both literature examples and the PostgreSQL case.Source: §1 · p. 2
  • The method prioritizes soundness, generality, and implementability, while setting completeness aside and providing an optimization to reduce transformation cost.The authors describe the approach as lifting SC tools across models ranging from x86 to Power.Source: §1 · p. 2

2 Context: Axiomatic Model

The section presents an axiomatic account of weak-memory executions using events and relations between them. An execution is valid when it meets per-address consistency, avoids causal loops, and preserves consensus among relations safe on the architecture.

2 Context: Axiomatic Model

  • The framework of covers SC, Sun TSO (x86), PSO, RMO, Alpha, and a fragment of Power, and is introduced through litmus tests.The section names store buffering and independent reads of independent writes as examples.Source: §2 · p. 2, Figure 1 · p. 3, Figure 2 · p. 3
  • An execution graph represents memory events and their relations; a cycle can indicate a potential violation of processor consensus.The keyword allowed asks whether an architecture permits a specified outcome, such as r1=0;r2=0.Source: §2 · p. 3
  • Each instruction issues read or write events ordered per processor by program order, with dependencies represented by dp.An event has a unique identifier, direction, address, and value.Source: §2 · p. 3
  • The execution witness uses write serialization ws and read-from rf, with from-read fr derived when a read precedes a later memory write than its source write.Together, these relations represent write coherence and how reads obtain values.Source: §2 · pp. 3–4
  • Weak behaviors arise when program order or read-from relations are relaxed; TSO permits write-read reordering and internal read-from relaxation, while Power/ARM can relax external read-from.External read-from relaxation corresponds to non-atomic writes, which the passage says cannot occur on TSO/x86.Source: §2 · p. 4
  • Validity requires per-address SC, no causal loop, and an acyclic consensus among relations safe on the architecture.The conditions are expressed as acyclicity checks over ws, rf, fr, po-loc, dp, and the architecture's safe relations.Source: §2 · p. 4

3 Simulating Weak Behaviours on SC

The paper models weak-memory executions by transforming programs for SC execution, using a shared abstract machine and architecture-specific protocols. Its optimization requires delaying only one pair per critical cycle, while SC executions need no delays.

3.1 The Abstract Machine

  • The machine represents store buffering and caching scenarios, including fully non-atomic stores, through its per-location rather than per-thread buffer.The paper illustrates TSO store buffering and Power caching behavior with sb and iriw+dps examples.Source: §3.1 · pp. 5–7
  • Events split into delayed and flushed parts; program order governs entry, while safe pairs exit in order and delayed pairs exit in reverse order.The machine’s core also enforces uniproc and thin checks.Source: §3.1 · pp. 5–6
  • The abstract machine is equivalent to the axiomatic hierarchy of weak-memory models, expressed operationally through a core machine and architecture-specific protocols.The core uses a per-location write buffer and a load queue; protocols constrain when reads and writes leave them.Source: §3.1 · pp. 5–7, §3 · p. 5

3.2 Reducing the Number of Delay Pairs

  • One delayed pair per critical cycle suffices to simulate a weak execution, and SC executions require no delayed pairs.The selected pairs break critical cycles so an SC tool can reason about the weak-memory behavior.Source: §3.2 · pp. 8–9
  • The axiomatic execution’s partial orders can serve as a canonical representation of equivalent operational paths.The critical-pair characterization identifies which instructions need delaying for weak-memory verification.Source: §3.2 · p. 9
  • For each critical cycle, the transformation selects a delay pair and tags events using program-order and read-from relationships, handling other events directly from memory.The selected pair uses the delayed-exit rule; other pairs use the safe-exit rule.Source: §3.2 · p. 9

4 Implementation

The implementation transforms concurrent C programs into buffered and queued programs for SC verification tools. It approximates event structures and critical cycles, then instruments selected delay pairs while checking its buffer bound.

4 Implementation

  • The implementation translates C into a goto-program and instruments it for a selected model, with x86/TSO, PSO, RMO, and Power available.Transformed programs can be passed to SC analyzers through several supported input formats.Source: §4 · pp. 10–11
  • An abstract event graph over-approximates concrete event structures, and its possible critical cycles over-approximate cycles in concrete executions.Spurious cycles do not impair soundness.Source: §4 · p. 10
  • The tool can transform every delay pair or only one pair per cycle; the latter choice can substantially reduce analyzer time.The passage reports SatAbs times of 21.34 vs. 1.29 seconds on the PostgreSQL excerpt.Source: §4 · p. 11
  • The transformation uses a buffer of size 2 per variable and adds assertions to detect when that bound is exceeded.Writes and loads are transformed with nondeterministic choices, and postponed reads are represented in a queue.Source: §4 · p. 11

5 Experimental Results

Experiments validate the transformation on weak-memory litmus tests and apply it to PostgreSQL code, where Power permits the lb idiom and commonly exhibits mp. The optimized approach verifies more tests than the full transformation, and transforming one rfe pair reduces SatAbs’s verification time for the PostgreSQL example.

Validation

  • The evaluation uses 555 litmus tests of weak-memory effects, including instruction reordering, store buffering, and write atomicity relaxation.The tests are converted to C programs averaging 48 lines and involving two to four threads.Source: §5 · pp. 11–12
  • Across the tests and models, most tools other than Blender and SatAbs timed out or returned wrong results on a vast majority of tests.The comparison covers SC, TSO, PSO, RMO, and Power.Source: §5 · p. 12, Figure 7 · p. 12
  • 533 of 555 tests were verified with the optimized approach, versus 440 with the full approach, in more than twice the time needed for SC.Figure 6 compares the full and optimized transformations across models, tools, and tests.Source: §5 · pp. 12–13, Figure 6 · p. 12

PostgreSQL

  • In the PostgreSQL code, Power commonly exhibits the mp idiom, while the lb idiom is allowed but not observed on current Power machines.The authors note that lb could lead to bugs on future machines.Source: §5 · p. 13
  • 21.34 vs. 1.29 seconds: after transforming one rfe pair for Power’s mp case, SatAbs still finds the counterexample.The original transformed program exposes a buffered write that leaves the latch set while the flag remains unchanged.Source: §5 · p. 14
  • The proposed PostgreSQL patch places two lwsync barriers, after line 8 and before line 12, to solve both lb and mp.Source: §5 · p. 14

6 Conclusion

The paper presents a provably sound program transformation that lets SC verification tools handle a wide range of weak memory models. Its experiments, including the PostgreSQL case, demonstrate practicability, while noting that scalability remains an unresolved challenge.

6 Conclusion

  • The sound transformation lifts SC methods and tools to weak memory models ranging from x86 to Power.The approach relies on a generic operational model equivalent to the axiomatic model of.Source: §6 · p. 14
  • Experiments, particularly the PostgreSQL case, demonstrate practicability through validating a proposed fix and identifying an additional idiom that would be a bug on future Power machines.The proposed fix repairs the additional idiom already.Source: §6 · pp. 14–15
  • The verification problem under weak memory remains far from solved, particularly because of scalability.Source: §6 · p. 15
Loading 1207.7264v1…