AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM

Martin Beck, Koustubha Bhat, Lazar Stricevic, Geng Chen, Diogo Behrens, Ming Fu and 3 others

Moving concurrent software from Intel processors to Arm ones is not a recompile, because Arm chips are allowed to reorder memory operations that Intel chips are not, and code written against the stricter guarantees breaks in ways that appear only rarely and under load; the job is normally done by hand by a small number of experts, so AtoMig (Huawei Dresden, MPI-SWS, TU Dresden and Shanghai Jiao Tong) automates it by finding the loops where threads wait for each other and working outwards from there — porting millions of lines with about one percent slowdown, and fixing a real bug in MariaDB along the way.

The argument in one glance

Problem

The same program is correct on one processor and broken on another

Weakly ordered processors may reorder memory operations that strongly ordered ones may not — stores to different addresses, for instance. Concurrent code written and tested against the stricter model relies on orderings the new hardware does not provide, and the failures are rare, load-dependent and hard to reproduce.
What people did

Have an expert insert the necessary barriers

Someone who understands both the memory model and the software works out which memory operations must stay ordered and inserts the minimum synchronisation to enforce it. Done well, the result is both correct and fast.
Why it fell short

Experts are scarce, and they get it wrong in both directions

Too few barriers is incorrect; too many is slow, and one unnecessary barrier in a Linux spinlock cost four percent of whole-kernel performance. An attempt to optimise barriers in another Linux lock introduced a bug that went unfixed for three years. Meanwhile a database bug was closed by a change that merely made a compiler hide it.
This paper's idea

Find where threads wait for each other, and work outwards

Rather than searching for every racing access, which needs analysis that does not scale, look for loops whose exit depends on another thread. Those are where synchronisation lives. Strengthen what they touch, then follow the same memory locations through the rest of the program.

Why this problem is worth solving

The thing that differs between the two processor families is not the instruction set.

The rules a processor promises about the order in which one thread’s memory operations become visible to another. The model on Intel processors is comparatively strict: it preserves the order of stores relative to each other, so a thread that writes a message and then sets a flag can be relied on to have the message visible by the time another thread sees the flag. Arm and RISC-V make no such promise, permitting stores to different addresses to be reordered along with much else. Where the algorithm needs an ordering the hardware does not guarantee, the programmer must ask for one with a barrier — either a standalone fence instruction, or an ordering requirement attached to a load or store, which is generally the faster option.

is why a working program can stop working without a line changing.

The construct the whole approach hangs on is easy to state and turns out to be enough.

A loop that keeps executing until some other thread changes something. Formally as this paper defines it, a loop qualifies when every one of its exit conditions depends on memory outside the function, and no store inside the loop that lacks such a dependency can influence those conditions. Together those two clauses say the loop is waiting rather than computing. That is a useful thing to be able to detect, because a thread that waits for another thread is doing synchronisation almost by definition, so the memory locations a spinloop tests are exactly the ones whose ordering matters.

is the entry point that makes the analysis affordable.

What people did before, and where it broke

Make every shared access sequentially consistent. The blunt instrument: order everything, so nothing can be reordered wrongly. Safe, scalable and easy to apply. Where it broke. Speed. Measured here, one database runs 2.49 times slower this way and several concurrent data structures between 3.75 and 5.35 times slower.
Let the hardware pretend to be the old processor. Some Arm chips can run in a stricter mode, which paired with binary translation lets old programs run unchanged. Where it broke. It is specific to particular hardware, does not cover every instruction, and costs real performance — a benchmark scored about 22 percent lower through translation than natively on the same machine.
Have experts do it. Historically how this has been done, and capable of excellent results. Where it broke. There are not enough people who understand both a memory model and a large codebase in detail. One organisation spent several person-years fixing the bugs that surfaced after a manual port, and the fixes turned out to be wrong.
Propose barrier placements and verify them. Generate a candidate set of barriers and use a model checker to prove it correct, refining until it passes. Where it broke. Model checkers examine every distinct execution and cannot handle programs beyond a few thousand lines. They also usually need the code curated or annotated first.
Statically detect the patterns that need barriers. Build a graph of possible executions, apply rules, insert what is missing. Where it broke. It leans on precise alias analysis, which is where the scalability goes; and its coverage depends on the client code available.
Start from everything ordered and remove what is provably unnecessary. The converse strategy, which scales because removal is a local argument. Where it broke. It does not manage to remove very much. Measured on one benchmark suite it ends up 16 percent slower than simply ordering everything, partly because it uses standalone fences where attached ordering would be cheaper.
Run a race detector and strengthen whatever it flags. Practical tooling that already exists. Where it broke. Safety. It only sees what the tests exercise, so the correctness of the result is bounded by test coverage, and getting that coverage takes substantial manual effort.
The gap. Every approach either guarantees correctness and stops at a few thousand lines, or scales and costs too much performance. Nobody had asked whether there is a cheap, syntactic thing to look for that correlates well enough with real synchronisation to be worth targeting.

