diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index dc7de29..8575c6d 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,6 +193,7 @@ 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 [] @@ -215,6 +215,7 @@ let do_run init_func init_schedule = if !finished_processes == num_processes then ( tracing := false; !final_func (); + num_traces := !num_traces + 1; tracing := true) | (process_id_to_run, next_op, next_ptr) :: schedule -> if !finished_processes == num_processes then @@ -259,21 +260,113 @@ let do_run init_func init_schedule = backtrack = IntSet.empty; } -let rec explore func state clock last_access = +module Cvs = struct + (* Cvs (clock vectors) let us track happens-before relationship between different objects. *) + module Clock_vector = struct + type t = (int, CCVector.ro) CCVector.t + + let make size : t = CCVector.init size (fun _ -> 0) + + let extend desired_size t : t = + let diff = desired_size - CCVector.length t in + if diff <= 0 then t + else + let mut = CCVector.copy t in + for _ = 1 to diff do + CCVector.push mut 0 + done; + CCVector.freeze mut + + let update (t : t) ~proc_id ~state_time : t = + let t = CCVector.copy t in + CCVector.set t proc_id state_time; + CCVector.freeze t + + let get t ~proc_id = CCVector.get t proc_id + + let max (t1 : t) (t2 : t) : t = + let rec f = function + | [], [] -> [] + | [], _ | _, [] -> + failwith + (Printf.sprintf + "max: vector clocks have different lengths (%d, %d)" + (CCVector.length t1) (CCVector.length t2)) + | item1 :: tail1, item2 :: tail2 -> max item1 item2 :: f (tail1, tail2) + in + CCVector.of_list (f (CCVector.to_list t1, CCVector.to_list t2)) + |> CCVector.freeze + end + + type proc_obj_key = Processor of int | Object of int + + module Proc_obj_map = Map.Make (struct + type t = proc_obj_key + + let compare t1 t2 = + match (t1, t2) with + | Processor v1, Processor v2 | Object v1, Object v2 -> Int.compare v1 v2 + | Processor _, Object _ -> 1 + | Object _, Processor _ -> -1 + end) + + let extend_all desired_size = + Proc_obj_map.map (Clock_vector.extend desired_size) + + let update_clock_vectors current_state clock_vectors j j_proc state_time = + let cv_length = List.length current_state.procs in + let clock_vectors = extend_all cv_length clock_vectors in + match j_proc.op with + | Make -> clock_vectors + | Start -> + Proc_obj_map.add (Processor j) + (Clock_vector.make cv_length) + clock_vectors + | Get | Set | Exchange | CompareAndSwap | FetchAndAdd -> + let obj_key = Object (Option.get j_proc.obj_ptr) in + let proc_key = Processor j in + let cv = + let proc_cv = Proc_obj_map.find proc_key clock_vectors in + let cv = + let obj_cv_opt = Proc_obj_map.find_opt obj_key clock_vectors in + match obj_cv_opt with + | Some obj_cv -> + assert (CCVector.length proc_cv = CCVector.length obj_cv); + Clock_vector.max obj_cv proc_cv + | None -> proc_cv + in + Clock_vector.update cv ~proc_id:j ~state_time + in + Proc_obj_map.update obj_key (fun _ -> Some cv) clock_vectors + |> Proc_obj_map.update proc_key (fun _ -> Some cv) + + let init () = + Proc_obj_map.add (Processor 0) (Clock_vector.make 1) Proc_obj_map.empty + + let clock_val clock_vectors pre_s proc = + let cv = Proc_obj_map.find (Processor proc.proc_id) clock_vectors in + Clock_vector.get cv ~proc_id:pre_s.run_proc +end + +let rec explore func state clock_vectors last_access = let s = last_element state in List.iter (fun proc -> - let j = proc.proc_id in - let i = + match Option.bind proc.obj_ptr (fun ptr -> IntMap.find_opt ptr last_access) - |> Option.value ~default:0 - in - if i != 0 then - let pre_s = List.nth state (i - 1) in - if IntSet.mem j pre_s.enabled then - pre_s.backtrack <- IntSet.add j pre_s.backtrack - else pre_s.backtrack <- IntSet.union pre_s.backtrack pre_s.enabled) + with + | None -> () + | Some i -> + assert (i > 0); + let pre_s = List.nth state (i - 1) in + let clock_val = Cvs.clock_val clock_vectors pre_s proc in + if i > clock_val then + let j = proc.proc_id in + if IntSet.mem j pre_s.enabled then + pre_s.backtrack <- IntSet.add j pre_s.backtrack + else pre_s.backtrack <- IntSet.union pre_s.backtrack pre_s.enabled) s.procs; + let state_time = List.length state in if IntSet.cardinal s.enabled > 0 then ( let p = IntSet.min_elt s.enabled in let dones = ref IntSet.empty in @@ -286,15 +379,22 @@ let rec explore func state clock last_access = List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state @ [ (j, j_proc.op, j_proc.obj_ptr) ] in - let statedash = state @ [ do_run func schedule ] in - let state_time = List.length statedash - 1 in + let current_state = do_run func schedule in + let statedash = state @ [ current_state ] in + + (* Start is a no-op for practical reasons. *) + assert (Option.is_some j_proc.obj_ptr || j_proc.op == Start); + let new_last_access = match j_proc.obj_ptr with | Some ptr -> IntMap.add ptr state_time last_access | None -> last_access in - let new_clock = IntMap.add j state_time clock in - explore func statedash new_clock new_last_access + (* Update clock vectors *) + let new_clock_vectors = + Cvs.update_clock_vectors current_state clock_vectors j j_proc state_time + in + explore func statedash new_clock_vectors new_last_access done) let every f = every_func := f @@ -323,12 +423,16 @@ let reset_state () = finished_processes := 0; atomics_counter := 1; num_runs := 0; + num_traces := 0; schedule_for_checks := []; CCVector.clear processes let trace func = reset_state (); let empty_state = do_run func [ (0, Start, None) ] :: [] in - let empty_clock = IntMap.empty in + let clock_vectors = Cvs.init () in let empty_last_access = IntMap.empty in - explore func empty_state empty_clock empty_last_access + explore func empty_state clock_vectors empty_last_access + +let num_runs () = !num_runs +let num_traces () = !num_traces diff --git a/src/tracedAtomic.mli b/src/tracedAtomic.mli index 4e0b8e3..fb4d6be 100644 --- a/src/tracedAtomic.mli +++ b/src/tracedAtomic.mli @@ -60,3 +60,9 @@ val final : (unit -> unit) -> unit val every : (unit -> unit) -> unit (** run [f] between every possible interleaving *) + +val num_runs : unit -> int +(** [num_runs ()] returns number of states explored in the last run *) + +val num_traces : unit -> int +(** [num_traces ()] returns number of traces validated in the last run *) diff --git a/tests/dune b/tests/dune index 9d006d4..137f114 100644 --- a/tests/dune +++ b/tests/dune @@ -12,3 +12,8 @@ (name test_michael_scott_queue) (libraries dscheck alcotest) (modules test_michael_scott_queue michael_scott_queue)) + +(test + (name test_disjoint) + (libraries dscheck alcotest) + (modules test_disjoint)) diff --git a/tests/test_disjoint.ml b/tests/test_disjoint.ml new file mode 100644 index 0000000..669915a --- /dev/null +++ b/tests/test_disjoint.ml @@ -0,0 +1,31 @@ +module Atomic = Dscheck.TracedAtomic + +let two_vars () = + let a = Atomic.make 0 in + let b = Atomic.make 0 in + let c = Atomic.make 0 in + let d = Atomic.make 0 in + + Atomic.trace (fun () -> + Atomic.spawn (fun () -> + Atomic.set a 1; + Atomic.set b 1; + Atomic.set c 1; + Atomic.set d 1) + |> ignore; + + Atomic.spawn (fun () -> + Atomic.set d 2; + Atomic.set c 2; + Atomic.set b 2; + Atomic.set a 2) + |> ignore; + + Atomic.final (fun () -> ())); + + assert (Atomic.num_runs () = 33); + assert (Atomic.num_traces () = 5) + +let () = + let open Alcotest in + run "disjoint_test" [ ("basic", [ test_case "two-vars" `Quick two_vars ]) ]