33 files changed, 2061 insertions(+), 0 deletions(-)

A .gitignore
A Makefile
A cases/buffering.sexp
A cases/fenced.sexp
A cases/fifo.sexp
A cases/forwarding.sexp
A cases/peterson.sexp
A cases/spinlock.sexp
A check.ml
A dune
A dune-project
A engine.ml
A engine.mli
A layout.ml
A layout.mli
A machine.ml
A machine.mli
A main.ml
A reorder.opam
A sexp.ml
A sexp.mli
A smt/fences.smt2
A smt/laws.smt2
A smt/machine.smt2
A solver.ml
A solver.mli
A store.ml
A store.mli
A syntax.ml
A syntax.mli
A toolchain.json
A view.ml
A view.mli

@@ 1,2 @@
+_build/
+build/

@@ 1,11 @@
+.PHONY: all check demo
+
+all:
+	dune build @all
+
+check:
+	dune runtest --force --no-buffer
+
+demo: all
+	_build/default/main.exe repair cases/peterson.sexp --out build/repair --animate
+	_build/default/main.exe contrast build/repair/witness.sexp build/repair/repair.sexp --animate

@@ 1,11 @@
+(case
+  (name "store buffering")
+  (names x y)
+  (bound 8)
+  (threads
+    ((store 0 1)
+     (load 1 0))
+    ((store 1 1)
+     (load 0 0)))
+  (candidates (0 1) (1 1))
+  (goal (outcome (registers (0 0 0) (1 0 0)) (memory ) (drained false))))

@@ 1,13 @@
+(case
+  (name "store buffering with explicit fences")
+  (names x y)
+  (bound 10)
+  (threads
+    ((store 0 1)
+     (fence)
+     (load 1 0))
+    ((store 1 1)
+     (fence)
+     (load 0 0)))
+  (candidates )
+  (goal (outcome (registers (0 0 0) (1 0 0)) (memory ) (drained false))))

@@ 1,11 @@
+(case
+  (name "FIFO publication order")
+  (names x y)
+  (bound 8)
+  (threads
+    ((store 0 1)
+     (store 1 1))
+    ((load 1 0)
+     (load 0 1)))
+  (candidates )
+  (goal (outcome (registers (1 0 1) (1 1 0)) (memory ) (drained false))))

@@ 1,11 @@
+(case
+  (name "newest buffered store wins")
+  (names x)
+  (bound 7)
+  (threads
+    ((store 0 1)
+     (store 0 2)
+     (load 0 0))
+    ((move 0 0)))
+  (candidates )
+  (goal (outcome (registers (0 0 1)) (memory ) (drained false))))

@@ 1,25 @@
+(case
+  (name "Peterson mutual exclusion")
+  (names flag0 flag1 turn)
+  (bound 14)
+  (threads
+    ((store 0 1)
+     (store 2 1)
+     (load 1 0)
+     (branch 0 0 6)
+     (load 2 1)
+     (branch 1 1 2)
+     (enter)
+     (leave)
+     (store 0 0))
+    ((store 1 1)
+     (store 2 0)
+     (load 0 0)
+     (branch 0 0 6)
+     (load 2 1)
+     (branch 1 0 2)
+     (enter)
+     (leave)
+     (store 1 0)))
+  (candidates (0 1) (0 2) (1 1) (1 2))
+  (goal overlap))

@@ 1,17 @@
+(case
+  (name "atomic exchange spinlock")
+  (names lock)
+  (bound 14)
+  (threads
+    ((exchange 0 0 1)
+     (branch 0 1 0)
+     (enter)
+     (leave)
+     (store 0 0))
+    ((exchange 0 0 1)
+     (branch 0 1 0)
+     (enter)
+     (leave)
+     (store 0 0)))
+  (candidates )
+  (goal overlap))

@@ 1,168 @@
+let checks = ref 0
+let visited = ref 0
+
+let require condition message =
+  if not condition then failwith message;
+  incr checks
+
+let rejects action message =
+  let failed = try action (); false with Invalid_argument _ | Failure _ -> true in
+  require failed message
+
+let read name = Syntax.load ("cases/" ^ name ^ ".sexp")
+
+let laws () =
+  let source = Layout.generate ~timeout:300000 ^ Store.read "smt/machine.smt2" ^
+    "\n" ^ Store.read "smt/laws.smt2" in
+  let answers = Sexp.parse (Solver.script source) in
+  require (answers = List.init 16 (fun _ -> Sexp.Atom "unsat")) "SMT machine laws";
+  print_endline "16 SMT machine laws passed"
+
+let codec () =
+  List.iter (fun text ->
+    let value = Sexp.Atom text in
+    require (Sexp.one (Sexp.print value) = value) "string round trip")
+    [""; "hello"; "with spaces"; "a\"b\\c"; "a\nb\tc"; "lambda \206\187"];
+  List.iter (fun text -> rejects (fun () -> ignore (Sexp.one text)) "malformed expression")
+    ["("; ")"; "(a"; "\"unfinished"; "a b"; "\"\\z\""];
+  require (Sexp.word (Sexp.Atom "#xffffffffffffffff") = -1L) "unsigned 64-bit model value";
+  List.iter (fun name ->
+    let case = read name in
+    require (Syntax.decode (Syntax.encode case) = case) "case round trip")
+    ["buffering"; "forwarding"; "fifo"; "fenced"; "peterson"; "spinlock"]
+
+let fixtures () =
+  List.iter (fun (name, expected) ->
+    let case = read name in
+    let result = Engine.check case Syntax.Tso in
+    let reachable, count = Machine.reachable case Syntax.Tso [] case.bound in
+    visited := !visited + count;
+    require ((result.witness <> None) = expected && reachable = expected) ("fixture " ^ name);
+    Option.iter (fun witness ->
+      let states, _ = Engine.replay witness in
+      require (Machine.bad case states.(witness.bound)) "witness final state";
+      require (List.length (View.frame ~width:148 witness witness.bound) < 52) "trace display height") result.witness;
+    Printf.printf "%-12s %-5s %5d reference states\n%!" name
+      (if result.witness = None then "unsat" else "sat") count)
+    ["buffering", true; "forwarding", false; "fifo", false;
+     "fenced", false; "peterson", true; "spinlock", false]
+
+let differential () =
+  let random = Random.State.make [|731|] in
+  let choose n = Random.State.int random n in
+  let instruction () = match choose 5 with
+    | 0 -> Syntax.Store (choose 2, Int64.of_int (choose 3))
+    | 1 -> Syntax.Load (choose 2, choose 2)
+    | 2 -> Syntax.Move (choose 2, Int64.of_int (choose 3))
+    | 3 -> Syntax.Fence
+    | _ -> Syntax.Exchange (choose 2, choose 2, 1L) in
+  for number = 0 to 17 do
+    let case = {
+      Syntax.name=Printf.sprintf "generated%d" number; names=[|"x"; "y"|]; bound=6;
+      threads=Array.init 2 (fun _ -> Array.init 2 (fun _ -> instruction ()));
+      candidates=[]; goal=Syntax.Outcome {
+        registers=[0, 0, Int64.of_int (choose 2); 1, 0, Int64.of_int (choose 2)];
+        memory=[]; drained=false};
+    } in
+    List.iter (fun model ->
+      let expected, count = Machine.reachable case model [] case.bound in
+      visited := !visited + count;
+      let result = Engine.check case model in
+      require ((result.witness <> None) = expected) "seeded differential query") [Syntax.Sc; Syntax.Tso]
+  done;
+  print_endline "36 seeded SMT queries matched exhaustive reference execution"
+
+let buffers () =
+  let stores = Array.init 10 (fun value -> Syntax.Store (0, Int64.of_int value)) in
+  let case = {Syntax.name="ring wrap"; names=[|"x"|]; bound=22;
+    threads=[|Array.append stores [|Syntax.Load (0, 0)|]; [|Syntax.Move (0, -1L)|]|];
+    candidates=[]; goal=Syntax.Outcome {registers=[0, 0, 9L; 1, 0, -1L]; memory=[]; drained=false}} in
+  List.iter (fun drained ->
+    let actors = Array.of_list (List.concat (List.init drained (fun _ -> [0; 2])) @
+      List.init (11 - drained) (fun _ -> 0) @ [1]) in
+    let result = Engine.check ~bound:(Array.length actors) ~fixed:actors case Syntax.Tso in
+    require (result.witness <> None) "ring reuse and last buffered write") [9; 10];
+  let initial = Machine.initial case in
+  let state = ref initial in
+  for _ = 0 to 7 do
+    match Machine.step case Syntax.Tso [] !state 0 with
+    | Some (next, _) -> state := next | None -> failwith "unexpected full buffer"
+  done;
+  require (Machine.step case Syntax.Tso [] !state 0 = None) "full FIFO blocks ninth store";
+  require (initial.pc = [|0; 0|] && initial.buffers = [|[]; []|]) "transition preserves previous state";
+  require (Machine.step case Syntax.Tso [] initial 2 = None) "empty FIFO cannot drain"
+
+let outcomes () =
+  let case = read "buffering" in
+  let sc = Engine.outcomes case Syntax.Sc in
+  let tso = Engine.outcomes case Syntax.Tso in
+  require (sc = [0L, 1L; 1L, 0L; 1L, 1L]) "SC outcome enumeration";
+  require (tso = [0L, 0L; 0L, 1L; 1L, 0L; 1L, 1L]) "TSO outcome enumeration";
+  print_endline "complete register outcome sets: SC=3, TSO=4"
+
+let graph () =
+  let case = read "peterson" in
+  let graph = Machine.explore case Syntax.Tso [] in
+  require (List.length graph.violations > 0) "unfenced graph exposes overlap";
+  let seen = Hashtbl.create (Array.length graph.states) in
+  Array.iter (fun state -> Hashtbl.add seen state ()) graph.states;
+  let edges = ref 0 in
+  Array.iter (fun state ->
+    for actor = 0 to 3 do
+      match Machine.step case Syntax.Tso [] state actor with
+      | None -> ()
+      | Some (next, _) -> incr edges; require (Hashtbl.mem seen next) "closed graph successor"
+    done) graph.states;
+  require (!edges = graph.edges) "graph edge count";
+  rejects (fun () -> ignore (Machine.explore ~limit:10 case Syntax.Tso [])) "exploration limit is explicit";
+  Printf.printf "unfenced graph closed: %d states, %d edges, %d violating states\n%!"
+    (Array.length graph.states) graph.edges (List.length graph.violations)
+
+let validation () =
+  let case = read "buffering" in
+  List.iter (fun case -> rejects (fun () -> Syntax.validate case) "invalid case") [
+    {case with bound=0}; {case with bound=65}; {case with names=[||]};
+    {case with threads=[||]}; {case with candidates=[0, 9]};
+    {case with candidates=[0, 1; 0, 1]};
+    {case with threads=[|[|Syntax.Load (0, 4)|]; case.threads.(1)|]};
+    {case with threads=[|[|Syntax.Branch (0, 0L, 3)|]; case.threads.(1)|]}];
+  rejects (fun () -> ignore (Engine.check ~fixed:[|0|] case Syntax.Tso)) "fixed schedule bound mismatch"
+
+let repair folder =
+  let case = read "peterson" in
+  let report = match Engine.repair case folder with
+    | Some report -> report | None -> failwith "expected repair" in
+  require (List.length report.fences = 2) "minimum repair has two fences";
+  let checked = Engine.audit (Filename.concat folder "repair.sexp") (Filename.concat folder "audit") in
+  require (report = checked) "repair certificate audit";
+  List.iter (fun fences ->
+    let found, _ = Machine.reachable case Syntax.Tso fences case.bound in
+    require found "every cheaper fence placement still fails") ([] :: List.map (fun location -> [location]) case.candidates);
+  let graph = Machine.explore case Syntax.Tso report.fences in
+  require (graph.violations = []) "repaired complete state graph excludes overlap";
+  let witness = Engine.load_witness (Filename.concat folder "witness.sexp") in
+  let fixed = Machine.reschedule case report.fences witness.actors in
+  Engine.validate_schedule case report.fences fixed;
+  let states, _ = Machine.replay case Syntax.Tso report.fences fixed in
+  require (not (Machine.bad case states.(Array.length states - 1))) "repaired requested schedule avoids overlap";
+  rejects (fun () -> ignore (Engine.replay {witness with actors=[|2|]})) "tampered witness rejected";
+  let unrepairable = {(read "buffering") with candidates=[]} in
+  require (Engine.repair unrepairable (Filename.concat folder "impossible") = None) "unrepairable case terminates";
+  Printf.printf "minimum repair checked: 2 fences; repaired graph closed with %d states and no overlap\n%!"
+    (Array.length graph.states)
+
+let () =
+  let started = Unix.gettimeofday () in
+  let folder = Filename.concat (Filename.get_temp_dir_name ()) (Printf.sprintf "reorder%d" (Unix.getpid ())) in
+  Store.mkdir folder;
+  codec ();
+  laws ();
+  fixtures ();
+  differential ();
+  buffers ();
+  outcomes ();
+  graph ();
+  validation ();
+  repair folder;
+  Printf.printf "%d checks passed; %d bounded reference states; %.1fs\n%!"
+    !checks !visited (Unix.gettimeofday () -. started)

