A .gitattributes => .gitattributes +2 -0
@@ 0,0 1,2 @@
+* linguist-detectable=false
+*.smt2 linguist-detectable=true linguist-language=SMT
M Makefile => Makefile +2 -2
@@ 7,5 7,5 @@ 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
+ dune exec reorder -- repair cases/peterson.sexp --out build/repair --animate
+ dune exec reorder -- contrast build/repair/witness.sexp build/repair/repair.sexp --animate
A README.md => README.md +13 -0
@@ 0,0 1,13 @@
+Reorder synthesises minimum fence placements for programs with two threads under a finite [x86-TSO](https://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf) model, using SMT queries to find counterexamples and an independent OCaml interpreter to replay each execution before adding its fence constraint.
+
+
+
+On the Peterson fixture it places `mfence` before each flag load and closes the complete graph of 365 reachable states without overlapping critical sections, while a separate SMT query excludes every cheaper placement among the declared candidate locations.
+
+## Example
+
+```sh
+dune exec reorder -- repair cases/peterson.sexp --out build/repair
+dune exec reorder -- contrast build/repair/witness.sexp build/repair/repair.sexp --animate
+dune exec reorder -- graph cases/peterson.sexp build/repair/repair.sexp --animate
+```
A media/repair.svg => media/repair.svg +103 -0
@@ 0,0 1,103 @@
+<svg xmlns="http://www.w3.org/2000/svg" width="1080" height="610" viewBox="0 0 1080 610" role="img" aria-labelledby="title description">
+ <title id="title">A minimum fence repair for Peterson mutual exclusion</title>
+ <desc id="description">Selected events from an independently replayed execution show both threads reading zero from the other flag before entering their critical sections. Six counterexamples give constraints over four candidate fence positions. Choosing T0 at instruction 2 and T1 at instruction 2 covers all six constraints, while a budget of one fence is unsatisfiable. The original complete graph has 1315 states, 3483 edges and 12 violating states. The repaired complete graph has 365 states, 678 edges and no violating state. All figures come from the Peterson fixture</desc>
+ <defs>
+ <marker id="arrow" viewBox="0 0 8 8" refX="7" refY="4" markerWidth="7" markerHeight="7" orient="auto">
+ <path d="M1 1 L7 4 L1 7" fill="none" stroke="#68737b" stroke-width="1"/>
+ </marker>
+ </defs>
+ <rect width="1080" height="610" fill="#fff"/>
+ <g font-family="Latin Modern Roman, STIX Two Text, Times New Roman, serif" fill="#20272c">
+ <text x="34" y="38" font-size="27">Peterson under TSO</text>
+ <text x="34" y="65" font-size="17" fill="#4b5563">From a buffered execution to a checked minimum repair</text>
+ <text x="265" y="103" text-anchor="middle" font-size="20">Replayed counterexample</text>
+ <text x="779" y="103" text-anchor="middle" font-size="20">Blocking constraints</text>
+ <g text-anchor="middle" font-size="18">
+ <text x="150" y="136">Thread 0</text>
+ <text x="380" y="136">Thread 1</text>
+ </g>
+ <g fill="none" stroke="#88939a" stroke-width="1" marker-end="url(#arrow)">
+ <path d="M150 148 V350"/>
+ <path d="M380 148 V350"/>
+ </g>
+ <g fill="#fff">
+ <path d="M65 151 H235 V175 H65 Z M65 199 H235 V223 H65 Z M49 223 H251 V247 H49 Z M101 295 H199 V319 H101 Z"/>
+ <path d="M295 175 H465 V199 H295 Z M295 247 H465 V271 H295 Z M279 271 H481 V295 H279 Z M331 319 H429 V343 H331 Z"/>
+ </g>
+ <g text-anchor="middle" font-family="DejaVu Sans Mono, monospace" font-size="16">
+ <text x="150" y="169">flag0 ← 1</text>
+ <text x="380" y="193">flag1 ← 1</text>
+ <text x="150" y="217">turn ← 1</text>
+ <text x="380" y="265">turn ← 0</text>
+ <text x="150" y="241">r0 ← flag1 = 0</text>
+ <text x="380" y="289">r0 ← flag0 = 0</text>
+ <text x="150" y="313">enter</text>
+ <text x="380" y="337">enter</text>
+ </g>
+ <path d="M113 354 V361 H417 V354" fill="none" stroke="#68737b" stroke-width="1"/>
+ <text x="265" y="385" font-size="20" text-anchor="middle">Both threads enter</text>
+ <text x="265" y="409" font-size="16" fill="#4b5563" text-anchor="middle">The flag stores are still buffered at the reads</text>
+ <path d="M491 257 H549" fill="none" stroke="#68737b" stroke-width="1" marker-end="url(#arrow)"/>
+ <text x="520" y="243" font-size="15" text-anchor="middle" fill="#4b5563">learn</text>
+ <g fill="#edf4f1">
+ <rect x="711" y="152" width="58" height="200"/>
+ <rect x="891" y="152" width="58" height="200"/>
+ </g>
+ <g text-anchor="middle" font-family="DejaVu Sans Mono, monospace" font-size="16">
+ <text x="650" y="137">T0@1</text>
+ <text x="740" y="137" fill="#176654">T0@2</text>
+ <text x="830" y="137">T1@1</text>
+ <text x="920" y="137" fill="#176654">T1@2</text>
+ </g>
+ <path d="M716 144 H764 M896 144 H944" fill="none" stroke="#176654" stroke-width="1.5"/>
+ <g fill="none" stroke="#68737b" stroke-width="1">
+ <path d="M610 155 H600 V349 H610 M960 155 H970 V349 H960"/>
+ </g>
+ <g text-anchor="end" font-size="17" font-style="italic" fill="#4b5563">
+ <text x="581" y="179">c₀</text>
+ <text x="581" y="211">c₁</text>
+ <text x="581" y="243">c₂</text>
+ <text x="581" y="275">c₃</text>
+ <text x="581" y="307">c₄</text>
+ <text x="581" y="339">c₅</text>
+ </g>
+ <g fill="#20272c">
+ <circle cx="650" cy="173" r="4"/><circle cx="830" cy="173" r="4"/>
+ <circle cx="830" cy="205" r="4"/>
+ <circle cx="650" cy="237" r="4"/><circle cx="830" cy="237" r="4"/>
+ <circle cx="650" cy="269" r="4"/>
+ <circle cx="650" cy="301" r="4"/>
+ </g>
+ <g fill="#176654">
+ <circle cx="740" cy="173" r="5"/><circle cx="920" cy="173" r="5"/>
+ <circle cx="920" cy="205" r="5"/>
+ <circle cx="740" cy="237" r="5"/>
+ <circle cx="740" cy="269" r="5"/>
+ <circle cx="920" cy="301" r="5"/>
+ <circle cx="740" cy="333" r="5"/><circle cx="920" cy="333" r="5"/>
+ </g>
+ <text x="785" y="385" font-size="18" text-anchor="middle">Every constraint needs a selected fence</text>
+ <text x="785" y="409" font-size="16" fill="#4b5563" text-anchor="middle">No single column covers all six rows</text>
+ <path d="M34 436 H1046" fill="none" stroke="#88939a" stroke-width="1"/>
+ <text x="34" y="474" font-size="24">Minimum repair</text>
+ <text x="34" y="507" font-family="DejaVu Sans Mono, monospace" font-size="21" fill="#176654">T0@2 ∧ T1@2</text>
+ <text x="34" y="535" font-size="18">mfence before each flag load</text>
+ <text x="34" y="578" font-size="17">Fence budget ≤ 1 is UNSAT</text>
+ <g text-anchor="middle" font-size="17">
+ <text x="746" y="474">States</text>
+ <text x="863" y="474">Edges</text>
+ <text x="990" y="474">Violating states</text>
+ <text x="746" y="507">1315</text>
+ <text x="863" y="507">3483</text>
+ <text x="990" y="507">12</text>
+ <g fill="#176654">
+ <text x="746" y="539">365</text>
+ <text x="863" y="539">678</text>
+ <text x="990" y="539">0</text>
+ </g>
+ </g>
+ <text x="523" y="507" font-size="17">Without fences</text>
+ <text x="523" y="539" font-size="17" fill="#176654">With two fences</text>
+ <text x="523" y="578" font-size="17">Reachable graph closed under every transition</text>
+ </g>
+</svg>
R dune => src/dune +0 -6
@@ 9,9 9,3 @@
(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)))
R engine.ml => src/engine.ml +0 -0
R engine.mli => src/engine.mli +0 -0
R layout.ml => src/layout.ml +0 -0
R layout.mli => src/layout.mli +0 -0
R machine.ml => src/machine.ml +0 -0
R machine.mli => src/machine.mli +0 -0
R main.ml => src/main.ml +11 -0
@@ 29,6 29,17 @@ let () =
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";
+ if not (Float.is_finite !delay) || !delay < 0. || !delay > 10. then
+ invalid_arg "delay outside 0..10 seconds";
+ let minimum, maximum = match command with
+ | "layout" | "laws" -> 0, 0
+ | "contrast" -> 2, 2
+ | "graph" -> 1, 2
+ | "check" | "repair" | "replay" | "compare" | "audit" | "emit" -> 1, 1
+ | _ -> invalid_arg "unknown command" in
+ let count = List.length !files in
+ if count < minimum || count > maximum then
+ invalid_arg (Printf.sprintf "%s expects %d..%d input files" command minimum maximum);
let file () = match !files with path :: _ -> path | [] -> invalid_arg "missing input file" in
let output fallback = Option.value !folder ~default:fallback in
let load () =
R sexp.ml => src/sexp.ml +0 -0
R sexp.mli => src/sexp.mli +0 -0
R solver.ml => src/solver.ml +0 -0
R solver.mli => src/solver.mli +0 -0
R store.ml => src/store.ml +0 -0
R store.mli => src/store.mli +0 -0
R syntax.ml => src/syntax.ml +0 -0
R syntax.mli => src/syntax.mli +0 -0
R view.ml => src/view.ml +2 -1
@@ 146,7 146,8 @@ let draw view 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 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=[]}
R view.mli => src/view.mli +0 -0
R check.ml => test/check.ml +27 -0
@@ 184,6 184,32 @@ let validation () =
{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
@@ 222,6 248,7 @@ let () =
graph ();
constraints ();
validation ();
+ cli folder;
repair folder;
Printf.printf "%d checks passed; %d bounded reference states; %.1fs\n%!"
!checks !visited (Unix.gettimeofday () -. started)
A test/dune => test/dune +6 -0
@@ 0,0 1,6 @@
+(test
+ (name check)
+ (modules check)
+ (libraries core unix)
+ (deps ../src/main.exe (glob_files ../cases/*.sexp) (glob_files ../smt/*.smt2))
+ (action (chdir .. (run %{test}))))
