PaperlayerView exact revision on arXiv

Source-linked AI summary

Stateless Model Checking for TSO and PSO

Parosh Abdulla, Stavros Aronis, Mohammed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos Sagonas

arXiv:1501.02069v1cs.LO

TL;DR

Stateless model checking under TSO and PSO must handle both the combinatorial growth of thread schedules and additional relaxed-memory executions. The paper addresses this with chronological traces and DPOR, achieving full coverage while exploring only executions distinguished by Shasha-Snir traces. Experiments with LLVM assembly from C/pthreads programs show verification effort close to sequential consistency in many cases.

  • Problem

    Stateless model checking must address exponentially many schedules under sequential consistency and further redundant executions introduced by relaxed-memory semantics.

  • Method

    Chronological traces represent TSO and PSO executions with a partial-order happens-before relation that supports DPOR and corresponds one-to-one with Shasha-Snir traces.

  • Results

    The method explores exactly one execution per Shasha-Snir trace, and robust programs require as many explored executions under TSO and PSO as under sequential consistency.

  • Takeaways & Limitations

    Nidhugg applies the technique to LLVM assembly from C/pthreads programs, and its verification effort is almost the same under TSO and PSO as under sequential consistency for typical benchmarks.

  • Takeaways & Limitations

    The presented technique is scoped to TSO and PSO, while extending Nidhugg to Power, ARM, and C/C++ memory models remains future work.

Abstract

from arXiv · show

We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Chronological traces induce a partial order relation on relaxed memory executions, capturing dependencies that are needed to represent the interaction via shared variables. They are optimal in the sense that they only distinguish computations that are inequivalent under the widely-used representation by Shasha and Snir. This allows an optimal dynamic partial order reduction algorithm to explore a minimal number of executions while still guaranteeing full coverage. We apply our techniques to check, under the TSO and PSO memory models, LLVM assembly produced for C/pthreads programs. Our experiments show that our technique reduces the verification effort for relaxed memory models to be almost that for the standard model of sequential consistency. In many cases, our implementation significantly outperforms other comparable tools.

1 Introduction

Relaxed memory models make stateless model checking harder by adding subtle thread interactions and redundant executions beyond sequential consistency. The paper introduces chronological traces and DPOR techniques that avoid equivalent executions while preserving full coverage under TSO and PSO.

  • Relaxed memory models such as TSO and PSO add subtle interactions, including same-thread reordering and buffered stores, to the interleavings that verification must consider.
  • Stateless model checking systematically explores thread schedulings to detect unexpected results, crashes, and assertion violations without false positives or memory explosion.
  • Under sequential consistency, DPOR reduces exponential scheduling growth by exploring one representative for each equivalence class defined by a happens-before relation.
  • Relaxed-memory state structures create additional executions, many equivalent to sequentially consistent executions, requiring DPOR to avoid redundant exploration.
  • Chronological traces provide a canonical partial-order representation with one-to-one correspondence to Shasha-Snir traces, enabling Optimal-DPOR to explore exactly one execution per trace.
  • For robust programs, including data-race-free programs, Optimal-DPOR explores as many relaxed-memory executions as under sequential consistency.
  • The implementation checks bounded executions of C/pthreads programs under SC, TSO, and PSO using generated chronological traces and the Source-DPOR algorithm.

2 Overview of Main Concepts

The overview introduces TSO executions, Shasha-Snir traces, and chronological traces, then shows how chronological traces support DPOR that avoids redundant executions while preserving coverage.

  • TSO: TSO delays stores in per-thread FIFO buffers, allowing executions unavailable under sequential consistency, including both registers ending with value 0.Loads may read from memory or from a same-thread buffered store.
  • Shasha-Snir traces: Shasha-Snir traces encode program order and cross-thread causal dependencies, but their happens-before relation can be cyclic.The representation uses executed instructions as nodes and dependency edges for reads-from, read-before-update, and successive writes.
  • Chronological traces: Chronological traces add explicit update events and selectively omit load-update edges so equivalent buffering cases are not distinguished.They omit relations involving same-thread loads and updates, and updates hidden by an earlier update to the loaded location.
  • Chronological traces: For the buffer-forwarding example, the proposed representation merges three redundant relations and reduces six distinguished cases to the minimal three.The three remaining cases differ in loaded values or final memory values, so they must remain distinct.
  • TSO and PSO: Under PSO, chronological traces omit same-thread edges between updates to different locations, reflecting PSO’s weaker store ordering than TSO.The paper describes a corresponding adaptation of the trace construction for PSO.
  • DPOR: DPOR explores executions by reversing reversible chronological-trace edges, and the example terminates after examining precisely its three chronological traces.One reversal changes the load from reading 1 to reading 2; no further unrepeated reversible edge remains afterward.

3 Formalization