How a codebase gets ported

From an expert reading code to a compiler pass finding waiting loops

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

Applied to five widely deployed applications from 29,000 to 3.1 million lines, with correctness checked by model checking on smaller concurrent data structures.

The idea

Give up on finding every racing access, and look for something cheap that correlates with them. The reason previous static approaches did not scale is that they tried to answer the general question — which memory accesses can race — and that requires precise alias analysis over the whole program, which is where the memory exhaustion happens. The move here is to answer a much easier question instead. A loop whose exit depends only on values another thread must supply is doing synchronisation, effectively by definition, and detecting one requires only local reasoning about dependencies within the loop. So spinloops become the entry point: find them cheaply, and the variables they test are guaranteed to be interesting. Whether this catches everything is precisely what is given up, and the paper says so — in its own comparison table it marks itself as partially rather than fully safe, and argues that manual porting offers no guarantee either. Trading exhaustive coverage for a small, cheaply detectable target set that captures the cases that actually matter is the same bargain the targeted rowhammer defence covered elsewhere on this site strikes when it protects a handful of addresses instead of all of memory.

Existing annotations record what developers meant, even when they do not do anything. Two of the four detection sources are pure archaeology. Atomic operations already in the code prove concurrent access, but on the old memory model almost every strength of ordering behaved the same, so developers routinely requested weaker ordering than their algorithm actually required and never found out; all of these get promoted. More interesting is the volatile qualifier, which developers reach for on shared variables to stop the compiler optimising them away — and which has no effect whatsoever on what the hardware does with the access. It is therefore a reliable signal of developer belief that a variable is shared, attached to a mechanism that provides none of the guarantees they were reaching for. Turning those into ordered atomics converts an intention into an enforcement. There is a facility to exclude variables marked volatile for hardware reasons rather than concurrency ones, and the paper notes it was never needed in any experiment. Mining an artefact that projects already produce for a different purpose, and extracting from it information nobody was deliberately recording, is the same manoeuvre the binary analysis work covered elsewhere on this site makes with debug information.

The honest position is that verification does not reach this far, so it is traded away deliberately. The paper is unusually direct about what it is not. It provides no formal correctness guarantee. Its correctness evidence comes from running a model checker on small concurrent data structures, which is all that model checking can handle, and the multi-million-line applications it ports are verified by nothing. The argument for accepting this is a comparison of what is on offer: verification-backed placement is correct and stops at a few thousand lines, while everything that scales either costs a large multiple in performance or depends on test coverage. Given a real need to move millions of lines, an unverified tool that is measurably better than the alternatives is the available option. That formal methods in this area operate at a scale several orders of magnitude below production software is not a criticism of them — the concurrency verification work covered elsewhere on this site establishes its results for two devices and a single memory location, which is where rigour currently reaches.

Following one waiting loop through the tool

What happens to a message-passing pattern

One thread prepares data then sets a flag; another spins on the flag then reads the data. Correct on the old model, broken on the new one.

Step 1 of 5

Recognise the loop as waiting rather than computing

The reader loops until the flag changes. Its exit condition depends on a variable outside the function, and nothing the loop itself stores affects that condition. Both clauses of the definition hold, so it is classified as a spinloop.

The analysis needed here is local: chase the loads feeding the loop comparison and check whether the memory they come from is function-local. That is what keeps the cost manageable across millions of lines.

Why it works