@@ 1,17 @@
+(library
+ (name core)
+ (wrapped false)
+ (modules store sexp syntax machine layout solver engine view)
+ (libraries unix))
+
+(executable
+ (name main)
+ (public_name reorder)
+ (modules main)
+ (libraries core unix))
+
+(test
+ (name check)
+ (modules check)
+ (libraries core unix)
+ (deps (glob_files cases/*.sexp) (glob_files smt/*.smt2)))

@@ 1,7 @@
+(lang dune 3.20)
+(name reorder)
+(generate_opam_files true)
+(package
+ (name reorder)
+ (synopsis "Bounded x86-TSO checking and minimum fence synthesis")
+ (depends (ocaml (>= 5.5))))

@@ 1,241 @@
+type witness = {
+  case : Syntax.t;
+  model : Syntax.model;
+  bound : int;
+  fences : Syntax.location list;
+  actors : int array;
+}
+type result = { witness : witness option; query : Solver.query }
+type phase = Searching of int * Syntax.location list
+  | Counterexample of witness | Excluded of int | Refining of int
+  | Verified of Syntax.location list * int * int
+type repair = {
+  case : Syntax.t;
+  fences : Syntax.location list;
+  clauses : int list list;
+  rounds : int;
+  bound : int;
+  states : int;
+}
+
+let decision = function
+  | Solver.Unknown reason -> failwith ("solver returned unknown: " ^ reason)
+  | answer -> answer
+
+let verify case model fences bound values =
+  let rec split count prefix = function
+    | rest when count = 0 -> List.rev prefix, rest
+    | value :: rest -> split (count - 1) (value :: prefix) rest
+    | [] -> failwith "incomplete scheduler model"
+  in
+  let actors, observations = split bound [] values in
+  let actors = Array.of_list (List.map (fun value -> Int64.to_int (Solver.bits value)) actors) in
+  let states, _ = Machine.replay case model fences actors in
+  let expected = List.concat (Array.to_list (Array.map Machine.observations states)) in
+  if List.map Solver.bits observations <> expected then
+    failwith "solver model disagrees with independent state-by-state replay";
+  actors, states
+
+let witness_sexp (witness : witness) =
+  let open Sexp in
+  List [Atom "witness"; List [Atom "version"; i 1];
+    List [Atom "case"; Syntax.encode witness.case];
+    List [Atom "model"; a (Syntax.model_name witness.model)];
+    List [Atom "bound"; i witness.bound];
+    List (Atom "fences" :: List.map (fun (t, pc) -> List [i t; i pc]) witness.fences);
+    List (Atom "actors" :: Array.to_list (Array.map i witness.actors))]
+
+let fields tag = function
+  | Sexp.List (Sexp.Atom name :: fields) when name = tag -> fields
+  | _ -> invalid_arg ("expected " ^ tag)
+let single key fields = match Sexp.field key fields with
+  | [value] -> value | _ -> invalid_arg ("invalid field " ^ key)
+
+let replay (witness : witness) =
+  Syntax.validate witness.case;
+  Syntax.validate {witness.case with candidates=witness.fences};
+  if witness.bound < 1 || witness.bound > 64 || Array.length witness.actors <> witness.bound then
+    invalid_arg "witness length differs from its bound";
+  let states, events = Machine.replay witness.case witness.model witness.fences witness.actors in
+  if not (Machine.bad witness.case states.(Array.length states - 1)) then
+    invalid_arg "witness does not reach the requested outcome";
+  states, events
+
+let load_witness path =
+  let fields = fields "witness" (Sexp.one (Store.read path)) in
+  if Sexp.integer (single "version" fields) <> 1 then invalid_arg "unsupported witness version";
+  let witness = {
+    case = Syntax.decode (single "case" fields);
+    model = Syntax.model (Sexp.atom (single "model" fields));
+    bound = Sexp.integer (single "bound" fields);
+    fences = List.map Syntax.location (Sexp.field "fences" fields);
+    actors = Array.of_list (List.map Sexp.integer (Sexp.field "actors" fields));
+  } in
+  ignore (replay witness);
+  witness
+
+let save folder result =
+  Store.mkdir folder;
+  Store.write (Filename.concat folder "query.smt2") (Solver.standalone result.query);
+  let path = Filename.concat folder "witness.sexp" in
+  match result.witness with
+  | Some witness -> Store.write path (Sexp.print (witness_sexp witness) ^ "\n")
+  | None -> if Sys.file_exists path then Sys.remove path
+
+let check ?(timeout=300000) ?(tick=fun () -> ()) ?bound ?(fences=[]) ?folder ?fixed case model =
+  let bound = Option.value bound ~default:case.Syntax.bound in
+  let query = Solver.compile ~timeout ?fixed case model fences bound in
+  let witness = match decision (Solver.solve ~timeout ~tick query) with
+    | Solver.Unsat -> None
+    | Solver.Sat values ->
+        let actors, states = verify case model fences bound values in
+        if not (Machine.bad case states.(bound)) then failwith "invalid final model state";
+        Some {case; model; bound; fences; actors}
+    | Solver.Unknown _ -> assert false in
+  let result = {witness; query} in
+  Option.iter (fun folder -> save folder result) folder;
+  result
+
+let blockers (witness : witness) =
+  let states, _ = Machine.replay witness.case Syntax.Tso [] witness.actors in
+  let result = ref [] in
+  Array.iteri (fun i actor ->
+    if actor < 2 && states.(i).buffers.(actor) <> [] then
+      List.iteri (fun candidate location ->
+        if location = (actor, states.(i).pc.(actor)) then result := candidate :: !result)
+        witness.case.candidates) witness.actors;
+  List.sort_uniq compare !result
+
+let repair_sexp (repair : repair) =
+  let open Sexp in
+  List [Atom "repair"; List [Atom "case"; Syntax.encode repair.case];
+    List [Atom "rounds"; i repair.rounds];
+    List [Atom "bound"; i repair.bound]; List [Atom "states"; i repair.states];
+    List (Atom "fences" :: List.map (fun (t, pc) -> List [i t; i pc]) repair.fences);
+    List (Atom "clauses" :: List.map (fun clause -> List (List.map i clause)) repair.clauses)]
+
+let load_repair path =
+  let fields = fields "repair" (Sexp.one (Store.read path)) in
+  let repair = {
+    case = Syntax.decode (single "case" fields);
+    rounds = Sexp.integer (single "rounds" fields);
+    bound = Sexp.integer (single "bound" fields);
+    states = Sexp.integer (single "states" fields);
+    fences = List.map Syntax.location (Sexp.field "fences" fields);
+    clauses = List.map (fun clause -> List.map Sexp.integer (Sexp.list clause)) (Sexp.field "clauses" fields);
+  } in
+  if repair.bound < repair.case.bound || repair.bound > 64 || repair.states < 1 ||
+     repair.rounds <> List.length repair.clauses + 1 ||
+     List.sort_uniq compare repair.fences <> List.sort compare repair.fences ||
+     not (List.for_all (fun location -> List.mem location repair.case.candidates) repair.fences)
+  then invalid_arg "invalid repair certificate";
+  repair
+
+let repair ?(timeout=300000) ?(tick=fun () -> ()) ?(notify=fun _ -> ()) case folder =
+  Store.mkdir folder;
+  List.iter (fun name ->
+    let path = Filename.concat folder name in
+    if Sys.file_exists path then Sys.remove path) ["repair.sexp"; "witness.sexp"];
+  let count = List.length case.Syntax.candidates in
+  let clauses = ref [] in
+  let rounds = ref 0 in
+  let search_bound = ref case.bound in
+  let rec search budget =
+    if budget > count then failwith "fence search exhausted";
+    let candidate = Solver.candidate ~count ~budget !clauses in
+    Store.write (Filename.concat folder "synthesis.smt2") (Solver.standalone candidate);
+    match decision (Solver.solve ~timeout ~tick candidate) with
+    | Solver.Unsat -> notify (Excluded budget); search (budget + 1)
+    | Solver.Sat values ->
+        let selected = List.filter_map Fun.id (List.mapi (fun i value ->
+          if Solver.truth value then Some (List.nth case.candidates i) else None) values) in
+        notify (Searching (budget, selected));
+        let target = Filename.concat folder (Printf.sprintf "round%02d" !rounds) in
+        let bounded = check ~timeout ~tick ~bound:!search_bound ~fences:selected ~folder:target case Syntax.Tso in
+        let result, closure = match bounded.witness with
+          | Some _ -> bounded, None
+          | None ->
+              let graph = Machine.explore case Syntax.Tso selected in
+              match Machine.counterexample graph with
+              | None -> bounded, Some graph
+              | Some actors ->
+                  search_bound := max !search_bound (Array.length actors);
+                  notify (Refining !search_bound);
+                  let deeper = check ~timeout ~tick ~bound:(Array.length actors)
+                    ~fixed:actors ~fences:selected ~folder:target case Syntax.Tso in
+                  if deeper.witness = None then failwith "graph counterexample has no SMT execution";
+                  deeper, None
+        in
+        incr rounds;
+        begin match result.witness with
+        | None ->
+            let lower = Solver.candidate ~count ~budget:(List.length selected - 1) !clauses in
+            begin match decision (Solver.solve ~timeout ~tick lower) with
+            | Solver.Unsat -> () | _ -> failwith "minimum fence certificate is satisfiable"
+            end;
+            Store.write (Filename.concat folder "minimal.smt2") (Solver.standalone lower);
+            let graph = match closure with Some graph -> graph | None -> assert false in
+            let report = {case; fences = selected; clauses = !clauses; rounds = !rounds;
+              bound= !search_bound; states=Array.length graph.states} in
+            Store.write (Filename.concat folder "repair.sexp") (Sexp.print (repair_sexp report) ^ "\n");
+            notify (Verified (selected, report.bound, report.states));
+            Some report
+        | Some witness ->
+            if !rounds = 1 then Store.write (Filename.concat folder "witness.sexp")
+              (Sexp.print (witness_sexp witness) ^ "\n");
+            notify (Counterexample witness);
+            let clause = blockers witness in
+            if clause = [] then None else begin
+              if List.mem clause !clauses then failwith "repeated excluded counterexample";
+              clauses := !clauses @ [clause];
+              search budget
+            end
+        end
+    | Solver.Unknown _ -> assert false
+  in
+  search 0
+
+let certify ?(timeout=300000) ?(tick=fun () -> ()) path =
+  let report = load_repair path in
+  List.iteri (fun i clause ->
+    let path = Filename.concat (Filename.dirname path) (Printf.sprintf "round%02d/witness.sexp" i) in
+    let witness = load_witness path in
+    if witness.case <> report.case || witness.model <> Syntax.Tso || witness.bound > report.bound || blockers witness <> clause then
+      invalid_arg "counterexample does not support its fence constraint") report.clauses;
+  let lower = Solver.candidate ~count:(List.length report.case.candidates)
+    ~budget:(List.length report.fences - 1) report.clauses in
+  begin match decision (Solver.solve ~timeout ~tick lower) with
+  | Solver.Unsat -> () | _ -> invalid_arg "minimum fence count is unsupported"
+  end;
+  let graph = Machine.explore report.case Syntax.Tso report.fences in
+  if graph.violations <> [] || Array.length graph.states <> report.states then
+    invalid_arg "repair state graph does not support the certificate";
+  report
+
+let audit ?(timeout=300000) ?(tick=fun () -> ()) path folder =
+  let report = certify ~timeout ~tick path in
+  let verified = check ~timeout ~tick ~bound:report.bound ~fences:report.fences ~folder report.case Syntax.Tso in
+  if verified.witness <> None then invalid_arg "repair still admits the forbidden outcome";
+  report
+
+let validate_schedule ?(timeout=300000) case fences actors =
+  let bound = Array.length actors in
+  let query = Solver.compile ~timeout ~fixed:actors ~require_goal:false case Syntax.Tso fences bound in
+  match decision (Solver.solve ~timeout query) with
+  | Solver.Sat values -> ignore (verify case Syntax.Tso fences bound values)
+  | _ -> failwith "repaired schedule has no matching SMT execution"
+
+let outcomes ?(timeout=300000) ?(tick=fun () -> ()) case model =
+  let case = {case with Syntax.goal = Syntax.Outcome {registers=[]; memory=[]; drained=false}} in
+  let rec loop found =
+    if List.length found = 16 then failwith "outcome enumeration exceeded sixteen distinct register pairs";
+    let query = Solver.compile ~timeout ~blocks:found case model [] case.bound in
+    match decision (Solver.solve ~timeout ~tick query) with
+    | Solver.Unsat -> List.sort_uniq compare found
+    | Solver.Sat values ->
+        let _, states = verify case model [] case.bound values in
+        let final = states.(case.bound) in
+        loop ((final.regs.(0).(0), final.regs.(1).(0)) :: found)
+    | Solver.Unknown _ -> assert false
+  in
+  loop []

@@ 1,33 @@
+type witness = {
+  case : Syntax.t;
+  model : Syntax.model;
+  bound : int;
+  fences : Syntax.location list;
+  actors : int array;
+}
+type result = { witness : witness option; query : Solver.query }
+type phase = Searching of int * Syntax.location list
+  | Counterexample of witness | Excluded of int | Refining of int
+  | Verified of Syntax.location list * int * int
+type repair = {
+  case : Syntax.t;
+  fences : Syntax.location list;
+  clauses : int list list;
+  rounds : int;
+  bound : int;
+  states : int;
+}
+val check : ?timeout:int -> ?tick:(unit -> unit) -> ?bound:int ->
+  ?fences:Syntax.location list -> ?folder:string -> ?fixed:int array ->
+  Syntax.t -> Syntax.model -> result
+val witness_sexp : witness -> Sexp.t
+val load_witness : string -> witness
+val replay : witness -> Machine.t array * Machine.event array
+val save : string -> result -> unit
+val repair : ?timeout:int -> ?tick:(unit -> unit) -> ?notify:(phase -> unit) ->
+  Syntax.t -> string -> repair option
+val load_repair : string -> repair
+val certify : ?timeout:int -> ?tick:(unit -> unit) -> string -> repair
+val audit : ?timeout:int -> ?tick:(unit -> unit) -> string -> string -> repair
+val validate_schedule : ?timeout:int -> Syntax.t -> Syntax.location list -> int array -> unit
+val outcomes : ?timeout:int -> ?tick:(unit -> unit) -> Syntax.t -> Syntax.model -> (int64 * int64) list

@@ 1,53 @@
+let join = String.concat " "
+
+let structure name constructor fields =
+  let width = List.fold_left (fun sum (_, _, size) -> sum + size) 0 fields in
+  let arguments = join (List.map (fun (field, kind, _) -> Printf.sprintf "(%s %s)" field kind) fields) in
+  let values = join (List.map (fun (field, _, _) -> field) fields) in
+  let high = ref (width - 1) in
+  let selectors = List.map (fun (field, kind, size) ->
+    let low = !high - size + 1 in
+    let result = Printf.sprintf
+      "(define-fun %s ((cells %s)) %s ((_ extract %d %d) cells))" field name kind !high low in
+    high := low - 1;
+    result) fields in
+  [Printf.sprintf "(define-sort %s () (_ BitVec %d))" name width;
+   Printf.sprintf "(define-fun %s (%s) %s (concat %s))" constructor arguments name values] @ selectors
+
+let record name prefix element count size =
+  let fields = List.init count (fun i -> Printf.sprintf "%s%d" prefix i, element, size) in
+  let lines = structure name prefix fields in
+  let value = ref (Printf.sprintf "(%s%d cells)" prefix (count - 1)) in
+  for i = count - 2 downto 0 do
+    value := Printf.sprintf "(ite (= i #x%02x) (%s%d cells) %s)" i prefix i !value
+  done;
+  let fields = List.init count (fun i ->
+    Printf.sprintf "(ite (= i #x%02x) v (%s%d cells))" i prefix i) in
+  lines @ [Printf.sprintf "(define-fun at ((cells %s) (i Index)) %s\n  %s)" name element !value;
+    Printf.sprintf "(define-fun update ((cells %s) (i Index) (v %s)) %s\n  (%s %s))"
+      name element name prefix (join fields)]
+
+let generate ~timeout =
+  if timeout <= 0 then invalid_arg "timeout must be positive";
+  let lines = ["(set-logic QF_BV)"; "(set-option :produce-models true)";
+    Printf.sprintf "(set-option :timeout %d)" timeout;
+    "(define-sort Index () (_ BitVec 8))"; "(define-sort Word () (_ BitVec 64))"] @
+    record "Slots" "indices" "Index" 16 8 @
+    record "Words" "words" "Word" 16 64 @
+    record "Queues" "queues" "Words" 2 1024 @
+    record "Positions" "positions" "Slots" 2 128 @
+    structure "State" "state" [
+      "memory", "Words", 1024; "registers", "Words", 1024;
+      "counters", "Slots", 128; "heads", "Slots", 128; "tails", "Slots", 128;
+      "addresses", "Positions", 256; "values", "Queues", 2048;
+      "positions", "Positions", 256; "critical", "Slots", 128] in
+  let constants = List.map (fun (name, kind, constructor, value, count) ->
+    Printf.sprintf "(define-fun %s () %s\n  (%s %s))" name kind constructor
+      (join (List.init count (fun _ -> value)))) [
+    "zeros", "Words", "words", "#x0000000000000000", 16;
+    "slots", "Slots", "indices", "#x00", 16;
+    "absent", "Slots", "indices", "#xff", 16;
+    "emptyqueues", "Queues", "queues", "zeros", 2;
+    "emptypositions", "Positions", "positions", "slots", 2;
+    "unseen", "Positions", "positions", "absent", 2] in
+  String.concat "\n\n" (lines @ constants) ^ "\n"

@@ 1,1 @@
+val generate : timeout:int -> string

@@ 1,183 @@
+type origin = Memory | Buffer
+type event = Idle | Drain of int * int * int64
+  | Issue of int * int * Syntax.instruction * origin option
+type t = {
+  pc : int array;
+  regs : int64 array array;
+  memory : int64 array;
+  buffers : (int * int64) list array;
+  critical : bool array;
+}
+
+let initial (case : Syntax.t) = {
+  pc = [|0; 0|]; regs = Array.init 2 (fun _ -> Array.make 4 0L);
+  memory = Array.make (Array.length case.names) 0L;
+  buffers = [|[]; []|]; critical = [|false; false|];
+}
+
+let copy state = {
+  pc = Array.copy state.pc; regs = Array.map Array.copy state.regs;
+  memory = Array.copy state.memory; buffers = Array.copy state.buffers;
+  critical = Array.copy state.critical;
+}
+
+let step (case : Syntax.t) memory_model fences state actor =
+  let open Syntax in
+  if actor < 0 || actor > 4 then invalid_arg "invalid scheduler choice";
+  if actor = 4 then Some (state, Idle) else
+  let t = actor mod 2 in
+  let out = copy state in
+  if actor >= 2 then
+    match state.buffers.(t) with
+    | [] -> None
+    | (a, v) :: tail ->
+        out.buffers.(t) <- tail;
+        out.memory.(a) <- v;
+        Some (out, Drain (t, a, v))
+  else
+    let pc = state.pc.(t) in
+    if pc >= Array.length case.threads.(t) ||
+       (List.mem (t, pc) fences && state.buffers.(t) <> []) then None
+    else begin
+      let ins = case.threads.(t).(pc) in
+      out.pc.(t) <- pc + 1;
+      let done_ origin = Some (out, Issue (t, pc, ins, origin)) in
+      match ins with
+      | Store (a, v) ->
+          if List.length state.buffers.(t) = 8 then None
+          else begin
+            if memory_model = Sc then out.memory.(a) <- v
+            else out.buffers.(t) <- state.buffers.(t) @ [a, v];
+            done_ None
+          end
+      | Load (a, r) ->
+          let value, origin = List.fold_left (fun (value, origin) (address, stored) ->
+            if address = a then stored, Buffer else value, origin)
+            (state.memory.(a), Memory) state.buffers.(t) in
+          out.regs.(t).(r) <- value;
+          done_ (Some origin)
+      | Fence -> if state.buffers.(t) <> [] then None else done_ None
+      | Move (r, v) -> out.regs.(t).(r) <- v; done_ None
+      | Branch (r, v, target) ->
+          if state.regs.(t).(r) = v then out.pc.(t) <- target;
+          done_ None
+      | Enter -> out.critical.(t) <- true; done_ None
+      | Leave -> out.critical.(t) <- false; done_ None
+      | Exchange (a, r, v) ->
+          if state.buffers.(t) <> [] then None else begin
+            out.regs.(t).(r) <- state.memory.(a);
+            out.memory.(a) <- v;
+            done_ None
+          end
+    end
+
+let replay case model fences actors =
+  let states = Array.make (Array.length actors + 1) (initial case) in
+  let events = Array.make (Array.length actors) Idle in
+  Array.iteri (fun i actor ->
+    match step case model fences states.(i) actor with
+    | None -> invalid_arg (Printf.sprintf "disabled transition at step %d" i)
+    | Some (state, event) -> states.(i + 1) <- state; events.(i) <- event) actors;
+  states, events
+
+let observations state =
+  List.map Int64.of_int (Array.to_list state.pc) @
+  Array.to_list state.regs.(0) @ Array.to_list state.regs.(1) @
+  Array.to_list state.memory @
+  Array.to_list (Array.map (fun queue -> Int64.of_int (List.length queue)) state.buffers) @
+  Array.to_list (Array.map (fun active -> if active then 1L else 0L) state.critical)
+
+let bad (case : Syntax.t) state =
+  match case.goal with
+  | Syntax.Overlap -> state.critical.(0) && state.critical.(1)
+  | Syntax.Outcome goal ->
+      Array.for_all (fun t -> state.pc.(t) = Array.length case.threads.(t)) [|0; 1|] &&
+      List.for_all (fun (t, r, v) -> state.regs.(t).(r) = v) goal.registers &&
+      List.for_all (fun (a, v) -> state.memory.(a) = v) goal.memory &&
+      (not goal.drained || Array.for_all ((=) []) state.buffers)
+
+let reachable case model fences bound =
+  let start = initial case in
+  let todo = Queue.create () in
+  let seen = Hashtbl.create 512 in
+  Queue.add (start, 0) todo;
+  Hashtbl.add seen start ();
+  let rec search () =
+    if Queue.is_empty todo then false, Hashtbl.length seen else
+    let state, depth = Queue.take todo in
+    if bad case state then true, Hashtbl.length seen else begin
+      if depth < bound then
+        for actor = 0 to 3 do
+          match step case model fences state actor with
+          | Some (next, _) when not (Hashtbl.mem seen next) ->
+              Hashtbl.add seen next ();
+              Queue.add (next, depth + 1) todo
+          | _ -> ()
+        done;
+      search ()
+    end
+  in
+  search ()
+
+let reschedule case fences requested =
+  let state = ref (initial case) in
+  let actors = ref [] in
+  let execute actor = match step case Syntax.Tso fences !state actor with
+    | None -> false
+    | Some (next, _) -> state := next; actors := actor :: !actors; true
+  in
+  Array.iter (fun actor ->
+    if not (execute actor) then begin
+      if actor < 2 then begin
+        while (!state).buffers.(actor) <> [] do
+          if not (execute (actor + 2)) then failwith "cannot drain pending store"
+        done
+      end;
+      if not (execute actor) then ignore (execute 4)
+    end) requested;
+  Array.of_list (List.rev !actors)
+
+type graph = { states : t array; parents : (int * int) array; edges : int; violations : int list }
+
+let explore ?(limit=250000) ?(visit=fun _ _ -> ()) case model fences =
+  let start = initial case in
+  let todo = Queue.create () in
+  let seen = Hashtbl.create 2048 in
+  let states = ref [] in
+  let violations = ref [] in
+  let edges = ref 0 in
+  let insert state parent actor =
+    let id = Hashtbl.length seen in
+    if id >= limit then failwith "state graph exceeds the exploration limit";
+    Hashtbl.add seen state id;
+    states := (id, state, parent, actor) :: !states;
+    Queue.add (id, state) todo;
+    visit state (id + 1)
+  in
+  insert start (-1) 4;
+  while not (Queue.is_empty todo) do
+    let id, state = Queue.take todo in
+    if bad case state then violations := id :: !violations;
+    for actor = 0 to 3 do
+      match step case model fences state actor with
+      | None -> ()
+      | Some (next, _) ->
+          incr edges;
+          if not (Hashtbl.mem seen next) then insert next id actor
+    done
+  done;
+  let values = Array.make (Hashtbl.length seen) start in
+  let parents = Array.make (Array.length values) (-1, 4) in
+  List.iter (fun (id, state, parent, actor) ->
+    values.(id) <- state; parents.(id) <- parent, actor) !states;
+  {states=values; parents; edges= !edges; violations=List.rev !violations}
+
+let counterexample graph =
+  match graph.violations with
+  | [] -> None
+  | id :: _ ->
+      let rec path id actors =
+        let parent, actor = graph.parents.(id) in
+        if parent < 0 then Array.of_list actors else path parent (actor :: actors)
+      in
+      Some (path id [])

@@ 1,21 @@
+type origin = Memory | Buffer
+type event = Idle | Drain of int * int * int64
+  | Issue of int * int * Syntax.instruction * origin option
+type t = {
+  pc : int array;
+  regs : int64 array array;
+  memory : int64 array;
+  buffers : (int * int64) list array;
+  critical : bool array;
+}
+val initial : Syntax.t -> t
+val step : Syntax.t -> Syntax.model -> Syntax.location list -> t -> int -> (t * event) option
+val replay : Syntax.t -> Syntax.model -> Syntax.location list -> int array -> t array * event array
+val observations : t -> int64 list
+val bad : Syntax.t -> t -> bool
+val reachable : Syntax.t -> Syntax.model -> Syntax.location list -> int -> bool * int
+val reschedule : Syntax.t -> Syntax.location list -> int array -> int array
+type graph = { states : t array; parents : (int * int) array; edges : int; violations : int list }
+val explore : ?limit:int -> ?visit:(t -> int -> unit) -> Syntax.t ->
+  Syntax.model -> Syntax.location list -> graph
+val counterexample : graph -> int array option

@@ 1,130 @@
+let () =
+  let exit_code = ref 0 in
+  try
+    if Array.length Sys.argv < 2 then
+      invalid_arg "usage: reorder check|repair|replay|contrast|compare|graph|audit|laws|layout|emit [file] [options]";
+    let command = Sys.argv.(1) in
+    let files = ref [] in
+    let model = ref Syntax.Tso in
+    let bound = ref None in
+    let fences = ref [] in
+    let folder = ref None in
+    let animate = ref false in
+    let delay = ref 0.7 in
+    let width = ref 148 in
+    let timeout = ref 300000 in
+    let location text = match String.split_on_char ':' text with
+      | [t; pc] -> int_of_string t, int_of_string pc
+      | _ -> invalid_arg "fence locations use thread:instruction" in
+    let options = [
+      "--model", Arg.String (fun text -> model := Syntax.model text), "sc or tso";
+      "--bound", Arg.Int (fun value -> bound := Some value), "maximum scheduler transitions";
+      "--fence", Arg.String (fun text -> fences := !fences @ [location text]), "thread:instruction";
+      "--out", Arg.String (fun path -> folder := Some path), "output file or directory";
+      "--animate", Arg.Set animate, "animate actual execution and solver progress";
+      "--delay", Arg.Set_float delay, "seconds per displayed transition";
+      "--width", Arg.Set_int width, "terminal width between 78 and 180 columns";
+      "--timeout", Arg.Set_int timeout, "solver budget in milliseconds";
+    ] in
+    let current = ref 1 in
+    Arg.parse_argv ~current Sys.argv options (fun path -> files := !files @ [path]) "reorder";
+    if !timeout < 1 || !timeout > 3600000 then invalid_arg "timeout outside 1..3600000 milliseconds";
+    let file () = match !files with path :: _ -> path | [] -> invalid_arg "missing input file" in
+    let output fallback = Option.value !folder ~default:fallback in
+    let load () =
+      let case = Syntax.load (file ()) in
+      let case = match !bound with None -> case | Some bound -> {case with Syntax.bound} in
+      Syntax.validate case;
+      case in
+    let with_view case action =
+      let view = View.create ~width:!width ~delay:!delay ~animate:!animate case in
+      Fun.protect ~finally:(fun () -> View.finish view) (fun () -> action view) in
+    let report case result =
+      Printf.printf "%s\nmodel=%s  bound=%d  buffer<=8\n" (View.headline case.Syntax.name)
+        (Syntax.model_name !model) case.bound;
+      match result.Engine.witness with
+      | None -> print_endline "UNSAT  requested outcome excluded within the bound"
+      | Some witness ->
+          Printf.printf "SAT  %d transitions; independent replay passed\n"
+            (Array.fold_left (fun n actor -> if actor = 4 then n else n + 1) 0 witness.actors);
+          exit_code := 1 in
+    begin match command with
+    | "check" ->
+        let case = load () in
+        let result = with_view case (fun view ->
+          Engine.check ~timeout:!timeout ~tick:(fun () -> View.tick view)
+            ~fences:!fences ~folder:(output "build/check") case !model) in
+        report case result
+    | "repair" ->
+        let case = load () in
+        let result = with_view case (fun view ->
+          Engine.repair ~timeout:!timeout ~tick:(fun () -> View.tick view)
+            ~notify:(View.notify view) case (output "build/repair")) in
+        begin match result with
+        | None -> print_endline "No repair exists at the candidate locations"; exit_code := 1
+        | Some result ->
+            Printf.printf "Minimum repair: %d fences; bound %d; %d checked counterexamples\n"
+              (List.length result.fences) result.bound (List.length result.clauses)
+        end
+    | "replay" ->
+        let witness = Engine.load_witness (file ()) in
+        with_view witness.case (fun view -> View.play view witness)
+    | "contrast" ->
+        let witness_path, repair_path = match !files with
+          | [left; right] -> left, right | _ -> invalid_arg "contrast needs a witness and a repair" in
+        let witness = Engine.load_witness witness_path in
+        let repair = Engine.certify ~timeout:!timeout repair_path in
+        with_view witness.case (fun view -> View.contrast view witness repair)
+    | "compare" ->
+        let case = load () in
+        with_view case (fun view ->
+          View.phase view "enumerating sequentially consistent outcomes";
+          let sc = Engine.outcomes ~timeout:!timeout ~tick:(fun () -> View.tick view) case Syntax.Sc in
+          View.phase view "enumerating TSO outcomes";
+          let tso = Engine.outcomes ~timeout:!timeout ~tick:(fun () -> View.tick view) case Syntax.Tso in
+          View.outcomes view sc tso)
+    | "graph" ->
+        let case = load () in
+        let fences = match !files with
+          | [_; path] ->
+              let repair = Engine.certify ~timeout:!timeout path in
+              if case <> repair.case then invalid_arg "graph and repair cases differ";
+              repair.fences
+          | [_] -> !fences
+          | _ -> invalid_arg "graph expects a case and an optional repair" in
+        with_view case (fun view -> ignore (View.graph view fences))
+    | "audit" ->
+        let repair = Engine.audit ~timeout:!timeout (file ()) (output "build/audit") in
+        Printf.printf "repair verified at bound %d\n%d witnesses replayed; lower-budget certificate UNSAT\n"
+          repair.bound (List.length repair.clauses)
+    | "layout" ->
+        let path = output "build/layout.smt2" in
+        Store.write path (Layout.generate ~timeout:!timeout);
+        print_endline path
+    | "emit" ->
+        let case = load () in
+        let query = Solver.compile ~timeout:!timeout case !model !fences case.bound in
+        let path = output "build/query.smt2" in
+        Store.write path (Solver.standalone query);
+        print_endline path
+    | "laws" ->
+        let root = Store.root () in
+        let text = Layout.generate ~timeout:!timeout ^
+          Store.read (Filename.concat root "smt/machine.smt2") ^ "\n" ^
+          Store.read (Filename.concat root "smt/laws.smt2") in
+        Store.write (output "build/laws.smt2") text;
+        let responses = Sexp.parse (Solver.script ~timeout:!timeout text) in
+        if responses <> List.init 16 (fun _ -> Sexp.Atom "unsat") then failwith "machine law check failed";
+        print_endline "16 SMT machine laws verified"
+    | _ -> invalid_arg "unknown command"
+    end;
+    exit !exit_code
+  with
+  | Invalid_argument message | Failure message | Sys_error message ->
+      Printf.eprintf "reorder: %s\n" message;
+      exit 2
+  | Unix.Unix_error (error, operation, _) ->
+      Printf.eprintf "reorder: %s: %s\n" operation (Unix.error_message error);
+      exit 2
+  | Arg.Bad message -> prerr_string message; exit 2
+  | Arg.Help message -> print_string message

@@ 1,23 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Bounded x86-TSO checking and minimum fence synthesis"
+depends: [
+  "dune" {>= "3.20"}
+  "ocaml" {>= "5.5"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+x-maintenance-intent: ["(latest)"]

@@ 1,111 @@
+type t = Atom of string | List of t list
+
+let parse text =
+  let length = String.length text in
+  let position = ref 0 in
+  let fail message = invalid_arg (Printf.sprintf "%s at byte %d" message !position) in
+  let rec space () =
+    if !position < length then
+      match text.[!position] with
+      | ' ' | '\n' | '\r' | '\t' -> incr position; space ()
+      | _ -> ()
+  in
+  let quoted () =
+    incr position;
+    let buffer = Buffer.create 32 in
+    let rec loop () =
+      if !position = length then fail "unterminated string";
+      let character = text.[!position] in
+      incr position;
+      match character with
+      | '"' -> Buffer.contents buffer
+      | '\\' ->
+          if !position = length then fail "incomplete escape";
+          let escaped = match text.[!position] with
+            | 'n' -> '\n' | 'r' -> '\r' | 't' -> '\t'
+            | '"' -> '"' | '\\' -> '\\'
+            | _ -> fail "unsupported escape"
+          in
+          incr position;
+          Buffer.add_char buffer escaped;
+          loop ()
+      | character -> Buffer.add_char buffer character; loop ()
+    in
+    loop ()
+  in
+  let rec value () =
+    space ();
+    if !position = length then fail "expected expression";
+    match text.[!position] with
+    | '(' ->
+        incr position;
+        let rec items result =
+          space ();
+          if !position = length then fail "unterminated list";
+          if text.[!position] = ')' then begin
+            incr position;
+            List (List.rev result)
+          end else items (value () :: result)
+        in
+        items []
+    | ')' -> fail "unexpected closing parenthesis"
+    | '"' -> Atom (quoted ())
+    | _ ->
+        let start = !position in
+        while !position < length && not (List.mem text.[!position] ['('; ')'; ' '; '\n'; '\r'; '\t']) do
+          incr position
+        done;
+        Atom (String.sub text start (!position - start))
+  in
+  let rec values result =
+    space ();
+    if !position = length then List.rev result else values (value () :: result)
+  in
+  values []
+
+let one text = match parse text with
+  | [value] -> value
+  | _ -> invalid_arg "expected one expression"
+
+let rec print = function
+  | Atom text ->
+      if text <> "" && not (String.exists (fun c -> List.mem c ['('; ')'; ' '; '\n'; '\r'; '\t'; '"'; '\\']) text)
+      then text else begin
+        let buffer = Buffer.create (String.length text + 2) in
+        Buffer.add_char buffer '"';
+        String.iter (function
+          | '"' -> Buffer.add_string buffer "\\\""
+          | '\\' -> Buffer.add_string buffer "\\\\"
+          | '\n' -> Buffer.add_string buffer "\\n"
+          | '\r' -> Buffer.add_string buffer "\\r"
+          | '\t' -> Buffer.add_string buffer "\\t"
+          | c -> Buffer.add_char buffer c) text;
+        Buffer.add_char buffer '"';
+        Buffer.contents buffer
+      end
+  | List values -> "(" ^ String.concat " " (List.map print values) ^ ")"
+
+let atom = function Atom text -> text | _ -> invalid_arg "expected atom"
+let list = function List values -> values | _ -> invalid_arg "expected list"
+let field name values =
+  let matches = List.filter_map (function
+    | List (Atom key :: values) when key = name -> Some values
+    | _ -> None) values
+  in
+  match matches with
+  | [values] -> values
+  | [] -> invalid_arg ("missing field " ^ name)
+  | _ -> invalid_arg ("duplicate field " ^ name)
+
+let integer value = int_of_string (atom value)
+let word = function
+  | Atom text when String.starts_with ~prefix:"#x" text ->
+      Int64.of_string ("0x" ^ String.sub text 2 (String.length text - 2))
+  | Atom text when String.starts_with ~prefix:"#b" text ->
+      Int64.of_string ("0b" ^ String.sub text 2 (String.length text - 2))
+  | Atom text -> Int64.of_string text
+  | List [Atom "-"; Atom text] -> Int64.neg (Int64.of_string text)
+  | _ -> invalid_arg "invalid scalar"
+let a text = Atom text
+let i value = Atom (string_of_int value)
+let w value = Atom (Printf.sprintf "0x%016Lx" value)

@@ 1,12 @@
+type t = Atom of string | List of t list
+val parse : string -> t list
+val one : string -> t
+val print : t -> string
+val atom : t -> string
+val list : t -> t list
+val field : string -> t list -> t list
+val integer : t -> int
+val word : t -> int64
+val a : string -> t
+val i : int -> t
+val w : int64 -> t

@@ 1,6 @@
+(set-logic QF_LIA)
+(set-option :produce-models true)
+(set-option :timeout 60000)
+
+(define-fun weight ((enabled Bool)) Int
+  (ite enabled 1 0))

@@ 1,98 @@
+(declare-const s State)
+(declare-const t Index)
+(declare-const other Index)
+(declare-const a Index)
+(declare-const v Word)
+(declare-const r Index)
+(declare-const destination Index)
+
+(assert (bvult t #x02))
+(assert (bvult other #x02))
+(assert (bvult a #x10))
+(assert (bvult r #x04))
+(assert (bvule (at (heads s) t) (at (tails s) t)))
+(assert (bvult (at (tails s) t) #x40))
+(assert (bvult (pending s t) #x08))
+(assert (distinct other t))
+
+(push 1)
+(assert (distinct (read (write s t a v) t a) v))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (memory (write s t a v)) (memory s)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (pending (write s t a v) t) (bvadd (pending s t) #x01)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (pending (write s t a v) other) (pending s other)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (bvugt (pending s t) #x00))
+(assert (distinct (pending (drain s t) t) (bvsub (pending s t) #x01)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (pending (drain s t) other) (pending s other)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (reg (put s t r v) t r) v))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (pc (advance s t destination) t) destination))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (pc (advance s t destination) other) (pc s other)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (at (critical (mark s t #x01)) t) #x01))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (at (memory (exchange s t a r v)) a) v))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (reg (exchange s t a r v) t r) (at (memory s) a)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (reg (load-step s t a r) t r) (read s t a)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (memory (load-step s t a r)) (memory s)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (distinct (pending (fence-step s t) t) (pending s t)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (= (pending s t) #x00))
+(assert (distinct (at (memory (store-step s t a v true)) a) v))
+(check-sat)
+(pop 1)

@@ 1,88 @@
+(define-fun initial () State
+  (state zeros zeros slots slots slots emptypositions emptyqueues unseen slots))
+
+(define-fun pc ((s State) (t Index)) Index
+  (at (counters s) t))
+
+(define-fun reg ((s State) (t Index) (r Index)) Word
+  (at (registers s) (bvadd (bvmul #x08 t) r)))
+
+(define-fun pending ((s State) (t Index)) Index
+  (bvsub (at (tails s) t) (at (heads s) t)))
+
+(define-fun read ((s State) (t Index) (a Index)) Word
+  (let ((index (at (at (positions s) t) a)))
+    (ite (and (bvuge index (at (heads s) t))
+              (bvult index (at (tails s) t)))
+      (at (at (values s) t) (bvand index #x07))
+      (at (memory s) a))))
+
+(define-fun advance ((s State) (t Index) (p Index)) State
+  (state (memory s) (registers s) (update (counters s) t p)
+    (heads s) (tails s) (addresses s) (values s) (positions s) (critical s)))
+
+(define-fun put ((s State) (t Index) (r Index) (v Word)) State
+  (state (memory s) (update (registers s) (bvadd (bvmul #x08 t) r) v)
+    (counters s) (heads s) (tails s)
+    (addresses s) (values s) (positions s) (critical s)))
+
+(define-fun write ((s State) (t Index) (a Index) (v Word)) State
+  (let ((index (at (tails s) t)))
+    (state (memory s) (registers s) (counters s) (heads s)
+      (update (tails s) t (bvadd index #x01))
+      (update (addresses s) t (update (at (addresses s) t) (bvand index #x07) a))
+      (update (values s) t (update (at (values s) t) (bvand index #x07) v))
+      (update (positions s) t (update (at (positions s) t) a index))
+      (critical s))))
+
+(define-fun drain ((s State) (t Index)) State
+  (let ((index (at (heads s) t)))
+    (state
+      (update (memory s)
+        (at (at (addresses s) t) (bvand index #x07))
+        (at (at (values s) t) (bvand index #x07)))
+      (registers s) (counters s)
+      (update (heads s) t (bvadd index #x01)) (tails s)
+      (addresses s) (values s) (positions s) (critical s))))
+
+(define-fun mark ((s State) (t Index) (v Index)) State
+  (state (memory s) (registers s) (counters s)
+    (heads s) (tails s) (addresses s) (values s) (positions s)
+    (update (critical s) t v)))
+
+(define-fun exchange ((s State) (t Index) (a Index) (r Index) (v Word)) State
+  (state (update (memory s) a v)
+    (update (registers s) (bvadd (bvmul #x08 t) r) (at (memory s) a))
+    (counters s) (heads s) (tails s)
+    (addresses s) (values s) (positions s) (critical s)))
+
+(define-fun store-step ((s State) (t Index) (a Index) (v Word) (sc Bool)) State
+  (let ((next (write s t a v)))
+    (advance (ite sc (drain next t) next) t (bvadd (pc s t) #x01))))
+
+(define-fun load-step ((s State) (t Index) (a Index) (r Index)) State
+  (advance (put s t r (read s t a)) t (bvadd (pc s t) #x01)))
+
+(define-fun fence-step ((s State) (t Index)) State
+  (advance s t (bvadd (pc s t) #x01)))
+
+(define-fun move-step ((s State) (t Index) (r Index) (v Word)) State
+  (advance (put s t r v) t (bvadd (pc s t) #x01)))
+
+(define-fun branch-step
+  ((s State) (t Index) (r Index) (v Word) (target Index)) State
+  (advance s t (ite (= (reg s t r) v) target (bvadd (pc s t) #x01))))
+
+(define-fun enter-step ((s State) (t Index)) State
+  (advance (mark s t #x01) t (bvadd (pc s t) #x01)))
+
+(define-fun leave-step ((s State) (t Index)) State
+  (advance (mark s t #x00) t (bvadd (pc s t) #x01)))
+
+(define-fun exchange-step
+  ((s State) (t Index) (a Index) (r Index) (v Word)) State
+  (advance (exchange s t a r v) t (bvadd (pc s t) #x01)))
+
+(define-fun overlap ((s State)) Bool
+  (and (= (at (critical s) #x00) #x01)
+       (= (at (critical s) #x01) #x01)))

@@ 1,208 @@
+type value = Bits of int64 | Truth of bool
+type answer = Sat of value list | Unsat | Unknown of string
+type query = { source : string; probes : (string * string) list }
+
+let strategy = "(check-sat-using (then simplify solve-eqs bit-blast sat))"
+let bits = function Bits value -> value | _ -> invalid_arg "expected bitvector"
+let truth = function Truth value -> value | _ -> invalid_arg "expected boolean"
+let index value = Printf.sprintf "#x%02x" value
+let word value = Printf.sprintf "#x%016Lx" value
+let all = function [] -> "true" | values -> "(and " ^ String.concat " " values ^ ")"
+let any = function [] -> "false" | values -> "(or " ^ String.concat " " values ^ ")"
+let equal_state left right = all (List.map (fun field ->
+  Printf.sprintf "(= (%s %s) (%s %s))" field left field right)
+  ["memory"; "registers"; "counters"; "heads"; "tails"; "addresses"; "values"; "positions"; "critical"])
+
+let command source =
+  if String.starts_with ~prefix:"(set-logic QF_BV)" source then strategy else "(check-sat)"
+
+let connection ~timeout ~tick action =
+  let input_read, input_write = Unix.pipe ~cloexec:true () in
+  let output_read, output_write = Unix.pipe ~cloexec:true () in
+  let executable = Option.value (Sys.getenv_opt "Z3") ~default:"z3" in
+  let pid = Unix.create_process executable [|executable; "-in"; "-smt2"|]
+    input_read output_write output_write in
+  Unix.close input_read;
+  Unix.close output_write;
+  let input = Unix.out_channel_of_descr input_write in
+  let pending = ref "" in
+  let deadline = Unix.gettimeofday () +. float_of_int timeout /. 1000. +. 30. in
+  let chunk = Bytes.create 8192 in
+  let read () =
+    if Unix.gettimeofday () > deadline then failwith "solver transport timed out";
+    tick ();
+    let ready, _, _ = Unix.select [output_read] [] [] 0.1 in
+    if ready = [] then None else
+    let size = Unix.read output_read chunk 0 (Bytes.length chunk) in
+    if size = 0 then Some "" else Some (Bytes.sub_string chunk 0 size)
+  in
+  let rec line () = match String.index_opt !pending '\n' with
+    | Some ending ->
+        let result = String.sub !pending 0 ending in
+        pending := String.sub !pending (ending + 1) (String.length !pending - ending - 1);
+        result
+    | None -> match read () with
+        | None -> line ()
+        | Some "" -> failwith ("solver closed its output: " ^ !pending)
+        | Some text -> pending := !pending ^ text; line ()
+  in
+  let finish () =
+    let buffer = Buffer.create 4096 in
+    Buffer.add_string buffer !pending;
+    pending := "";
+    let rec loop () = match read () with
+      | None -> loop ()
+      | Some "" -> Buffer.contents buffer
+      | Some text -> Buffer.add_string buffer text; loop ()
+    in
+    loop ()
+  in
+  let reaped = ref false in
+  Fun.protect ~finally:(fun () ->
+    close_out_noerr input;
+    Unix.close output_read;
+    if not !reaped then begin
+      (try Unix.kill pid Sys.sigkill with Unix.Unix_error (Unix.ESRCH, _, _) -> ());
+      ignore (Unix.waitpid [] pid)
+    end) (fun () ->
+      let result = action input line finish in
+      let _, status = Unix.waitpid [] pid in
+      reaped := true;
+      if status <> Unix.WEXITED 0 then failwith "solver process failed";
+      result)
+
+let script ?(timeout=300000) ?(tick=fun () -> ()) source =
+  connection ~timeout ~tick (fun input _ finish ->
+    output_string input (source ^ "\n(exit)\n");
+    flush input;
+    finish ())
+
+let solve ?(timeout=300000) ?(tick=fun () -> ()) query =
+  connection ~timeout ~tick (fun input line finish ->
+    output_string input query.source;
+    List.iteri (fun i (kind, term) ->
+      Printf.fprintf input "(define-fun q%d () %s %s)\n" i kind term) query.probes;
+    output_string input (command query.source ^ "\n");
+    flush input;
+    let status = String.trim (line ()) in
+    begin match status with
+    | "sat" when query.probes <> [] ->
+        let names = List.init (List.length query.probes) (Printf.sprintf "q%d") in
+        Printf.fprintf input "(get-value (%s))\n" (String.concat " " names)
+    | "unknown" -> output_string input "(get-info :reason-unknown)\n"
+    | "sat" | "unsat" -> ()
+    | _ -> failwith ("invalid solver response: " ^ status)
+    end;
+    output_string input "(exit)\n";
+    flush input;
+    let response = finish () in
+    match status with
+    | "unsat" -> Unsat
+    | "unknown" -> Unknown response
+    | _ when query.probes = [] -> Sat []
+    | _ ->
+        let entries = Sexp.list (Sexp.one response) in
+        let table = Hashtbl.create (List.length entries) in
+        List.iter (function
+          | Sexp.List [Sexp.Atom name; value] ->
+              let value = match value with
+                | Sexp.Atom "true" -> Truth true
+                | Sexp.Atom "false" -> Truth false
+                | value -> Bits (Sexp.word value) in
+              Hashtbl.add table name value
+          | _ -> failwith "invalid model entry") entries;
+        Sat (List.init (List.length query.probes) (fun i -> Hashtbl.find table (Printf.sprintf "q%d" i))))
+
+let instruction state t =
+  let open Syntax in
+  let call name values = Printf.sprintf "(%s-step %s %s%s)" name state (index t)
+    (if values = [] then "" else " " ^ String.concat " " values) in
+  function
+  | Store (a, v) -> [Printf.sprintf "(bvult (pending %s %s) #x08)" state (index t)],
+      (fun sc -> call "store" [index a; word v; string_of_bool sc])
+  | Load (a, r) -> [], (fun _ -> call "load" [index a; index r])
+  | Fence -> [Printf.sprintf "(= (pending %s %s) #x00)" state (index t)],
+      (fun _ -> call "fence" [])
+  | Move (r, v) -> [], (fun _ -> call "move" [index r; word v])
+  | Branch (r, v, pc) -> [], (fun _ -> call "branch" [index r; word v; index pc])
+  | Enter -> [], (fun _ -> call "enter" [])
+  | Leave -> [], (fun _ -> call "leave" [])
+  | Exchange (a, r, v) -> [Printf.sprintf "(= (pending %s %s) #x00)" state (index t)],
+      (fun _ -> call "exchange" [index a; index r; word v])
+
+let property (case : Syntax.t) state =
+  match case.goal with
+  | Syntax.Overlap -> Printf.sprintf "(overlap %s)" state
+  | Syntax.Outcome goal ->
+      let finished = List.init 2 (fun t -> Printf.sprintf "(= (pc %s %s) %s)"
+        state (index t) (index (Array.length case.threads.(t)))) in
+      let registers = List.map (fun (t, r, v) -> Printf.sprintf "(= (reg %s %s %s) %s)"
+        state (index t) (index r) (word v)) goal.registers in
+      let memory = List.map (fun (a, v) -> Printf.sprintf "(= (at (memory %s) %s) %s)"
+        state (index a) (word v)) goal.memory in
+      let drained = if not goal.drained then [] else List.init 2 (fun t ->
+        Printf.sprintf "(= (pending %s %s) #x00)" state (index t)) in
+      all (finished @ registers @ memory @ drained)
+
+let observations (case : Syntax.t) state =
+  List.init 2 (fun t -> "Index", Printf.sprintf "(pc %s %s)" state (index t)) @
+  List.init 8 (fun i -> "Word", Printf.sprintf "(reg %s %s %s)" state (index (i / 4)) (index (i mod 4))) @
+  List.init (Array.length case.names) (fun a -> "Word", Printf.sprintf "(at (memory %s) %s)" state (index a)) @
+  List.init 2 (fun t -> "Index", Printf.sprintf "(pending %s %s)" state (index t)) @
+  List.init 2 (fun t -> "Index", Printf.sprintf "(at (critical %s) %s)" state (index t))
+
+let compile ?(timeout=300000) ?fixed ?(require_goal=true) ?(blocks=[]) case model fences bound =
+  Syntax.validate case;
+  if bound < 1 || bound > 64 then invalid_arg "step bound outside 1..64";
+  List.iter (fun (t, pc) ->
+    if t < 0 || t > 1 || pc < 0 || pc >= Array.length case.Syntax.threads.(t)
+    then invalid_arg "invalid fence location") fences;
+  Option.iter (fun actors ->
+    if Array.length actors <> bound || Array.exists (fun a -> a < 0 || a > 4) actors
+    then invalid_arg "invalid fixed schedule") fixed;
+  let buffer = Buffer.create 65536 in
+  Buffer.add_string buffer (Layout.generate ~timeout);
+  Buffer.add_string buffer (Store.read (Filename.concat (Store.root ()) "smt/machine.smt2"));
+  let add line = Buffer.add_string buffer (line ^ "\n") in
+  add ("(declare-const s0 State)\n(assert " ^ equal_state "s0" "initial" ^ ")");
+  for step = 0 to bound - 1 do
+    let state = Printf.sprintf "s%d" step in
+    let next = Printf.sprintf "s%d" (step + 1) in
+    let actor = Printf.sprintf "a%d" step in
+    add (Printf.sprintf "(declare-const %s State)\n(declare-const %s Index)" next actor);
+    let alternatives = List.concat (List.init 2 (fun t ->
+      let instructions = Array.to_list (Array.mapi (fun pc ins ->
+        let guards, call = instruction state t ins in
+        let guards = if List.mem (t, pc) fences then
+          Printf.sprintf "(= (pending %s %s) #x00)" state (index t) :: guards else guards in
+        all (Printf.sprintf "(= (pc %s %s) %s)" state (index t) (index pc) ::
+          equal_state next (call (model = Syntax.Sc)) :: guards)) case.threads.(t)) in
+      [all [Printf.sprintf "(= %s %s)" actor (index t); any instructions];
+       all [Printf.sprintf "(= %s %s)" actor (index (t + 2));
+         Printf.sprintf "(bvugt (pending %s %s) #x00)" state (index t);
+         equal_state next (Printf.sprintf "(drain %s %s)" state (index t))]])) in
+    add ("(assert " ^ any (alternatives @ [all ["(= " ^ actor ^ " #x04)"; equal_state next state]]) ^ ")");
+    if step > 0 && fixed = None then
+      add (Printf.sprintf "(assert (=> (= %s #x04) (= a%d #x04)))" actor (step - 1));
+    Option.iter (fun actors -> add (Printf.sprintf "(assert (= %s %s))" actor (index actors.(step)))) fixed
+  done;
+  let final = Printf.sprintf "s%d" bound in
+  if require_goal then add ("(assert " ^ property case final ^ ")");
+  List.iter (fun (left, right) -> add ("(assert " ^ any [
+    Printf.sprintf "(distinct (reg %s #x00 #x00) %s)" final (word left);
+    Printf.sprintf "(distinct (reg %s #x01 #x00) %s)" final (word right)] ^ ")")) blocks;
+  let probes = List.init bound (fun i -> "Index", Printf.sprintf "a%d" i) @
+    List.concat (List.init (bound + 1) (fun i -> observations case (Printf.sprintf "s%d" i))) in
+  {source = Buffer.contents buffer; probes}
+
+let candidate ~count ~budget clauses =
+  let lines = ref [Store.read (Filename.concat (Store.root ()) "smt/fences.smt2")] in
+  let add line = lines := line :: !lines in
+  for i = 0 to count - 1 do add (Printf.sprintf "(declare-const f%d Bool)" i) done;
+  let weights = List.init count (Printf.sprintf "(weight f%d)") in
+  add (Printf.sprintf "(assert (<= (+ 0 %s) %d))" (String.concat " " weights) budget);
+  List.iter (fun clause -> add ("(assert " ^ any (List.map (Printf.sprintf "f%d") clause) ^ ")")) clauses;
+  {source = String.concat "\n" (List.rev !lines) ^ "\n";
+   probes = List.init count (fun i -> "Bool", Printf.sprintf "f%d" i)}
+
+let standalone query = query.source ^ command query.source ^ "\n"

@@ 1,12 @@
+type value = Bits of int64 | Truth of bool
+type answer = Sat of value list | Unsat | Unknown of string
+type query = { source : string; probes : (string * string) list }
+val strategy : string
+val solve : ?timeout:int -> ?tick:(unit -> unit) -> query -> answer
+val script : ?timeout:int -> ?tick:(unit -> unit) -> string -> string
+val compile : ?timeout:int -> ?fixed:int array -> ?require_goal:bool ->
+  ?blocks:(int64 * int64) list -> Syntax.t -> Syntax.model -> Syntax.location list -> int -> query
+val candidate : count:int -> budget:int -> int list list -> query
+val standalone : query -> string
+val bits : value -> int64
+val truth : value -> bool

@@ 1,32 @@
+let read path =
+  let channel = open_in_bin path in
+  Fun.protect ~finally:(fun () -> close_in_noerr channel) (fun () ->
+    really_input_string channel (in_channel_length channel))
+
+let rec mkdir path =
+  if path <> "." && not (Sys.file_exists path) then begin
+    mkdir (Filename.dirname path);
+    Unix.mkdir path 0o755
+  end
+
+let write path text =
+  mkdir (Filename.dirname path);
+  let channel = open_out_bin path in
+  Fun.protect ~finally:(fun () -> close_out_noerr channel) (fun () ->
+    output_string channel text)
+
+let root () =
+  let rec find path =
+    if Sys.file_exists (Filename.concat path "smt/machine.smt2") then path
+    else
+      let parent = Filename.dirname path in
+      if parent = path then invalid_arg "cannot locate smt/machine.smt2"
+      else find parent
+  in
+  match Sys.getenv_opt "REORDER_ROOT" with
+  | Some path -> find path
+  | None ->
+      try find (Sys.getcwd ()) with Invalid_argument _ ->
+        let executable = if Filename.is_relative Sys.executable_name then
+          Filename.concat (Sys.getcwd ()) Sys.executable_name else Sys.executable_name in
+        find (Filename.dirname executable)

@@ 1,4 @@
+val read : string -> string
+val write : string -> string -> unit
+val mkdir : string -> unit
+val root : unit -> string

@@ 1,132 @@
+type instruction =
+  | Store of int * int64 | Load of int * int | Fence
+  | Move of int * int64 | Branch of int * int64 * int
+  | Enter | Leave | Exchange of int * int * int64
+
+type goal = Overlap | Outcome of {
+  registers : (int * int * int64) list;
+  memory : (int * int64) list;
+  drained : bool;
+}
+
+type model = Sc | Tso
+type location = int * int
+type t = {
+  name : string;
+  names : string array;
+  bound : int;
+  threads : instruction array array;
+  candidates : location list;
+  goal : goal;
+}
+
+let model = function "sc" -> Sc | "tso" -> Tso | _ -> invalid_arg "unknown memory model"
+let model_name = function Sc -> "sc" | Tso -> "tso"
+let location value = match Sexp.list value with
+  | [t; pc] -> Sexp.integer t, Sexp.integer pc
+  | _ -> invalid_arg "invalid fence location"
+
+let instruction value =
+  let open Sexp in
+  match value with
+  | Store (a, v) -> List [Atom "store"; i a; w v]
+  | Load (a, r) -> List [Atom "load"; i a; i r]
+  | Fence -> List [Atom "fence"]
+  | Move (r, v) -> List [Atom "move"; i r; w v]
+  | Branch (r, v, target) -> List [Atom "branch"; i r; w v; i target]
+  | Enter -> List [Atom "enter"]
+  | Leave -> List [Atom "leave"]
+  | Exchange (a, r, v) -> List [Atom "exchange"; i a; i r; w v]
+
+let decode_instruction value =
+  let open Sexp in
+  match list value with
+  | [Atom "store"; a; v] -> Store (integer a, word v)
+  | [Atom "load"; a; r] -> Load (integer a, integer r)
+  | [Atom "fence"] -> Fence
+  | [Atom "move"; r; v] -> Move (integer r, word v)
+  | [Atom "branch"; r; v; target] -> Branch (integer r, word v, integer target)
+  | [Atom "enter"] -> Enter
+  | [Atom "leave"] -> Leave
+  | [Atom "exchange"; a; r; v] -> Exchange (integer a, integer r, word v)
+  | _ -> invalid_arg "invalid instruction"
+
+let validate case =
+  let check condition message = if not condition then invalid_arg message in
+  check (Array.length case.threads = 2) "exactly two threads required";
+  check (Array.length case.names > 0 && Array.length case.names <= 16) "address count outside 1..16";
+  check (case.bound > 0 && case.bound <= 64) "step bound outside 1..64";
+  let address a = check (a >= 0 && a < Array.length case.names) "address outside model" in
+  let register r = check (r >= 0 && r < 4) "register outside model" in
+  Array.iter (fun program ->
+    check (Array.length program > 0 && Array.length program <= 64) "thread length outside 1..64";
+    Array.iter (function
+      | Store (a, _) -> address a
+      | Load (a, r) | Exchange (a, r, _) -> address a; register r
+      | Move (r, _) -> register r
+      | Branch (r, _, target) -> register r;
+          check (target >= 0 && target <= Array.length program) "branch target outside thread"
+      | Fence | Enter | Leave -> ()) program) case.threads;
+  let thread t = check (t >= 0 && t < 2) "thread outside model" in
+  List.iter (fun (t, pc) -> thread t;
+    check (pc >= 0 && pc < Array.length case.threads.(t)) "fence outside thread") case.candidates;
+  check (List.length case.candidates = List.length (List.sort_uniq compare case.candidates)) "duplicate fence";
+  match case.goal with
+  | Overlap -> ()
+  | Outcome goal ->
+      List.iter (fun (t, r, _) -> thread t; register r) goal.registers;
+      List.iter (fun (a, _) -> address a) goal.memory
+
+let singleton = function [value] -> value | _ -> invalid_arg "expected one field value"
+
+let decode value =
+  let open Sexp in
+  let fields = match value with
+    | List (Atom "case" :: fields) -> fields
+    | _ -> invalid_arg "expected case"
+  in
+  let get key = singleton (field key fields) in
+  let goal = match field "goal" fields with
+    | [Atom "overlap"] -> Overlap
+    | [List (Atom "outcome" :: fields)] ->
+        let registers = List.map (fun value -> match list value with
+          | [t; r; v] -> integer t, integer r, word v
+          | _ -> invalid_arg "invalid register goal") (field "registers" fields) in
+        let memory = List.map (fun value -> match list value with
+          | [a; v] -> integer a, word v
+          | _ -> invalid_arg "invalid memory goal") (field "memory" fields) in
+        let drained = match field "drained" fields with
+          | [Atom "true"] -> true | [Atom "false"] -> false
+          | _ -> invalid_arg "invalid drain flag" in
+        Outcome {registers; memory; drained}
+    | _ -> invalid_arg "invalid goal"
+  in
+  let case = {
+    name = atom (get "name");
+    names = Array.of_list (List.map atom (field "names" fields));
+    bound = integer (get "bound");
+    threads = Array.of_list (List.map (fun thread ->
+      Array.of_list (List.map decode_instruction (list thread))) (field "threads" fields));
+    candidates = List.map location (field "candidates" fields);
+    goal;
+  } in
+  validate case;
+  case
+
+let encode case =
+  let open Sexp in
+  let goal = match case.goal with
+    | Overlap -> Atom "overlap"
+    | Outcome goal -> List [Atom "outcome";
+        List (Atom "registers" :: List.map (fun (t, r, v) -> List [i t; i r; w v]) goal.registers);
+        List (Atom "memory" :: List.map (fun (a, v) -> List [i a; w v]) goal.memory);
+        List [Atom "drained"; Atom (string_of_bool goal.drained)]] in
+  List [Atom "case"; List [Atom "name"; Atom case.name];
+    List (Atom "names" :: Array.to_list (Array.map a case.names));
+    List [Atom "bound"; i case.bound];
+    List (Atom "threads" :: Array.to_list (Array.map (fun thread ->
+      List (Array.to_list (Array.map instruction thread))) case.threads));
+    List (Atom "candidates" :: List.map (fun (t, pc) -> List [i t; i pc]) case.candidates);
+    List [Atom "goal"; goal]]
+
+let load path = decode (Sexp.one (Store.read path))

@@ 1,30 @@
+type instruction =
+  | Store of int * int64 | Load of int * int | Fence
+  | Move of int * int64 | Branch of int * int64 * int
+  | Enter | Leave | Exchange of int * int * int64
+
+type goal = Overlap | Outcome of {
+  registers : (int * int * int64) list;
+  memory : (int * int64) list;
+  drained : bool;
+}
+
+type model = Sc | Tso
+type location = int * int
+type t = {
+  name : string;
+  names : string array;
+  bound : int;
+  threads : instruction array array;
+  candidates : location list;
+  goal : goal;
+}
+
+val validate : t -> unit
+val decode : Sexp.t -> t
+val encode : t -> Sexp.t
+val load : string -> t
+val instruction : instruction -> Sexp.t
+val location : Sexp.t -> location
+val model : string -> model
+val model_name : model -> string

@@ 1,19 @@
+{
+  "solver": "Z3",
+  "version": "5.1.0",
+  "language": "SMT-LIB 2",
+  "basis": "https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf",
+  "semantics": "two threads, atomic 64-bit cells, FIFO store buffers, local forwarding, mfence and atomic exchange",
+  "bounds": {
+    "threads": 2,
+    "registers": 4,
+    "buffer": 8,
+    "steps": 64
+  },
+  "ocaml": "5.5.0",
+  "dune": "3.24.2",
+  "driver": "OCaml",
+  "solver_strategy": "simplify, solve-eqs, bit-blast, sat",
+  "timeout_ms": 300000,
+  "repair": "counterexample-guided synthesis refined by complete finite execution graphs"
+}

@@ 1,319 @@
+type t = {
+  width : int;
+  delay : float;
+  animate : bool;
+  case : Syntax.t;
+  started : float;
+  mutable last_draw : float;
+  mutable last_rows : int;
+  mutable title : string;
+  mutable fences : Syntax.location list;
+  mutable budget : int;
+  mutable round : int;
+  mutable excluded : int list;
+}
+
+let headline text =
+  String.split_on_char ' ' text
+  |> List.map (fun word ->
+    match String.uppercase_ascii word with
+    | "SC" | "TSO" | "SMT" | "FIFO" | "CPU" as acronym -> acronym
+    | _ -> String.capitalize_ascii word)
+  |> String.concat " "
+
+let fit width text =
+  if String.length text <= width then text ^ String.make (width - String.length text) ' '
+  else String.sub text 0 (max 0 (width - 3)) ^ "..."
+let line width = String.make width '-'
+let columns width left right =
+  let size = (width - 3) / 2 in
+  let height = max (List.length left) (List.length right) in
+  List.init height (fun i ->
+    let at values = if i < List.length values then List.nth values i else "" in
+    fit size (at left) ^ " | " ^ fit size (at right))
+let label (case : Syntax.t) address = case.names.(address)
+let number value = if value >= 0L && value < 1000000L then Int64.to_string value
+  else Printf.sprintf "0x%016Lx" value
+
+let instruction (case : Syntax.t) =
+  let open Syntax in
+  function
+  | Store (a, v) -> Printf.sprintf "mov [%s], %s" (label case a) (number v)
+  | Load (a, r) -> Printf.sprintf "mov r%d, [%s]" r (label case a)
+  | Fence -> "mfence"
+  | Move (r, v) -> Printf.sprintf "mov r%d, %s" r (number v)
+  | Branch (r, v, target) -> Printf.sprintf "if r%d == %s goto %02d" r (number v) target
+  | Enter -> "enter critical section"
+  | Leave -> "leave critical section"
+  | Exchange (a, r, v) -> Printf.sprintf "xchg [%s], %s -> r%d" (label case a) (number v) r
+
+let registers state t = String.concat "   " (List.init 4 (fun r ->
+  Printf.sprintf "r%d=%s" r (number state.Machine.regs.(t).(r))))
+let queue case entries = match entries with
+  | [] -> "[ empty ]"
+  | entries -> String.concat " -> " (List.map (fun (a, v) ->
+      Printf.sprintf "[ %s=%s ]" (label case a) (number v)) entries)
+let memory case state = String.concat "     " (List.init (Array.length case.Syntax.names) (fun a ->
+  Printf.sprintf "[ %s = %s ]" (label case a) (number state.Machine.memory.(a))))
+
+let program case fences state t =
+  let pc = state.Machine.pc.(t) in
+  let active = if state.critical.(t) then "   Inside Critical Section" else "" in
+  let head = [Printf.sprintf "Thread %d   pc=%02d%s" t pc active; registers state t; ""] in
+  let code = case.Syntax.threads.(t) in
+  let first = max 0 (min (pc - 3) (Array.length code - 9)) in
+  head @ List.concat (List.init (min 9 (Array.length code)) (fun offset ->
+    let i = first + offset in
+    let fence = if not (List.mem (t, i) fences) then [] else
+      [Printf.sprintf "     mfence%s" (if i = pc && state.buffers.(t) <> [] then "  < waiting for store buffer" else "")] in
+    fence @ [Printf.sprintf "%s %02d  %s" (if i = pc then ">" else " ") i (instruction case code.(i))])) @
+  [""; "FIFO Store Buffer   oldest -> newest"; queue case state.buffers.(t)]
+
+let event case before after = function
+  | Machine.Idle -> "scheduler idle"
+  | Machine.Drain (t, a, v) ->
+      Printf.sprintf "T%d drains %s=%s from its FIFO buffer into shared memory" t (label case a) (number v)
+  | Machine.Issue (t, _, Syntax.Load (a, r), Some origin) ->
+      let source = match origin with Machine.Memory -> "shared memory" | Machine.Buffer -> "its latest buffered write" in
+      let stale = List.exists (fun (address, _) -> address = a) before.Machine.buffers.(1 - t) in
+      Printf.sprintf "T%d reads %s=%s into r%d from %s%s" t (label case a)
+        (number after.Machine.regs.(t).(r)) r source
+        (if stale && origin = Machine.Memory then " while the other thread has a pending write" else "")
+  | Machine.Issue (t, pc, ins, _) ->
+      Printf.sprintf "T%d issues pc=%02d  %s" t pc (instruction case ins)
+
+let timeline actors count =
+  let first = max 0 (count - 24) in
+  let cells = List.init (count - first) (fun i ->
+    let actor = actors.(first + i) in
+    match actor with 0 -> "T0" | 1 -> "T1" | 2 -> "F0" | 3 -> "F1" | _ -> "..") in
+  ["Schedule    T=Instruction    F=FIFO Drain";
+   String.concat " " (List.init (count - first) (fun i -> Printf.sprintf "%02d" (first + i + 1)));
+   String.concat " " cells]
+
+let frame ~width (witness : Engine.witness) index =
+  let states, events = Engine.replay witness in
+  if index < 0 || index >= Array.length states then invalid_arg "trace frame outside execution";
+  let state = states.(index) in
+  let status = if state.critical.(0) && state.critical.(1) then "Mutual Exclusion Violated"
+    else if index = witness.bound then "Requested Outcome Reached" else "Execution in Progress" in
+  let description = if index = 0 then "All registers, memory cells and store buffers start empty"
+    else event witness.case states.(index - 1) state events.(index - 1) in
+  let heading = ["Reorder    " ^ headline witness.case.name;
+    Printf.sprintf "model=%s   transition=%02d/%02d   bound=%d   independent replay=passed"
+      (Syntax.model_name witness.model) index witness.bound witness.bound;
+    line width; status; ""] in
+  heading @ columns width (program witness.case witness.fences state 0) (program witness.case witness.fences state 1) @
+  [""; line width; "Shared Memory"; memory witness.case state; "";
+   "Current Transition"; description; ""] @ timeline witness.actors index
+
+let colour text =
+  let paint code text = "\027[" ^ code ^ "m" ^ text ^ "\027[0m" in
+  let code =
+    if String.contains text '>' && String.starts_with ~prefix:">" (String.trim text) then "1;34"
+    else if String.starts_with ~prefix:"Mutual Exclusion Violated" text then "1;31"
+    else if String.starts_with ~prefix:"Minimum Repair Verified" text then "1;32"
+    else if String.starts_with ~prefix:"Thread 0" text then "1;34"
+    else if String.starts_with ~prefix:"Thread 1" text then "1;35"
+    else if String.starts_with ~prefix:"Reorder" text then "1" else "30" in
+  match String.index_opt text '|' with
+  | None -> paint code text
+  | Some middle ->
+      let left = String.sub text 0 middle in
+      let right = String.sub text (middle + 1) (String.length text - middle - 1) in
+      paint "34" left ^ paint "30" "|" ^ paint "35" right
+
+let draw view lines =
+  let buffer = Buffer.create 16384 in
+  let write text =
+    let text = fit view.width text in
+    let last = ref (String.length text) in
+    while !last > 0 && text.[!last - 1] = ' ' do decr last done;
+    Buffer.add_string buffer (if view.animate then colour text else String.sub text 0 !last)
+  in
+  if view.animate then begin
+    let rows = Array.of_list lines in
+    for row = 0 to max view.last_rows (Array.length rows) - 1 do
+      Printf.bprintf buffer "\027[%d;1H\027[2K" (row + 1);
+      if row < Array.length rows then write rows.(row)
+    done;
+    Buffer.add_string buffer "\027[1;1H"
+  end else
+    List.iter (fun text -> write text; Buffer.add_char buffer '\n') lines;
+  output_string stdout (Buffer.contents buffer);
+  flush stdout;
+  view.last_rows <- List.length lines;
+  view.last_draw <- Unix.gettimeofday ()
+
+let create ?(width=140) ?(delay=0.7) ~animate case =
+  if width < 78 || width > 180 || delay < 0. || delay > 10. then invalid_arg "invalid display dimensions or delay";
+  if animate then begin print_string "\027[2J\027[H\027[?25l"; flush stdout end;
+  {width; delay; animate; case; started=Unix.gettimeofday (); last_draw=0.; last_rows=0;
+   title="Preparing SMT query"; fences=[]; budget=0; round=0; excluded=[]}
+
+let tick view =
+  let now = Unix.gettimeofday () in
+  if view.animate && now -. view.last_draw >= 0.35 then begin
+    let state = Machine.initial view.case in
+    let selected = String.concat "   " (List.map (fun (t, pc) -> Printf.sprintf "T%d@%02d" t pc) view.fences) in
+    draw view (["Reorder    " ^ headline view.case.name; line view.width;
+      Printf.sprintf "%s   elapsed %.1fs" view.title (now -. view.started);
+      Printf.sprintf "verification round %d   fence budget %d   selected %s" view.round view.budget
+        (if selected = "" then "none" else selected);
+      ""] @ columns view.width (program view.case view.fences state 0) (program view.case view.fences state 1) @
+      [""; line view.width;
+       "Counterexample Constraints";
+       "Lower budgets excluded: " ^ String.concat ", " (List.map string_of_int view.excluded);
+       "SMT query running; elapsed time measures actual solver work"])
+  end
+
+let finish view =
+  if view.animate then begin
+    Printf.printf "\027[%d;1H\027[0m\027[?25h" (view.last_rows + 1);
+    flush stdout
+  end
+
+let phase view title =
+  view.title <- title;
+  view.last_draw <- 0.;
+  tick view
+
+let play view witness =
+  let _, events = Engine.replay witness in
+  for index = 0 to witness.Engine.bound do
+    if index = 0 || index = witness.bound || events.(index - 1) <> Machine.Idle then begin
+      draw view (frame ~width:view.width witness index);
+      if view.animate then Unix.sleepf view.delay
+    end
+  done
+
+let notify view = function
+  | Engine.Searching (budget, fences) ->
+      view.round <- view.round + 1;
+      view.budget <- budget;
+      view.fences <- fences;
+      view.title <- "Searching for a violating execution";
+      if view.animate then (view.last_draw <- 0.; tick view)
+      else Printf.printf "round %d  budget %d  fences %s\n%!" view.round budget
+        (String.concat ", " (List.map (fun (t, pc) -> Printf.sprintf "T%d@%d" t pc) fences))
+  | Engine.Counterexample witness ->
+      if view.animate then begin
+        let faster = {view with delay=min 0.18 view.delay} in
+        play faster witness;
+        view.last_rows <- faster.last_rows;
+        view.last_draw <- faster.last_draw
+      end else print_endline "SAT  counterexample replay checked"
+  | Engine.Excluded budget ->
+      view.excluded <- view.excluded @ [budget];
+      if not view.animate then Printf.printf "budget %d excluded\n%!" budget
+  | Engine.Refining bound ->
+      view.title <- Printf.sprintf "Graph counterexample extends the SMT bound to %d" bound;
+      if not view.animate then print_endline view.title
+  | Engine.Verified (fences, bound, states) ->
+      view.fences <- fences;
+      view.title <- "Minimum Repair Verified";
+      let state = Machine.initial view.case in
+      draw view (["Reorder    " ^ headline view.case.name; line view.width;
+        "Minimum Repair Verified";
+        Printf.sprintf "%d fences   bound %d   %d actual verification queries"
+          (List.length fences) bound view.round;
+        Printf.sprintf "Closed graph: %d reachable states, no violating state" states; ""] @
+        columns view.width (program view.case fences state 0) (program view.case fences state 1) @
+        [""; "Counterexample replay passed; lower-budget SMT certificate is UNSAT"])
+
+let compact case state =
+  [Printf.sprintf "T0 pc=%02d  %s" state.Machine.pc.(0)
+      (if state.critical.(0) then "Inside" else "Outside"); registers state 0;
+   "T0 buffer  " ^ queue case state.buffers.(0); "";
+   Printf.sprintf "T1 pc=%02d  %s" state.pc.(1)
+      (if state.critical.(1) then "Inside" else "Outside"); registers state 1;
+   "T1 buffer  " ^ queue case state.buffers.(1); ""; memory case state;
+   ""; if state.critical.(0) && state.critical.(1) then "Overlap" else "No overlap in this state"]
+
+let contrast view (witness : Engine.witness) (repair : Engine.repair) =
+  if witness.case <> repair.case then invalid_arg "comparison cases differ";
+  let original, _ = Engine.replay witness in
+  let fixed = Machine.reschedule witness.case repair.fences witness.actors in
+  Engine.validate_schedule witness.case repair.fences fixed;
+  let repaired, _ = Machine.replay witness.case Syntax.Tso repair.fences fixed in
+  for index = 0 to witness.bound do
+    if index = 0 || index = witness.bound || witness.actors.(index - 1) <> 4 then begin
+    let prefix = Machine.reschedule witness.case repair.fences (Array.sub witness.actors 0 index) in
+    let corrected = repaired.(Array.length prefix) in
+    let left = ["Original Execution"; line ((view.width - 3) / 2)] @ compact witness.case original.(index) in
+    let right = ["Minimum Fence Repair"; line ((view.width - 3) / 2)] @ compact witness.case corrected in
+    draw view (["Reorder    Original and Repaired Executions";
+      Printf.sprintf "requested transition %02d/%02d   pending writes drain before fenced instructions" index witness.bound;
+      line view.width; ""] @ columns view.width left right @
+      [""; line view.width;
+       "left: replayed solver counterexample   right: separately SMT-checked repaired execution";
+       Printf.sprintf "Minimum repair certificate: %d fences, UNSAT at bound %d"
+         (List.length repair.fences) repair.bound]);
+    if view.animate then Unix.sleepf view.delay
+    end
+  done
+
+let outcomes view sc tso =
+  let values = List.sort_uniq compare (sc @ tso) in
+  let rows = List.map (fun ((left, right) as pair) -> Printf.sprintf "%-12s%-12s%-12s%s"
+    (number left) (number right)
+    (if List.mem pair sc then "allowed" else "excluded")
+    (if List.mem pair tso then "allowed" else "excluded")) values in
+  let initial = Machine.initial view.case in
+  draw view (["Reorder    Sequential Consistency Versus TSO"; line view.width;
+    "Register Outcome Enumeration Complete"; ""] @
+    columns view.width (program view.case [] initial 0) (program view.case [] initial 1) @
+    [""; line view.width; "Each row is a distinct pair of final register values";
+     "T0:r0       T1:r0       SC          TSO"] @ rows)
+
+let graph view fences =
+  if view.case.goal <> Syntax.Overlap then invalid_arg "graph view requires a mutual-exclusion property";
+  let rows = Array.length view.case.threads.(0) + 1 in
+  let cols = Array.length view.case.threads.(1) + 1 in
+  let counts = Array.init rows (fun _ -> Array.make cols 0) in
+  let unsafe = Array.init rows (fun _ -> Array.make cols false) in
+  let occupancy = Array.make 4 0 in
+  let depths = Array.init 2 (fun _ -> Array.make 9 0) in
+  let render count complete edges violations =
+    let grid = ["PC0 vs PC1  " ^ String.concat "" (List.init cols (fun pc -> Printf.sprintf "%6d" pc))] @
+      List.init rows (fun row -> Printf.sprintf "%9d  " row ^
+        String.concat "" (List.init cols (fun col ->
+          if counts.(row).(col) = 0 then "     ."
+          else Printf.sprintf "%5d%s" counts.(row).(col) (if unsafe.(row).(col) then "!" else " ")))) in
+    let selected = String.concat ", " (List.map (fun (t, pc) -> Printf.sprintf "T%d@%02d" t pc) fences) in
+    let occupancy = [""; "Critical Section Occupancy"] @
+      List.mapi (fun i name -> Printf.sprintf "%-18s %5d states" name occupancy.(i))
+        ["Both Outside"; "T0 Inside"; "T1 Inside"; "Both Inside"] in
+    let queues = [""; "FIFO Depth       T0 States    T1 States"] @
+      List.init 9 (fun depth -> Printf.sprintf "%10d %12d %12d" depth depths.(0).(depth) depths.(1).(depth)) in
+    let programs = ["Fence Placement"] @
+      program view.case fences (Machine.initial view.case) 0 @ [""] @
+      program view.case fences (Machine.initial view.case) 1 in
+    draw view (["Reorder    Finite Execution State Exploration"; line view.width;
+      "Program Counter Occupancy   each cell counts distinct reachable machine states";
+      "! marks a cell containing a mutual-exclusion violation"; ""] @ columns view.width (grid @ occupancy @ queues) programs @
+      [""; line view.width;
+       (if complete then Printf.sprintf "Reachable states %d   transitions %d   violating states %d" count edges violations
+        else Printf.sprintf "Reachable states %d   transition totals available at graph closure" count);
+       "Fences: " ^ (if selected = "" then "none" else selected);
+       if complete then "State Graph Closed   every enabled successor is already represented"
+       else "Exploring actual enabled instruction and FIFO-drain transitions"])
+  in
+  let visit state count =
+    let row, col = state.Machine.pc.(0), state.pc.(1) in
+    counts.(row).(col) <- counts.(row).(col) + 1;
+    let active = (if state.critical.(0) then 1 else 0) + (if state.critical.(1) then 2 else 0) in
+    occupancy.(active) <- occupancy.(active) + 1;
+    for thread = 0 to 1 do
+      let depth = List.length state.buffers.(thread) in
+      depths.(thread).(depth) <- depths.(thread).(depth) + 1
+    done;
+    if state.critical.(0) && state.critical.(1) then unsafe.(row).(col) <- true;
+    if view.animate && count mod 25 = 0 then begin
+      render count false 0 0;
+      Unix.sleepf (min 0.12 view.delay)
+    end
+  in
+  let graph = Machine.explore ~visit view.case Syntax.Tso fences in
+  render (Array.length graph.states) true graph.edges (List.length graph.violations);
+  graph

@@ 1,12 @@
+type t
+val headline : string -> string
+val create : ?width:int -> ?delay:float -> animate:bool -> Syntax.t -> t
+val tick : t -> unit
+val notify : t -> Engine.phase -> unit
+val frame : width:int -> Engine.witness -> int -> string list
+val play : t -> Engine.witness -> unit
+val contrast : t -> Engine.witness -> Engine.repair -> unit
+val outcomes : t -> (int64 * int64) list -> (int64 * int64) list -> unit
+val finish : t -> unit
+val phase : t -> string -> unit
+val graph : t -> Syntax.location list -> Machine.graph