1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

Reorder synthesises minimum fence placements for programs with two threads under a finite [x86-TSO](https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf) model, using SMT queries to find counterexamples and an independent OCaml interpreter to replay each execution before adding its fence constraint.

![A replayed Peterson execution yields fence constraints whose minimum solution excludes every overlapping critical section](media/repair.svg)

On the Peterson fixture it places `mfence` before each flag load and closes the complete graph of 365 reachable states without overlapping critical sections, while a separate SMT query excludes every cheaper placement among the declared candidate locations.

## Example

```sh
dune exec reorder -- repair cases/peterson.sexp --out build/repair
dune exec reorder -- contrast build/repair/witness.sexp build/repair/repair.sexp --animate
dune exec reorder -- graph cases/peterson.sexp build/repair/repair.sexp --animate
```