A waiting loop is synchronisation by definition, and cheap to spot. Deciding which accesses can race needs whole-program pointer reasoning → but deciding whether a loop exits on something another thread must change needs only local dependency checks inside the loop → so the entry points to synchronisation can be enumerated at a cost that scales, and 12,880 of them were found in one three-million-line database.
The old memory model hid the difference between orderings, so existing annotations understate what is needed. On the stricter model almost every strength of ordering behaved identically for most operations → so code that asked for weak ordering was never punished for it and nobody discovered the mistake → which means promoting all existing atomics to full ordering repairs a class of latent understatement rather than adding redundancy.
A qualifier that constrains the compiler and not the hardware is a pure signal of intent. Marking a variable volatile stops compiler optimisations but changes nothing about how the processor treats the access → so it identifies variables the developer believed were shared while providing none of the ordering they wanted → converting those to ordered atomics turns a belief into a guarantee.
Attached ordering is cheap enough that being generous costs little. The tool adds tens of thousands of ordering constraints, which sounds ruinous → but ordering attached to an existing load or store is much cheaper than a standalone fence → which is why one database absorbs 66,347 of them for a one percent slowdown while ordering everything indiscriminately costs 27 percent.
Approximate alias matching is the right trade at this scale. Precise inter-procedural alias analysis is reported to exhaust memory on large codebases → type and offset matching answers the same question in constant time from a map built once → and its errors are mostly in the direction of strengthening more accesses than needed, which costs a little performance rather than correctness.

What it costs (trade-offs and scope)

There is no formal correctness guarantee, and the paper leads with that. In its own comparison of approaches it marks itself as only partially safe. The defence is that manual porting offers no guarantee either and that everything with a guarantee stops at a few thousand lines, which is a fair argument and not a proof.
The correctness evidence covers small benchmarks only. A model checker was run on concurrent data structures from a library and on one hash table. The five real applications, up to 3.1 million lines, are verified by nothing.
The dangerous failure is a missed synchronisation, and it is inherent. Code that synchronises using only plain loads and stores is not detected by any of the heuristics. The argument that this is rare is partly theoretical — non-trivial wait-free algorithms provably need read-modify-write operations — and partly statistical, that over 80 percent of the algorithms in one library use them.
Alias matching is approximate in both directions. Type-based matching can strengthen accesses that did not need it, costing performance, and can miss accesses through addresses computed at runtime, costing correctness. The authors identify the latter as a real limitation.
Builds take two to three times as long. For the largest application that is about forty minutes instead of twenty. Peak memory is unchanged.
Everything is made fully ordered rather than minimally ordered. The tool does not try to infer the weakest sufficient ordering for each site; it strengthens to sequential consistency wherever it detects something. That is a deliberate simplification and part of why the approach scales.
One of the performance results is measured against a baseline the authors call incorrect. A hash table library exists only in an Intel-targeted version, so the comparison for it runs against code that has no correct counterpart, and shows the highest overheads at 1.10 and 1.40 times.
The comparison against the closest competing tool uses a different benchmark suite, because the authors had difficulty running that tool on their own benchmarks.
Application performance is measured with each project’s own test suite, so the numbers reflect what those suites exercise.
It needs source, or at least compiler intermediate representation. This is what allows the analysis to be effective, and it rules out binary-only settings that some competing approaches target.

The evaluation

Three ways to make code safe on a weakly ordered processor

Property	Order every shared access	Order everything, then remove what is provably redundant
Slowdown on large applications
Slowdown on concurrent data structures		Not measured on these
On a parallel benchmark suite
Scale reached		Limited by its binary lifting frontend
Correctness standing	Safe by construction	Barrier removals are formally verified

Five applications from 29,000 to 3.1 million lines, concurrent data structures from a widely used library, and a parallel benchmark suite, on a 96-core Arm server.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The paper is candid that it offers no formal correctness guarantee, and marks itself as only partially safe in its own comparison of approaches. Its correctness evidence comes from model checking small concurrent data structures, because that is the limit of what model checking reaches; the five real applications, up to 3.1 million lines, carry no such evidence. The dangerous failure mode is a missed synchronisation point, which happens when code coordinates using only plain loads and stores, and the case that this is rare rests on a theoretical result about wait-free algorithms plus a count that over 80 percent of one library’s algorithms use read-modify-write operations. Alias matching is approximate by design, using types and offsets rather than tracking pointers, which can over-strengthen at a cost in speed and can miss accesses through runtime-computed addresses at a cost in correctness — the authors name the latter as a limitation. Everything detected is strengthened to full sequential consistency rather than to the weakest sufficient ordering, which is a deliberate simplification. Builds take two to three times longer. The highest reported overheads come from a library whose baseline the authors themselves describe as incorrect, since no correct version exists for the target. The comparison against the nearest competing tool had to use a different benchmark suite because that tool would not run on theirs. And application performance is measured using each project’s own test suite, so it reflects what those suites happen to exercise.

