From 908ea7335d65c52f45e8387f6c42e462b25a624a Mon Sep 17 00:00:00 2001 From: james Date: Fri, 16 Oct 2026 14:37:18 +0100 Subject: [PATCH] feat(core): initialise tso checking and fence synthesis --- .gitignore | 2 + Makefile | 11 ++ cases/buffering.sexp | 11 ++ cases/fenced.sexp | 13 ++ cases/fifo.sexp | 11 ++ cases/forwarding.sexp | 11 ++ cases/peterson.sexp | 25 ++++ cases/spinlock.sexp | 17 +++ check.ml | 168 ++++++++++++++++++++++ dune | 17 +++ dune-project | 7 + engine.ml | 241 +++++++++++++++++++++++++++++++ engine.mli | 33 +++++ layout.ml | 53 +++++++ layout.mli | 1 + machine.ml | 183 ++++++++++++++++++++++++ machine.mli | 21 +++ main.ml | 130 +++++++++++++++++ reorder.opam | 23 +++ sexp.ml | 111 +++++++++++++++ sexp.mli | 12 ++ smt/fences.smt2 | 6 + smt/laws.smt2 | 98 +++++++++++++ smt/machine.smt2 | 88 ++++++++++++ solver.ml | 208 +++++++++++++++++++++++++++ solver.mli | 12 ++ store.ml | 32 +++++ store.mli | 4 + syntax.ml | 132 +++++++++++++++++ syntax.mli | 30 ++++ toolchain.json | 19 +++ view.ml | 319 ++++++++++++++++++++++++++++++++++++++++++ view.mli | 12 ++ 33 files changed, 2061 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 cases/buffering.sexp create mode 100644 cases/fenced.sexp create mode 100644 cases/fifo.sexp create mode 100644 cases/forwarding.sexp create mode 100644 cases/peterson.sexp create mode 100644 cases/spinlock.sexp create mode 100644 check.ml create mode 100644 dune create mode 100644 dune-project create mode 100644 engine.ml create mode 100644 engine.mli create mode 100644 layout.ml create mode 100644 layout.mli create mode 100644 machine.ml create mode 100644 machine.mli create mode 100644 main.ml create mode 100644 reorder.opam create mode 100644 sexp.ml create mode 100644 sexp.mli create mode 100644 smt/fences.smt2 create mode 100644 smt/laws.smt2 create mode 100644 smt/machine.smt2 create mode 100644 solver.ml create mode 100644 solver.mli create mode 100644 store.ml create mode 100644 store.mli create mode 100644 syntax.ml create mode 100644 syntax.mli create mode 100644 toolchain.json create mode 100644 view.ml create mode 100644 view.mli diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..2907da99f574830698d3d814cf5b132f54c7db7e --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +_build/ +build/ diff --git a/Makefile b/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..d34ef23f506c55f8d70f68d4180242d63a60771a --- /dev/null +++ b/Makefile @@ -0,0 +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 diff --git a/cases/buffering.sexp b/cases/buffering.sexp new file mode 100644 index 0000000000000000000000000000000000000000..a3e2729799bee8a13a8097e1c28aeec76e78b5c2 --- /dev/null +++ b/cases/buffering.sexp @@ -0,0 +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)))) diff --git a/cases/fenced.sexp b/cases/fenced.sexp new file mode 100644 index 0000000000000000000000000000000000000000..125eef50d2358d866d8082b563d172207413f5f5 --- /dev/null +++ b/cases/fenced.sexp @@ -0,0 +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)))) diff --git a/cases/fifo.sexp b/cases/fifo.sexp new file mode 100644 index 0000000000000000000000000000000000000000..96fa296fb13c00bd8afc4d63e1ea3a72fd8050b9 --- /dev/null +++ b/cases/fifo.sexp @@ -0,0 +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)))) diff --git a/cases/forwarding.sexp b/cases/forwarding.sexp new file mode 100644 index 0000000000000000000000000000000000000000..6305e1839efa2ed67ec1db263bc992babd71c7dd --- /dev/null +++ b/cases/forwarding.sexp @@ -0,0 +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)))) diff --git a/cases/peterson.sexp b/cases/peterson.sexp new file mode 100644 index 0000000000000000000000000000000000000000..f3d9ceb471cab66bc207296ee559654bd3d68660 --- /dev/null +++ b/cases/peterson.sexp @@ -0,0 +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)) diff --git a/cases/spinlock.sexp b/cases/spinlock.sexp new file mode 100644 index 0000000000000000000000000000000000000000..1788637daa9e4483b9c35cce71443e2ebdb60d2f --- /dev/null +++ b/cases/spinlock.sexp @@ -0,0 +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)) diff --git a/check.ml b/check.ml new file mode 100644 index 0000000000000000000000000000000000000000..d38de023c4a6332e5304710d68b5c76e643da88b --- /dev/null +++ b/check.ml @@ -0,0 +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) diff --git a/dune b/dune new file mode 100644 index 0000000000000000000000000000000000000000..388d9d4f06a3c9bf8dfbba1941f0a47c99d9a549 --- /dev/null +++ b/dune @@ -0,0 +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))) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..723c1b4214c5e049de74a27294e944f35e0ff478 --- /dev/null +++ b/dune-project @@ -0,0 +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)))) diff --git a/engine.ml b/engine.ml new file mode 100644 index 0000000000000000000000000000000000000000..63bbd4ae04b60c84ef27df193f51ea060b9a06a2 --- /dev/null +++ b/engine.ml @@ -0,0 +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 [] diff --git a/engine.mli b/engine.mli new file mode 100644 index 0000000000000000000000000000000000000000..382b46b4c204ddf56bcd25d52b10d0722e5cb38a --- /dev/null +++ b/engine.mli @@ -0,0 +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 diff --git a/layout.ml b/layout.ml new file mode 100644 index 0000000000000000000000000000000000000000..5d921a0f68ed8de21e61c6a9dc8a9018c0f5fb84 --- /dev/null +++ b/layout.ml @@ -0,0 +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" diff --git a/layout.mli b/layout.mli new file mode 100644 index 0000000000000000000000000000000000000000..fb036af78f2e2e8e8b74135253793caaa6b51704 --- /dev/null +++ b/layout.mli @@ -0,0 +1 @@ +val generate : timeout:int -> string diff --git a/machine.ml b/machine.ml new file mode 100644 index 0000000000000000000000000000000000000000..9bff03be5590e3af68f9a48787548b4778ee51ec --- /dev/null +++ b/machine.ml @@ -0,0 +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 []) diff --git a/machine.mli b/machine.mli new file mode 100644 index 0000000000000000000000000000000000000000..5bb3cbd375ad9544eeba30935f8faa9d8198e001 --- /dev/null +++ b/machine.mli @@ -0,0 +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 diff --git a/main.ml b/main.ml new file mode 100644 index 0000000000000000000000000000000000000000..f2ab3f9c37f6ff074336cf31d61589cdae2d7f6e --- /dev/null +++ b/main.ml @@ -0,0 +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 diff --git a/reorder.opam b/reorder.opam new file mode 100644 index 0000000000000000000000000000000000000000..724d545012dea03c87087367b29017e73ce3fcc9 --- /dev/null +++ b/reorder.opam @@ -0,0 +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)"] diff --git a/sexp.ml b/sexp.ml new file mode 100644 index 0000000000000000000000000000000000000000..ee05bc2d999820b1fe6aaa60a6e24c7e09cdc110 --- /dev/null +++ b/sexp.ml @@ -0,0 +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) diff --git a/sexp.mli b/sexp.mli new file mode 100644 index 0000000000000000000000000000000000000000..c22d5e6eebff260196771ecb650eb16b57268412 --- /dev/null +++ b/sexp.mli @@ -0,0 +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 diff --git a/smt/fences.smt2 b/smt/fences.smt2 new file mode 100644 index 0000000000000000000000000000000000000000..1e9b514c13081ec41beccf87fcf5f031ee7241ce --- /dev/null +++ b/smt/fences.smt2 @@ -0,0 +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)) diff --git a/smt/laws.smt2 b/smt/laws.smt2 new file mode 100644 index 0000000000000000000000000000000000000000..3879b5300eefb395be9e311a0698dea1952a2b9a --- /dev/null +++ b/smt/laws.smt2 @@ -0,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) diff --git a/smt/machine.smt2 b/smt/machine.smt2 new file mode 100644 index 0000000000000000000000000000000000000000..8c98c47f47911d58f7913bcfabf268af8da9f610 --- /dev/null +++ b/smt/machine.smt2 @@ -0,0 +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))) diff --git a/solver.ml b/solver.ml new file mode 100644 index 0000000000000000000000000000000000000000..a2b7aee30707d075de1ea03f15b9bbab44e1af19 --- /dev/null +++ b/solver.ml @@ -0,0 +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" diff --git a/solver.mli b/solver.mli new file mode 100644 index 0000000000000000000000000000000000000000..a5031191075ee59f82dcf55bcccb797659ffebb6 --- /dev/null +++ b/solver.mli @@ -0,0 +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 diff --git a/store.ml b/store.ml new file mode 100644 index 0000000000000000000000000000000000000000..953a070d9bb48366bb83a4a7c25e5f95a0232bac --- /dev/null +++ b/store.ml @@ -0,0 +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) diff --git a/store.mli b/store.mli new file mode 100644 index 0000000000000000000000000000000000000000..261331b2ae840c5faea1cc2098c8f135df434598 --- /dev/null +++ b/store.mli @@ -0,0 +1,4 @@ +val read : string -> string +val write : string -> string -> unit +val mkdir : string -> unit +val root : unit -> string diff --git a/syntax.ml b/syntax.ml new file mode 100644 index 0000000000000000000000000000000000000000..e333e2e88a9beb21565295996907e3b845cac438 --- /dev/null +++ b/syntax.ml @@ -0,0 +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)) diff --git a/syntax.mli b/syntax.mli new file mode 100644 index 0000000000000000000000000000000000000000..f7fc557b542363934257e245634cb1f8311367c0 --- /dev/null +++ b/syntax.mli @@ -0,0 +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 diff --git a/toolchain.json b/toolchain.json new file mode 100644 index 0000000000000000000000000000000000000000..72639b9f6d8ee17c83172264114121a30f337634 --- /dev/null +++ b/toolchain.json @@ -0,0 +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" +} diff --git a/view.ml b/view.ml new file mode 100644 index 0000000000000000000000000000000000000000..d600093bc4421fdc2854a2d2d70b0e3ac83f9b8d --- /dev/null +++ b/view.ml @@ -0,0 +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 diff --git a/view.mli b/view.mli new file mode 100644 index 0000000000000000000000000000000000000000..5424c0bb3cb87d36afeca0c92360dcde424ec838 --- /dev/null +++ b/view.mli @@ -0,0 +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