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 || not (Float.is_finite delay) || 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