255 lines
13 KiB
OCaml
255 lines
13 KiB
OCaml
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 storage folder =
|
|
let folder = Filename.concat folder "storage" in
|
|
let path = Filename.concat folder "nested/artefact" in
|
|
Store.write path "first";
|
|
let previous = open_in_bin path in
|
|
Fun.protect ~finally:(fun () -> close_in_noerr previous) (fun () ->
|
|
Store.write path "replacement";
|
|
require (Store.read path = "replacement") "artefact replacement";
|
|
require (really_input_string previous 5 = "first") "open reader retains previous artefact");
|
|
let target = Filename.concat folder "directory" in
|
|
Store.mkdir target;
|
|
let failed = try Store.write target "invalid"; false with Sys_error _ -> true in
|
|
require failed "directory cannot be replaced by an artefact";
|
|
require (Sys.is_directory target) "failed replacement preserves destination";
|
|
require (List.sort compare (Array.to_list (Sys.readdir folder)) = ["directory"; "nested"])
|
|
"failed replacement removes temporary file"
|
|
|
|
let transport folder =
|
|
let previous = Option.value (Sys.getenv_opt "Z3") ~default:"z3" in
|
|
let descriptors () = Array.length (Sys.readdir "/proc/self/fd") in
|
|
let before = descriptors () in
|
|
Fun.protect ~finally:(fun () -> Unix.putenv "Z3" previous) (fun () ->
|
|
Unix.putenv "Z3" (Filename.concat folder "missing");
|
|
for _ = 1 to 32 do
|
|
let failed = try ignore (Solver.script ""); false with
|
|
| Unix.Unix_error (Unix.ENOENT, _, _) -> true in
|
|
require failed "missing solver reports process creation failure"
|
|
done);
|
|
require (descriptors () = before) "failed solver spawn closes every pipe"
|
|
|
|
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 constraints () =
|
|
List.iter (fun (count, clauses) ->
|
|
rejects (fun () -> ignore (Solver.candidate ~count ~budget:1 clauses))
|
|
"invalid fence constraint")
|
|
[-1, []; 1, [[-1]]; 1, [[1]]; 0, [[0]]];
|
|
let solve count budget clauses = Solver.solve (Solver.candidate ~count ~budget clauses) in
|
|
require (solve 0 0 [] = Solver.Sat []) "empty candidate set satisfies zero budget";
|
|
require (solve 0 (-1) [] = Solver.Unsat) "negative lower budget remains unsatisfiable";
|
|
require (solve 2 0 [[0; 1]] = Solver.Unsat) "zero budget cannot hit a nonempty clause";
|
|
require (solve 2 1 [[0]; [1]] = Solver.Unsat) "independent singleton clauses require two fences";
|
|
require (solve 2 2 [[0]; [1]] = Solver.Sat [Solver.Truth true; Solver.Truth true])
|
|
"candidate values follow clause indices"
|
|
|
|
let validation () =
|
|
let case = read "buffering" in
|
|
let open Sexp in
|
|
let entries = List.tl (list (Syntax.encode case)) in
|
|
let decode entries = ignore (Syntax.decode (List (Atom "case" :: entries))) in
|
|
List.iter (fun extra ->
|
|
rejects (fun () -> decode (extra :: entries)) "unexpected case field")
|
|
[List [Atom "bounds"; i 8]; Atom "extra"; List []; List [List []]];
|
|
List.iter (fun extra ->
|
|
let entries = List.map (function
|
|
| List [Atom "goal"; List (Atom "outcome" :: goal)] ->
|
|
List [Atom "goal"; List (Atom "outcome" :: extra :: goal)]
|
|
| field -> field) entries in
|
|
rejects (fun () -> decode entries) "unexpected outcome field")
|
|
[List [Atom "drain"; Atom "true"]; Atom "extra"; List []];
|
|
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 cli folder =
|
|
let descriptor = Unix.openfile "/dev/null" [Unix.O_RDWR; Unix.O_CLOEXEC] 0 in
|
|
Fun.protect ~finally:(fun () -> Unix.close descriptor) (fun () ->
|
|
let run arguments =
|
|
let arguments = Array.of_list ("./src/main.exe" :: arguments) in
|
|
let pid = Unix.create_process "./src/main.exe" arguments descriptor descriptor descriptor in
|
|
snd (Unix.waitpid [] pid) in
|
|
List.iter (fun arguments ->
|
|
require (run arguments = Unix.WEXITED 2) "CLI rejects invalid input count")
|
|
[["layout"; "extra"]; ["laws"; "extra"];
|
|
["check"; "cases/buffering.sexp"; "extra"];
|
|
["graph"; "cases/buffering.sexp"; "a"; "b"];
|
|
["replay"]; ["contrast"; "one"]];
|
|
List.iter (fun delay ->
|
|
require (run ["layout"; "--delay"; delay] = Unix.WEXITED 2)
|
|
"CLI rejects invalid delay") ["nan"; "infinity"; "-infinity"; "-0.1"; "10.1"];
|
|
let path = Filename.concat folder "layout.smt2" in
|
|
require (run ["layout"; "--delay"; "0"; "--out"; path] = Unix.WEXITED 0)
|
|
"CLI accepts zero delay";
|
|
require (String.starts_with ~prefix:"(set-logic QF_BV)" (Store.read path))
|
|
"CLI writes the requested layout");
|
|
let case = read "buffering" in
|
|
List.iter (fun delay ->
|
|
rejects (fun () -> ignore (View.create ~animate:false ~delay case))
|
|
"view rejects nonfinite delay") [Float.nan; Float.infinity; Float.neg_infinity]
|
|
|
|
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;
|
|
storage folder;
|
|
transport folder;
|
|
codec ();
|
|
laws ();
|
|
fixtures ();
|
|
differential ();
|
|
buffers ();
|
|
outcomes ();
|
|
graph ();
|
|
constraints ();
|
|
validation ();
|
|
cli folder;
|
|
repair folder;
|
|
Printf.printf "%d checks passed; %d bounded reference states; %.1fs\n%!"
|
|
!checks !visited (Unix.gettimeofday () -. started)
|