Reorder synthesises minimum fence placements for programs with two threads under a finite x86-TSO model, using SMT queries to find counterexamples and an independent OCaml interpreter to replay each execution before adding its fence constraint.

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 #

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