Background

Why these bugs survive so long

Two stories from the paper explain why this problem needed automating rather than more care. In the first, an organisation ported software by hand, deployed it, and watched weak-memory bugs surface; after several person-years of fixing, the bugs stopped appearing, and it later emerged they had been fixed incorrectly. In the second, a database exhibited a genuine ordering bug. The engineers recognised the symptoms but misdiagnosed the cause, and their response was to reorder the fields of a data structure and remove some volatile annotations — which allowed a compiler optimisation to merge two loads into a single instruction, so the symptom vanished from optimised builds while the bug remained. Unoptimised builds still failed, but no test covered the scenario, so the non-fix was accepted. What both share is that the feedback signal is unreliable: these failures are rare, timing-dependent, and can be suppressed by changes that have nothing to do with the underlying defect, so an engineer’s evidence that a fix worked is much weaker than it appears. That is the same reason concurrency bugs resist ordinary testing at all, and why work on finding them turns to systematically perturbing schedules rather than running more tests, as the concurrency fuzzing research covered elsewhere on this site does. Barriers make it worse in the other direction too, since an unnecessary one is invisible except as a slow program — one redundant barrier in a Linux spinlock cost four percent of whole-kernel performance.

If you remember only three things

1. Weakly ordered processors permit reorderings that stronger ones do not, so concurrent code written and tested against the stricter model breaks when moved — rarely, under load, and in ways that are easily misdiagnosed; the repair is placing barriers, which is hard in both directions, since too few is incorrect and one unnecessary barrier in a Linux spinlock cost four percent of whole-kernel performance.
2. The insight that makes automation tractable is to stop looking for every racing access, which needs whole-program pointer analysis and does not scale, and instead look for loops whose exit depends on another thread — synchronisation almost by definition, detectable with purely local reasoning, and numerous enough to be worth targeting, at 12,880 in one three-million-line database.
3. The position taken is explicitly a trade: no formal correctness guarantee, verification only on benchmarks small enough for a model checker, in exchange for handling millions of lines at around one percent slowdown where ordering everything costs up to 149 percent — and on four hand-ported concurrent data structures the automatically generated version is actually faster than the human one.

Check yourself

Check your understanding

1. Why are spinloops a useful thing to look for?
2. Why does the tool convert variables marked volatile into ordered atomics?
3. Why does ordering a spin variable not fix an optimistic loop such as a sequence lock?
4. What is the paper explicit about giving up, and what does it get in return?

Sources

The paper is “AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM” by Martin Beck, Koustubha Bhat, Lazar Stricevic, Geng Chen, Diogo Behrens, Ming Fu, Viktor Vafeiadis, Haibo Chen and Hermann Haertig, published at ASPLOS 2023, pages 61-73, DOI 10.1145/3575693.3579849. The authors are at Huawei Dresden Research Center, Huawei Central Software Institute, MPI-SWS, TU Dresden and Shanghai Jiao Tong University.

This explainer is written from the full text, read from an author’s copy hosted at MPI-SWS after the publisher’s copy was unavailable. Everything above comes from the paper’s own sections: the motivating account of a manual port whose fixes proved incorrect after several person-years, and of a database bug closed by a change that let a compiler optimisation hide it; the background on memory models, explicit and implicit barriers, and the comparison table of eight porting approaches scored on safety, efficiency, scalability and practicality, including the measured penalty of hardware-assisted translation and the reasons verification-backed and alias-analysis-based approaches do not scale; the design covering the three explicit annotation sources of existing atomics, volatile qualifiers and inline assembly barriers, with the reasoning about why the older memory model let developers understate their ordering requirements and why volatile constrains only the compiler; the formal definition of a spinloop and the worked message-passing example, the separate treatment of optimistic loops with their sequence-lock example and why ordering the control variable is insufficient; the alias exploration scheme with its type and offset matching and the stated reason for preferring it to inter-procedural analysis; the static analysis engineering covering scoped dependency analysis, caching, function inlining for loops spanning calls, and the discussion of false negatives with its theoretical and statistical arguments; and the evaluation covering model checking results across three levels of detection, the discovered database bug with its two reorderings and merged upstream fix, the per-application statistics of lines, loops detected, barriers added and build times, the dynamic barrier counts, and the performance comparisons against ordering everything, against a barrier removal tool on a separate benchmark suite, and on a hash table library whose baseline the authors describe as incorrect.