The formalization models TSO executions with program and auxiliary update events, then represents them as chronological traces that preserve the equivalence classes of Shasha-Snir traces. This representation supports DPOR algorithms that cover each relaxed-memory equivalence class, with Optimal-DPOR exploring exactly one execution per class.

  • Operational semantics: The formalization represents TSO configurations with shared memory and per-thread registers, program counters, and store buffers.Stores enter a thread’s buffer, while loads read from memory or forward from the thread’s latest buffered value.
  • Operational semantics: Auxiliary update threads nondeterministically flush the oldest buffered store to memory.A fence is enabled only when the issuing thread’s store buffer is empty.
  • Execution representation: A program execution is a sequence of events generated by deterministic transitions of regular and auxiliary threads.Each event records the executing thread and instruction transition.
  • Chronological traces: Chronological traces are directed graphs over instruction and update events whose six edge relations induce the execution’s happens-before structure.The relations include program order, store-update links, update order, reads-from, overwrite, and update-to-fence dependencies.
  • Trace equivalence: Chronological traces and Shasha-Snir traces induce the same equivalence relation on completed executions.Theorem 1 states T(τ) = T(τ′) iff TC(τ) = TC(τ′).
  • DPOR correctness: Source-DPOR explores at least one execution per Shasha-Snir equivalence class, while Optimal-DPOR explores exactly one.Thus the chronological-trace happens-before relation provides full coverage without redundant equivalent executions.

4 Implementation

The authors implement their relaxed-memory DPOR technique in Nidhugg, a stateless model checker for C programs using pthreads and LLVM compilation. The implementation detects assertion and robustness violations under selected memory models and optimizes spin-loop handling.

  • Nidhugg: Nidhugg checks C programs with pthreads by exploring executions up to a bounded length under relaxed memory models.It uses LLVM compilation rather than a hardware-specific implementation or a custom C semantics.
  • Analysis strategy: Nidhugg detects assertion and robustness violations and implements Source-DPOR adapted to relaxed memory.Before exploration, spin loops are replaced by an equivalent load and assume statement to reduce unproductive loads.

5 Experimental Results

Experiments on C/pthreads benchmarks compare Nidhugg with CBMC and goto-instrument under SC, TSO, and PSO. Nidhugg usually incurs only a modest relaxed-memory cost, often outperforms the comparison tools, and scales to selected real-life code, with PSO slower on memory-location-intensive programs.

  • Benchmark evaluation: The evaluation covers intensely racy benchmarks, classical synchronization algorithms, race-focused programs, mutex-based programs, and industrial code.The comparison includes Nidhugg, CBMC, and goto-instrument across SC, TSO, and PSO analyses.
  • Overall comparison: Nidhugg performs well compared with the other tools for most examples.Table 1 reports analysis times and marks errors, timeouts, crashes, and wrong results with distinct indicators.
  • Memory-model overhead: Nidhugg usually pays only a modest performance price when moving from sequential consistency to TSO and PSO.For robust stack safe.c, the number of Shasha-Snir traces is equal across models, yielding almost identical TSO and PSO runtimes to SC.
  • Tool comparison: For several benchmarks, Nidhugg is several orders of magnitude faster than CBMC and goto-instrument.The implementation is reported to compare favorably with both competing tools.
  • Spin-loop optimization: Replacing spin loops with load-and-assume statements improves analysis on pgsql.c relative to a version where automatic replacement fails.The comparison benchmark is pgsql bnd.c.
  • Observed limitation: Nidhugg is not faster on fib true.c, where a separate checking thread creates many races; forcing threads to join alleviates the problem.The paper demonstrates this with fib true join.c.
  • Larger programs: Nidhugg analyzes approximately 8000-line Apache Portable Runtime benchmarks within a few seconds, but PSO is about three times slower than TSO.The slowdown is attributed to PSO requiring one store buffer per memory location when many locations are accessed.

6 Related Work

The paper positions its contribution as the first application of stateless model checking to relaxed memory models and contrasts chronological traces with bounded, transformed-program, and Xtop-based approaches. Unlike Xtop objects, chronological traces do not distinguish executions that are Shasha-Snir equivalent.

  • Positioning: The authors identify their work as the first application of stateless model checking techniques to relaxed memory models.Related work includes precise analyses, monitoring and testing, and bounded model checking for relaxed-memory programs.
  • Closest approaches: The two closest approaches use bounded model checking across memory models or reduce relaxed-memory verification to sequential consistency through code transformation.The transformation approach augments programs with buffers and queues and introduces Xtop objects.
  • Trace representation: Xtop objects can distinguish executions that are semantically equivalent under Shasha-Snir traces, whereas chronological traces do not.The paper reports an extensive experimental comparison with the corresponding tools.

7 Concluding Remarks

The paper presents Nidhugg and chronological traces for stateless model checking under TSO and PSO, with experiments showing improved performance over comparable tools. The approach is currently scoped to these memory models, with extensions to others left for future work.

  • Chronological traces provide novel execution representations for TSO and PSO and induce a partial-order happens-before relation usable by DPOR.
  • A strict one-to-one correspondence between chronological and Shasha-Snir traces supports the representation's equivalence-preserving design.
  • Nidhugg checks LLVM assembly from C/pthreads programs under SC, TSO, and PSO.
  • Experiments show significantly better performance than CBMC and goto-instrument in many cases.
  • The planned extension to Power, ARM, and C/C++ memory models requires adapting chronological traces while preserving their one-to-one correspondence with Shasha-Snir traces.

