Probabilistic Concurrency Testing for Weak Memory Programs

There is a well-known randomised algorithm for finding concurrency bugs that comes with an actual probability guarantee — it bounds how many scheduling decisions a bug needs and samples from executions with that many, so the odds shrink with the difficulty of the bug rather than the size of the program; this paper (Delft) shows the guarantee silently stops applying on modern hardware, because a whole class of bugs corresponds to no scheduling order at all, and repairs it by counting how much the threads learn from each other instead of when they run.

Why this problem is worth solving

The behaviours real hardware produces are not a subset of the behaviours you can explain by taking turns.

There is one randomised testing algorithm whose appeal is that it comes with a theorem.

What people did before, and where it broke

• Run the program many times and hope. The default, and it does find bugs. Where it broke. The probability of hitting a specific interleaving falls exponentially with the number of scheduling decisions, so a bug requiring a particular order among a few hundred operations will essentially never appear.
• Enumerate executions systematically, with a bound. Explore all schedules with at most a few context switches, or a few preemptions, or a bounded number of phases. Where it broke. The count of executions still explodes, and choosing the bound is guesswork with no statement about what you have covered.
• Sample randomly with a probability guarantee. The algorithm this paper builds on: bound the number of ordering constraints and prove the odds depend only on that. Where it broke. The definition of difficulty it depends on is stated in scheduling terms, which presumes interleaving semantics. Under a weak memory model the algorithm still runs and its theorem no longer covers the executions that matter.
• Test weak memory programs by randomising two things. The state-of-the-art tool for C and C++ atomics picks the next thread at random and separately picks, at random, which write each read observes among those visible to it. Where it broke. It samples from the set of all program executions with no bound and no guarantee, so nothing is known about what it is likely to find.
• Verify instead of test. Model checkers for weak memory exist and are sound. Where it broke. Weak memory verification must explore an even larger space than the interleaving case, so it scales poorly on real programs.
• The gap. One line of work has a guarantee that assumes a semantics real machines do not obey; another handles the real semantics with no guarantee at all. Nobody had asked whether the guarantee could be made to survive the move.

How you bound something other than the schedule

The idea

A theorem can stop applying without anything appearing to break. This is the observation the paper turns on, and it is the kind that is easy to miss because the software keeps working. The guarantee attached to the original algorithm is genuinely strong, and it rests entirely on defining the difficulty of a bug as the fewest ordering constraints needed to expose it. That definition is only meaningful if every behaviour a program can exhibit comes from some interleaving of its threads — and on every processor anyone actually uses, it does not. The two-thread example where both reads return zero is not a hard-to-reach interleaving; it is not an interleaving. So a bug can have no ordering-difficulty at all, in which case the algorithm can be pointed at it, run happily, and offer no probability bound whatsoever. Discovering that careful reasoning was being done against a model the real system does not implement is the same unsettling finding the persistency race work covered elsewhere on this site reports, where programmers reasoning meticulously about crash recovery turn out to have been reasoning about a program the language standard never promised them.

Repairing the definition is the whole contribution, and the test of a good repair is that the old one falls out of it. The replacement is to count not orderings but occasions on which one thread observes another’s work — a read taking a value written elsewhere, or an acquiring operation synchronising with a releasing one. What makes this the right generalisation rather than merely a different measure is the check that follows. Under interleaving semantics, switching threads makes everything the outgoing thread has done visible to the incoming one, so an ordering constraint induces exactly one such occasion; the old notion is the special case where contact and scheduling coincide. The theorem then transfers with the same shape, giving odds exponentially small only in the new difficulty. And the awkward example now has a difficulty of zero, which is not a degenerate answer but a precise one: the bug appears when the threads communicate not at all, each read taking the value its own thread already knows. Finding that the right move is to redefine the quantity being measured so that what you care about becomes expressible is the same manoeuvre the memory consistency testing work covered elsewhere on this site makes when it manufactures near-misses because genuine violations are too rare to count.

Bounding contact instead of scheduling changes the knob into a different kind of knob. Under the old algorithm, restricting the count meant restricting how often threads take turns; here it restricts how much any thread is allowed to learn. Every read that is not one of the chosen few must take its value from its own thread’s private record of what it has seen, which is a strong constraint and a natural one — most reads in most programs are not the ones that matter. The chosen few are then delayed as late as possible, so that by the time they run, the writes they might observe have happened, and they are the only points at which information crosses. A second bound restricts how stale a chosen read’s value may be, cutting its options from every write ever performed to a handful. The result is that the parameter now measures something intrinsic to the bug rather than to the execution: the paper’s synthetic experiment inserts relaxed writes that change neither behaviour nor difficulty, and the original algorithm’s hit rate degrades while the new one holds steady, because the original counts program events and the new one counts only the events that can carry information. That the interesting bugs live in the interactions that rarely occur, and that provoking those deliberately is the only way to see them, is the same lesson the message-reordering work covered elsewhere on this site draws about programs whose correctness must hold under every schedule.

Following one three-thread program at three depths

This setting is not vacuous — it is exactly what exposes the store-buffering bug in the earlier two-thread example, whose difficulty is zero and which the original algorithm cannot characterise at all.

Why it works

