VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)

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

scope and result

VSync extends stateless model checking to weak-memory programs containing await loops. Its central procedure is Await Model Checking (AMC), which explores execution graphs, filters redundant await iterations, and reports safety or await-termination violations. This document is the technical report accompanying the ASPLOS’21 paper; it gives AMC in detail (Sec. 1), its correctness proof (Sec. 2), three study cases (Sec. 3) and evaluation setup and microbenchmark results (Sec. 4). The report says, “AMC is an enhancement of stateless model checking (SMC) capable of handling programs with awaits on WMMs.” (Sec. 1, p. 3) Inference: this is stateless model checking of execution graphs, not deductive invariant verification; the theorem covers only programs satisfying the two principles below, and its proof leaves memory-model consistency to case-by-case arguments (see the limits section).

Execution graphs contain read/write events and po, mo, and rf edges. A memory model is a consistency predicate cons_M(G). An await is a loop that, for every possible value of the polled variables, “either exits immediately or loops forever when executed in isolation” (Sec. 1.1, pp. 3-4). Let G_F contain consistent graphs where all awaits exit after a finite number of failed iterations and G_∞ the remaining consistent graphs; await termination (AT) holds iff G_∞ is empty (Definition 1, p. 4).

technique: wasteful-iteration filtering

Use this when an await can repeat reads from the same writes, creating infinitely many graphs with no new information.

1. Represent each candidate execution as a graph and enforce cons_M(G).
2. Define W(G) (wasteful) when an await reads the same combination of writes in two consecutive iterations (Definition 2, Sec. 1.2, p. 5).
3. During exploration discard every graph satisfying W(G). Under the two principles below, every graph in G_F has an equivalent graph in the finite non-wasteful set G_F*, so safety bugs in G_F are also in G_F* (Sec. 1.2, p. 5).
4. When an await read is added, also create a copy of the graph in which that read has no incoming rf edge. This is only a potential AT violation, because another thread may later add a write that resolves it. It becomes an actual violation when a popped graph has no runnable thread, still contains a read without incoming rf, and every consistent graph obtained by adding the missing edge and completing the await iteration is wasteful (Sec. 1.3, p. 7).

The report states, “AMC does not generate wasteful executions, as they do not add any additional information.” (Sec. 1.2, p. 5) In its example, a graph in which T1 reads from its own write twice in the await is wasteful, and none of the infinitely many variants with more reads from that write are generated. An infinite await is represented by a finite graph in which some read lacks an incoming rf edge, provided the mo of every polled variable is finite (Sec. 1.2, p. 6).

technique: bounded-length and bounded-effect conditions

AMC’s guarantees hold for the fragment of programs satisfying two principles (Sec. 1.2, p. 6).

• Bounded-Length: there is a bound b, chosen globally for the program, such that all executions in G_1 have length at most b. The paper says informally that the number of steps outside awaits is bounded, each failed await iteration is bounded, and infinite loops in client code are disallowed.
• Bounded-Effect: the effect of a failed await iteration is limited to that iteration. In graph terms, rf edges starting with writes generated by a failed iteration must go to reads generated in the same iteration; only writes that change the variable’s value matter (footnote 5). The formal version (Definition 3, Sec. 2.2, p. 17) is stricter: it forbids write events in failed iterations altogether and forbids register read-from edges that leave a failed iteration.

Why they suffice (Sec. 1.2, p. 6):

1. Bounded-Effect allows removing any failed iteration from a graph without affecting the rest, so any bug in a graph of G_F is also present in a graph of G_1.
2. With both principles, graphs in G_k are bounded for every k; the bound is b + (k-1)·x, where x is the maximum number of steps in a failed iteration of an await in G_1.
3. Together they imply that mo and the number of awaits are bounded, so G_F* is finite, G_∞* contains only finite graphs, and AMC terminates. AMC explores at most all graphs in G_F* and up to one graph in G_∞*.

For the primitives they studied, the authors argue the principles hold because awaits “either just poll a variable (without side effects) or perform some operation which only changes global state if it succeeds”, e.g. await_while(q==0); or await_while(!trylock(&L));, and the generic client code calls each primitive function a bounded number of times (Sec. 1.2, pp. 6-7). Inference: applying AMC to new code means checking that its awaits fit this pattern and that the client has no unbounded loops.

The correctness statement is: “For programs which satisfy the Bounded-Length principle and the Bounded-Effect principle, 1) AMC terminates, 2) AMC detects every possible safety violation, 3) AMC detects every possible non-terminating await, and 4) AMC has no false positives.” (Sec. 1.2, p. 7; restated as Theorem 1, Sec. 2, p. 8, with proofs in Secs. 2.1-2.3, pp. 8-26)

technique: depth-first graph exploration

VSync implements AMC on top of GenMC (Sec. 1.3, p. 7). The search is a depth-first construction driven by a stack of possibly incomplete or inconsistent graphs, initialized with the empty graph. Each iteration pops a graph and discards it if it violates cons_M or is wasteful. Otherwise the program state is rebuilt by emulating the threads over the graph, the runnable set is computed (a thread leaves it when it terminates or is stuck in an await), and an arbitrary runnable thread is picked. For its next instruction:

• failed assertion: stop and report the graph as a counterexample;
• write: for every existing read of the same variable, push a partial copy with an rf edge from the new write to that read (the function CalcRevisits of GenMC);
• read: for every write in the graph, push a copy with an rf edge from it; if the read is in an await, also push the copy with no incoming rf edge.

case study and optimization workflow

To optimize existing code, the report says custom atomics written in assembly have to be replaced with compiler builtin atomics or with VSync atomics, which compile down to builtin atomics (Sec. 3.3, pp. 30-31). For qspinlock the authors replaced Linux atomics with VSync atomics, and since Linux cmpxchg has a full barrier before and after only on success, they wrapped VSync’s atomic_cmpxchg with an added fence in the success case (Fig. 22). The qspinlock code used a union readable and writable with 8, 16 or 32 bits; because “AMC requires that accesses to the same memory locations always have the same size”, they changed all accesses to 32 bits (p. 31).

The DPDK v20.05 MCS lock had a missing rel barrier before or at the store to prev->next (Line 27 of Fig. 13), which can make Alice hang; AMC gives the counterexample graph for await termination in text form (Sec. 3.1, p. 27). Making Alice’s store rel and Bob’s read acq creates a synchronizes-with edge that fixes it under IMM (Figs. 14-15, p. 28); on ARM, making Alice’s write rel is sufficient (Fig. 17). The authors could not reproduce the DPDK bug on real hardware; they confirmed it on ARM with Rmem by asserting that Bob does not see alice->locked reverted to 1 (p. 28). They also report that the explicit fence at Line 32 appears useless (p. 29).

The internal Huawei MCS lock had a missing acq barrier at the end of mcslock_acquire() that “causes serious data corruption problems”; the authors reproduced it on real hardware and reported it with a fix (Sec. 3.2, p. 29).

For qspinlock, they based the work on Linux 4.4 and backported prefetch instructions from 5.6 so that only barriers differ (Sec. 3.3, p. 30). Table 1 (p. 31) reports for VSync 7 acq, 2 rel, 1 sc barriers, 11 minutes and the label VSync-verified. Linux 4.4, 4.16 and 5.6 are listed as Not verified, and 4.5 and 4.8 as having a barrier bug fixed in [6]. The text says VSync’s recommendation took roughly 11 minutes while expert optimization took several release cycles. The authors attribute differences from Linux 5.6 to multiple maximally relaxed correct combinations and to the different memory models (LKMM versus IMM). Inference: this workflow could check Rust atomic code only after its atomics are translated to the modeled memory events; it does not prove Rust ownership or functional postconditions.

performance evidence and limits

The microbenchmark has each thread repeatedly acquire a lock, increment a shared counter and release it. It varies threads over {1, 2, 4, 8, 16, 23, 31, 63, 95, 127} (127 only on the 128-core machine), runs each experiment for 30 seconds, repeats 5 times, and takes the median (Sec. 4.2.1, p. 35). Platforms are a Huawei TaiShan 200 (2 Kunpeng 920, 128 ARMv8 cores) and a GIGABYTE R182-Z91-00 (2 EPYC 7352, 48 cores, 96 with hyperthreading), with frequency fixed at 1.5 GHz (Sec. 4.1, p. 33).

Stability is the maximum throughput divided by the minimum for a parameter group. Table 4 has 741 records: 627 (84.62%) have stability at most 1.1, 114 (15.38%) exceed 1.1, and 45 (6.07%) exceed 1.2 (Sec. 4.2.2, p. 38). The report filters out records with more than 20% stability, which it says discards less than 7% of results. The speedup is T_o/T_s - 1, with T_o and T_s the median throughputs of the VSync-optimized and sc-only variants. Table 5 (p. 39) reports max, mean, min and standard deviation per lock; its caption says it “must be read with care (especially for the values of mean)” because the values aggregate only the authors’ own samples. The report says most speedups are close to 0, and that x86 shows up to 7x for 1 thread (p. 38). It also finds that larger critical sections reduce the effect of barrier optimization (p. 39).

Limits stated in the report: infinite client loops are disallowed by Bounded-Length; AMC requires same-size accesses to a location (Sec. 3.3, p. 31); the proofs “ignore the memory model consistency”, which “can be easily proven on a case by case basis (i.e., for concrete M)”, with a generic proof left as future work (Sec. 2.3, p. 18); and the formal Bounded-Effect definition forbids writes in failed iterations (Sec. 2.2, p. 17). Inference: the trusted base also includes GenMC, the encoding of the memory model’s consistency predicate, and the translation from source atomics to modeled events; the report does not list these. Inference: a Verus product would need its own model of atomics and Rust semantics, and AMC gives no deductive functional proofs.

techniques for the catalog

• wasteful-iteration filtering: discard await graphs whose consecutive iterations read the same writes
• missing-read termination witness: represent a possible non-terminating await with a read lacking an incoming rf edge
• bounded-effect proof: use bounded length and non-escaping failed-iteration effects to guarantee finite, sound exploration
• weak-memory graph checking: explore po/mo/rf graphs under a consistency predicate to find barrier bugs
• barrier optimization search: replace atomics, enumerate barrier modes, and retain modes whose AMC checks pass

Last edited: 2026-10-17