A Executions and Traces

The appendix introduces the execution representation and chronological traces, formalizes Shasha-Snir traces for TSO, and proves a one-to-one correspondence between the two trace representations.

  • The appendix formalizes program executions and chronological traces while recalling the TSO model and execution definition.
  • It also formalizes Shasha-Snir traces for TSO and proves a one-to-one correspondence with chronological traces.

A.1 Concurrent Programs

The concurrent-program model uses deterministic threads operating on shared memory under TSO, with store buffers and auxiliary update threads representing delayed memory updates. Executions are sequences of deterministic transitions identified by thread-labelled events.

  • The model assumes deterministic threads executing assembly-like code with stores, loads, and fences over shared memory under TSO.
  • A system configuration consists of thread-local states and shared memory, with each local state containing registers, a program counter, and a store buffer.
  • Each real thread has an auxiliary update thread that nondeterministically flushes pending store-buffer entries to memory.
  • A store appends its address-value pair to the issuing thread's buffer instead of immediately updating memory.
  • Loads read from memory when no buffered entry exists, otherwise forwarding the latest value from the thread's own buffer.
  • A fence is enabled only when the issuing thread's store buffer is empty.
  • An execution is a word of events, each recording a thread identifier and transition information, and event order follows the run sequence.
  • For stores, updst identifies the corresponding update event, while updld identifies the update supplying a load through buffer forwarding.

A.4 Chronological Traces

Chronological traces represent TSO executions as directed graphs whose vertices are instruction and update events and whose edges capture program order, store-update links, update order, value sources, coherence, and fence constraints.

  • A chronological trace is a directed graph containing all instruction and update events from an execution.
  • The trace's edges encode dependencies and ordering constraints among events, including program order and store-to-update correspondence.
  • The illustrated execution includes buffer forwarding, allowing the trace to represent values read from a thread's own pending stores.
  • Updates to the same memory location receive a total chronological order matching their execution order.
  • Source edges connect a load to a different thread's update when that update supplies the loaded value.
  • Coherence edges connect a load to the first later update that overwrites the value it read.
  • Updates from a thread are ordered before its fence because the fence requires all pending updates from that thread to be flushed.

A.5 Shasha-Snir Traces

Shasha-Snir traces represent completed executions as graphs over non-update events and four dependency relations. The paper proves these traces are equivalent, execution-class by execution-class, to chronological traces.

  • Theorem 1 states that two completed executions have identical Shasha-Snir traces if and only if they have identical chronological traces.
  • A completed execution requires every store to have reached memory before its Shasha-Snir trace is defined.
  • Shasha-Snir traces retain non-update events and organize them using program, store, source, and conflict-order relations.Store order totally orders stores to each memory location by when their updates reach memory; source order records which store supplies a load's value.
  • The source relation identifies the store whose value a load reads, including values obtained through memory or buffer forwarding.
  • The equivalence proof matches events and preserves program, store-to-update, update-to-fence, update-to-update, source, and conflict-order relations.

B DPOR for TSO

The paper uses chronological-trace happens-before relations to make DPOR correct for TSO executions. The construction tracks memory, store buffers, buffer forwarding, and vector-clock observations while preserving one representative per equivalence class.

  • Source-DPOR explores at least one execution per Shasha-Snir equivalence class, while Optimal-DPOR explores exactly one.
  • Chronological-trace happens-before relations satisfy the validity conditions required for DPOR correctness.The proof uses partial-order validity, thread ordering, prefix consistency, equivalence-class preservation, and dependency preservation.
  • Buffer-forwarded loads do not immediately synchronize with memory; they are associated with their buffer entry until the corresponding update reaches memory.
  • The auxiliary state combines vector clocks, per-thread store-buffer records, and per-location memory metadata.Buffers retain stores and buffer-forwarded loads; memory metadata records the latest update and latest reads by thread.
  • When memory accesses execute, vector clocks record newly observed events and the procedure computes races for DPOR.

D Chronological Traces Versus Xtop Objects

Chronological traces provide an acyclic representation that remains one-to-one with Shasha-Snir traces, unlike Xtop objects. The distinction matters because Xtop objects can encode multiple representations for one equivalence class.

  • Chronological traces are acyclic yet correspond one-to-one to Shasha-Snir traces, supporting one-execution-per-class exploration.
  • Two Xtop objects may map to the same Shasha-Snir trace, so Xtop objects do not provide the same canonical correspondence.
  • Xtop objects record which event pairs are reordered, whereas chronological traces omit that delayed-event information.
  • The Peterson mutual-exclusion and store-buffering illustrations provide examples of trace structures, while another figure depicts behavior allowed by PSO but not TSO.
Loading 1501.02069v1…