From 813a8cbfb1c0cce5de4be0150afc8f4943f9d4f0 Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Mon, 20 Mar 2023 18:40:52 +0000 Subject: [PATCH] checkpoint --- .ocamlformat | 2 +- src/tracedAtomic.ml | 218 ++++++++++++++++++++++++++++-- tests/dune | 10 ++ tests/test_michael_scott_queue.ml | 18 ++- tests/test_simple.ml | 16 +++ tests/test_simple2.ml | 19 +++ 6 files changed, 265 insertions(+), 18 deletions(-) create mode 100644 tests/test_simple.ml create mode 100644 tests/test_simple2.ml diff --git a/.ocamlformat b/.ocamlformat index 9d647c5..9d82a26 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,2 +1,2 @@ profile = default -version = 0.24.1 \ No newline at end of file +version = 0.25.1 \ No newline at end of file diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index dc7de29..f4ffa50 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -12,7 +12,6 @@ type _ Effect.t += | FetchAndAdd : (int t * int) -> int Effect.t module IntSet = Set.Make (Int) - module IntMap = Map.Make (Int) let _string_of_set s = IntSet.fold (fun y x -> string_of_int y ^ "," ^ x) s "" @@ -194,10 +193,36 @@ type state_cell = { } let num_runs = ref 0 +let num_traces = ref 0 (* we stash the current state in case a check fails and we need to log it *) let schedule_for_checks = ref [] +let print_trace () = + Printf.printf "-----------------------\n"; + List.iter + (fun s -> + match s with + | last_run_proc, last_run_op, last_run_ptr -> + let var_name i = + let c = Char.chr (i + 97) in + let seq = Seq.cons c Seq.empty in + String.of_seq seq + in + + let last_run_ptr = + Option.map (* string_of_int *) var_name last_run_ptr + |> Option.value ~default:"" + in + let tabs = + List.init last_run_proc (fun _ -> "\t\t") |> String.concat "" + in + Printf.printf "%sP%d: %s %s\n" tabs last_run_proc + (atomic_op_str last_run_op) + last_run_ptr) + !schedule_for_checks; + Printf.printf "-----------------------\n%!" + let do_run init_func init_schedule = init_func (); (*set up run *) @@ -214,6 +239,8 @@ let do_run init_func init_schedule = | [] -> if !finished_processes == num_processes then ( tracing := false; + print_trace (); + num_traces := !num_traces + 1; !final_func (); tracing := true) | (process_id_to_run, next_op, next_ptr) :: schedule -> @@ -259,6 +286,172 @@ let do_run init_func init_schedule = backtrack = IntSet.empty; } +let _set_to_str s = + IntSet.to_seq s |> List.of_seq |> List.map Int.to_string |> String.concat ", " + +let rec explore_source depth func state sleep = + (* sleep := IntSet.empty; *) + let s = last_element state in + (* Printf.printf "[depth=%d] explore (backtrack=[%s], sleep=[%s], enabled=[%s])\n%!" depth + (set_to_str s.backtrack) (set_to_str !sleep) (set_to_str s.enabled); *) + let p_maybe = IntSet.min_elt_opt (IntSet.diff s.enabled !sleep) in + match p_maybe with + | None -> () (* Printf.printf "[depth=%d] rtn\n%!" depth *) + | Some p -> + s.backtrack <- IntSet.singleton p; + + while IntSet.(cardinal (diff s.backtrack !sleep)) > 0 do + (* Printf.printf "[depth=%d] loop (backtrack=[%s], sleep=[%s])\n%!" depth + (set_to_str s.backtrack) (set_to_str !sleep); *) + let p = IntSet.min_elt (IntSet.diff s.backtrack !sleep) in + let proc = List.nth s.procs p in + + (* Printf.printf "[depth=%d] p=%d, %s\n%!" depth p (atomic_op_str proc.op); *) + (* run *) + let state_top = + let schedule = + List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state + @ [ (p, proc.op, proc.obj_ptr) ] + in + do_run func schedule + in + assert (state_top.run_proc = p); + let new_state = state @ [ state_top ] in + + let obj_ptr = Option.value proc.obj_ptr ~default:(-1) in + (* find reversible races *) + let reversible_races = + List.filter + (fun proc' -> + let run_ptr = Option.value proc'.run_ptr ~default:(-2) in + obj_ptr = run_ptr && proc'.run_proc <> p) + new_state + in + let reversible_races = + match reversible_races with + | [] -> [] + | _ -> [ last_element reversible_races ] + in + + (* Printf.printf "[depth=%d] reversible races sz: %d\n%!" depth + (List.length reversible_races); *) + for i = 0 to List.length reversible_races - 1 do + let e = List.nth reversible_races i in + (* Printf.printf "[depth=%d] inner loop, racing op: e=(q=%d, %s)\n%!" + depth e.run_proc (atomic_op_str e.run_op); *) + let found_e, prefix_rev, suffix_rev = + List.fold_left + (fun (seen_e, prefix, suffix) proc' -> + if seen_e then (seen_e, prefix, proc' :: suffix) + else if proc' == e then (true, prefix, suffix) + else (false, proc' :: prefix, suffix)) + (false, [], []) state + in + assert ( + List.length prefix_rev + List.length suffix_rev + = List.length state - 1); + assert found_e; + let prefix (* E' *) = List.rev prefix_rev in + + if List.length prefix > 0 then + (* List.iter + (fun proc -> + Printf.printf "[depth=%d] ::prefix:: (p=%d, %s)\n%!" depth + proc.run_proc + (atomic_op_str proc.run_op)) + prefix; *) + let suffix = List.rev suffix_rev in + + (* List.iter + (fun proc -> + Printf.printf "[depth=%d] ::suffix:: (p=%d, %s)\n%!" depth + proc.run_proc + (atomic_op_str proc.run_op)) + suffix; *) + let prefix_top = last_element prefix in + + (* Printf.printf + "[depth=%d] nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth + prefix_top.run_proc + (atomic_op_str prefix_top.run_op); *) + let v_E (* occurs after e but independent of e *) = + List.filter + (fun proc' -> + proc'.run_proc <> e.run_proc + && Option.value proc'.run_ptr ~default:(-1) + <> Option.value e.run_ptr ~default:(-2)) + suffix + in + + (* List.iter + (fun proc -> + Printf.printf + "[depth=%d] ::occurs_after_e_but_indep:: (p=%d, %s)\n%!" + depth proc.run_proc + (atomic_op_str proc.run_op)) + v_E; *) + let v = v_E @ [ state_top ] in + + (* List.iter + (fun proc -> + Printf.printf "[depth=%d] ::v:: (p=%d, %s)\n%!" depth + proc.run_proc + (atomic_op_str proc.run_op)) + v; *) + let initials = + let initials_map, initials_spawns = + List.fold_left + (fun (first_accesses, spawns) (state_cell : state_cell) -> + match state_cell.run_ptr with + | None -> + let new_spawns = + IntSet.add state_cell.run_proc spawns + in + (first_accesses, new_spawns) + | Some obj_ptr -> + let new_first_accesses = + IntMap.update obj_ptr + (function + | Some v -> Some v + | None -> Some state_cell.run_proc) + first_accesses + in + (new_first_accesses, spawns)) + (IntMap.empty, IntSet.empty) + v + in + IntMap.fold + (fun _ run_proc initials_set -> + IntSet.add run_proc initials_set) + initials_map initials_spawns + in + + (* Printf.printf "[depth=%d] initials=[%s], backtrack=[%s]\n%!" + depth (set_to_str initials) + (set_to_str prefix_top.backtrack); *) + if IntSet.(cardinal (inter prefix_top.backtrack initials)) = 0 then + let _initial = IntSet.min_elt initials in + (* Printf.printf "[depth=%d] adding initial to backtrack\n%!" + depth; *) + prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack + done; + + let sleep' = + IntSet.filter + (fun q -> + (* only keep q that are independent with p: must be other thread of execution and act on a different object (or none) *) + if q == p then false + else + let proc' = List.nth s.procs q in + match proc'.obj_ptr with + | None -> true + | Some obj_ptr' -> obj_ptr' <> obj_ptr) + !sleep + in + explore_source (depth + 1) func new_state (ref sleep'); + sleep := IntSet.add p !sleep + done + let rec explore func state clock last_access = let s = last_element state in List.iter @@ -305,17 +498,7 @@ let check f = tracing := false; if not (f ()) then ( Printf.printf "Found assertion violation at run %d:\n" !num_runs; - List.iter - (fun s -> - match s with - | last_run_proc, last_run_op, last_run_ptr -> - let last_run_ptr = - Option.map string_of_int last_run_ptr |> Option.value ~default:"" - in - Printf.printf "Process %d: %s %s\n" last_run_proc - (atomic_op_str last_run_op) - last_run_ptr) - !schedule_for_checks; + print_trace (); assert false); tracing := tracing_at_start @@ -326,9 +509,18 @@ let reset_state () = schedule_for_checks := []; CCVector.clear processes -let trace func = +let _trace func = reset_state (); let empty_state = do_run func [ (0, Start, None) ] :: [] in let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty in explore func empty_state empty_clock empty_last_access + +let _trace_source func = + reset_state (); + let empty_state = do_run func [ (0, Start, None) ] in + explore_source 0 func [ empty_state ] (ref IntSet.empty) + +let trace func = + _trace_source func; + Printf.printf "\nnum_traces: %d\n%!" !num_traces diff --git a/tests/dune b/tests/dune index 9d006d4..5ff04b6 100644 --- a/tests/dune +++ b/tests/dune @@ -12,3 +12,13 @@ (name test_michael_scott_queue) (libraries dscheck alcotest) (modules test_michael_scott_queue michael_scott_queue)) + +(test + (name test_simple) + (libraries dscheck alcotest) + (modules test_simple)) + +(test + (name test_simple2) + (libraries dscheck) + (modules test_simple2)) diff --git a/tests/test_michael_scott_queue.ml b/tests/test_michael_scott_queue.ml index 081643b..66cdef3 100644 --- a/tests/test_michael_scott_queue.ml +++ b/tests/test_michael_scott_queue.ml @@ -8,29 +8,39 @@ let drain queue = done; !remaining +let list_to_str s = + List.map (function Some i -> Int.to_string i | None -> "_") s + |> String.concat ", " + let producer_consumer () = Atomic.trace (fun () -> let queue = Michael_scott_queue.create () in let items_total = 4 in Atomic.spawn (fun () -> - for _ = 1 to items_total do - Michael_scott_queue.push queue 0 + for i = 1 to items_total do + Michael_scott_queue.push queue i done); + let result = ref [] in + (* consumer *) let popped = ref 0 in Atomic.spawn (fun () -> for _ = 1 to items_total do match Michael_scott_queue.pop queue with - | None -> () - | Some _ -> popped := !popped + 1 + | None -> result := None :: !result + | Some v -> + (result := Some v :: !result; + popped := !popped + 1) done); (* checks*) Atomic.final (fun () -> + Printf.printf "pop sequence: %s\n" (list_to_str !result); Atomic.check (fun () -> let remaining = drain queue in + Printf.printf "popped=%d, remaining=%d\n%!" !popped remaining; !popped + remaining = items_total))) let () = diff --git a/tests/test_simple.ml b/tests/test_simple.ml new file mode 100644 index 0000000..a2e5b7e --- /dev/null +++ b/tests/test_simple.ml @@ -0,0 +1,16 @@ +module Atomic = Dscheck.TracedAtomic + +let counter () = + let a = Atomic.make 0 in + let b = Atomic.make 0 in + Atomic.spawn (fun () -> + Atomic.set a 1; + Atomic.set b 2); + Atomic.spawn (fun () -> + Atomic.set a 3; + Atomic.set b 4); + Atomic.final (fun () -> + Printf.printf "a=%d, b=%d\n%!" (Atomic.get a) (Atomic.get b)) + +let test_safe_counter () = Atomic.trace counter +let _ = test_safe_counter () diff --git a/tests/test_simple2.ml b/tests/test_simple2.ml new file mode 100644 index 0000000..7d2a5ed --- /dev/null +++ b/tests/test_simple2.ml @@ -0,0 +1,19 @@ +module Atomic = Dscheck.TracedAtomic + +let test () = + let c = Atomic.make 0 in + let b = Atomic.make 0 in + let ok = Atomic.make false in + + Atomic.spawn (fun () -> Atomic.set b 1); + Atomic.spawn (fun () -> + Atomic.set c 1; + Atomic.set b 2); + Atomic.spawn (fun () -> + if Atomic.get c = 0 then if Atomic.get b = 0 then Atomic.set ok true); + + Atomic.final (fun () -> + Format.printf "b=%i c=%i ok=%b@." (Atomic.get b) (Atomic.get c) + (Atomic.get ok)) + +let () = Atomic.trace test