• The quantity being bounded has to be defined for the behaviours you are hunting. A bug that appears under no interleaving has no number of ordering constraints, so the original guarantee is silent about exactly the class of bugs that weak memory introduces → whereas every behaviour, interleaved or not, has a well-defined number of moments at which threads observe one another → so the new difficulty is defined everywhere and the bound applies everywhere.
• The new definition contains the old one, which is why nothing is lost. A generalisation that changed the answer for ordinary programs would be a different algorithm rather than an extension → but under interleaving semantics a thread switch makes everything the outgoing thread did visible, so an ordering constraint induces exactly one moment of contact → giving the same difficulty for the same bugs and the same behaviour on sequentially consistent programs.
• Most reads in a program carry no information between threads. Allowing every read to take any visible value makes the sample space the set of all executions, which is what the unguaranteed tools do → but restricting all but a chosen few to their own thread’s private record collapses that space enormously → so the sample is drawn from a small characterised set rather than from everything.
• Delaying the chosen reads is what makes the contact actually happen. Selecting a read as a contact point does nothing if it executes before the write it should observe exists → so its thread’s priority is lowered enough that it runs after the others, in an order the algorithm fixes in advance → which is why the chosen ordering among contact points changes whether the bug appears.
• Counting the right events makes the bound independent of program size. The original bound is exponential in the difficulty but its base is the number of program events, so padding a program with irrelevant operations weakens it → whereas the base here is the number of events that can carry information across threads → which is why inserting relaxed writes leaves the new algorithm’s hit rate flat while the original one degrades.

What it costs (trade-offs and scope)

• The comparison against the original algorithm is against a modified version of it. The original produces only sequentially consistent executions and so cannot find weak memory bugs at all, so the authors implemented a variant whose reads take any observable value uniformly at random. That is a reasonable and clearly stated choice, and it means the head-to-head is against a hybrid built for this paper.
• The margin over that baseline is small. Averaged over nine benchmarks, the modified original improves the bug-hitting rate over the unguaranteed tool by 16 percent and the new algorithm by 29. The paper describes the two as comparable, with the new one slightly better.
• The clear separation appears only in a synthetic experiment. Inserting relaxed writes that change neither behaviour nor bug difficulty makes the original’s hit rate fluctuate and decline while the new one stays flat. This validates the theory exactly, and it is a constructed workload rather than an observed one.
• Both bounded algorithms lose to the unguaranteed tool on one benchmark, and for an instructive reason: that program contains wait loops, and bounding communication prevents a thread from ever learning the value that would let it leave the loop. The remedy is a heuristic that switches to a random thread on detecting a livelock — and the paper notes that the more often it fires, the closer the algorithm gets to plain random testing.
• The second parameter does almost nothing here. Varying the history bound from one to four changes hit rates only slightly and sometimes lowers them, because few writes are visible within the bound in these programs. The case where it should help, programs with many visible writes, is argued rather than tested.
• You must supply the bug difficulty you are looking for, along with an estimate of how many communication events the program has. The mitigation is that hit rates stay comparable when the parameter is set one or two above the true value, which is reported, and it remains a parameter about the thing you have not found yet.
• The guarantee is a loose lower bound. Measured hit rates are frequently 100 percent while the proved bound is one over a quantity exponential in the difficulty. The bound establishes that the approach is not hopeless rather than predicting what it will do.
• Nine small data structures carry the head-to-head evidence. The three real applications are used only to measure overhead and to note that both tools find data races in all of them, with no comparison of detection rates.
• The overhead is real, at roughly 9 to 16 percent slower than the unguaranteed tool on the real applications, from maintaining a private view per thread.
• The claim of memory-model independence is structural rather than demonstrated. The algorithm is organised around two procedures that could be redefined for another model, but both are given only for C and C++, and the specific consistency axiom used follows one particular choice among several competing formulations.
• This is testing, not verification. No execution not sampled is ruled out, which the paper states plainly as the trade the whole field makes for scale.

The evaluation

Check yourself

Sources

The paper is “Probabilistic Concurrency Testing for Weak Memory Programs” by Mingyu Gao, Soham Chakraborty and Burcu Kulahcioglu Ozkan, published at ASPLOS 2023, pages 603-616, DOI 10.1145/3575693.3575729. The authors are at Delft University of Technology.

This explainer is written from the full 14-page text. Everything above comes from the paper’s own sections: the background on weak memory concurrency with its store-buffering example and the categories of C and C++ atomic accesses, and on the original probabilistic testing algorithm contrasted with naive random scheduling on a worked example; the demonstration that a naive application of that algorithm to a weak memory program fails to achieve its stated probability, and the argument that the underlying notion of bug difficulty does not capture weak memory concurrency; the revised definition in terms of communication relations, with the check that thread interleavings induce them and that the two notions agree on the sequentially consistent case; the formalisation of the C and C++ axiomatic model including the event and relation definitions, the derived relations, and the consistency axioms; the definitions of view, communication relation, communication event, bug depth and history depth, and the algorithm together with the procedure that executes an event and updates the thread view; the worked example showing a fence-synchronised program and three example executions of a three-thread message-passing program at difficulty zero, one and two; the probability bound and its derivation; and the evaluation covering the nine data-structure benchmarks with their event counts and bug difficulties, the three real applications, the modified baseline implementation, the hit rates across varying difficulty and history parameters, the comparison against the unguaranteed tool including the wait-loop benchmark where both bounded algorithms lose, the synthetic relaxed-write experiment, and the runtime overhead measurements.