From 609742674a25d4ff2ec86b6334c617aa369f9388 Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Mon, 13 Mar 2023 12:51:14 +0000 Subject: [PATCH 1/4] add test with multiple locations --- src/tracedAtomic.ml | 7 ++++++- src/tracedAtomic.mli | 6 ++++++ tests/dune | 5 +++++ tests/test_disjoint.ml | 31 +++++++++++++++++++++++++++++++ 4 files changed, 48 insertions(+), 1 deletion(-) create mode 100644 tests/test_disjoint.ml diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index dc7de29..0c00fd9 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 @@ -323,6 +324,7 @@ let reset_state () = finished_processes := 0; atomics_counter := 1; num_runs := 0; + num_traces := 0; schedule_for_checks := []; CCVector.clear processes @@ -332,3 +334,6 @@ let trace func = let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty in explore func empty_state empty_clock 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..7f9894d --- /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 () = 186); + assert (Atomic.num_traces () = 31) + +let () = + let open Alcotest in + run "disjoint_test" [ ("basic", [ test_case "two-vars" `Quick two_vars ]) ] From 5979b3778a92f65fa0c15b4738817b345bf1217e Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Mon, 13 Mar 2023 17:23:02 +0000 Subject: [PATCH 2/4] clock vector --- src/tracedAtomic.ml | 109 +++++++++++++++++++++++++++++++++++++---- tests/test_disjoint.ml | 4 +- 2 files changed, 101 insertions(+), 12 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 0c00fd9..8b4f210 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -260,7 +260,57 @@ let do_run init_func init_schedule = backtrack = IntSet.empty; } -let rec explore func state clock last_access = +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 key = Processor of int | Object of int + +module Proc_obj_map = Map.Make (struct + type t = 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 rec explore func state clock_vectors last_access = let s = last_element state in List.iter (fun proc -> @@ -271,10 +321,16 @@ let rec explore func state clock last_access = 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) + let happens_before = + let cv = Proc_obj_map.find (Processor proc.proc_id) clock_vectors in + Clock_vector.get cv ~proc_id:pre_s.run_proc + in + if i > happens_before then + 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 @@ -287,15 +343,46 @@ 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 + + assert (Option.is_some j_proc.obj_ptr || j_proc.op == Start); + + (* Start is a no-op for practical reasons. *) 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 cv_length = List.length current_state.procs in + let new_clock_vectors = + 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) + in + explore func statedash new_clock_vectors new_last_access done) let every f = every_func := f @@ -331,9 +418,11 @@ let reset_state () = let trace func = reset_state (); let empty_state = do_run func [ (0, Start, None) ] :: [] in - let empty_clock = IntMap.empty in + let clock_vectors = + Proc_obj_map.add (Processor 0) (Clock_vector.make 1) Proc_obj_map.empty + 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/tests/test_disjoint.ml b/tests/test_disjoint.ml index 7f9894d..669915a 100644 --- a/tests/test_disjoint.ml +++ b/tests/test_disjoint.ml @@ -23,8 +23,8 @@ let two_vars () = Atomic.final (fun () -> ())); - assert (Atomic.num_runs () = 186); - assert (Atomic.num_traces () = 31) + assert (Atomic.num_runs () = 33); + assert (Atomic.num_traces () = 5) let () = let open Alcotest in From be0bf243bc23b8d7e1a6beb596b17300cc6aeef3 Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Mon, 13 Mar 2023 19:41:33 +0000 Subject: [PATCH 3/4] refactor 1 --- src/tracedAtomic.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 8b4f210..68600e5 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -295,10 +295,10 @@ module Clock_vector = struct |> CCVector.freeze end -type key = Processor of int | Object of int +type proc_obj_key = Processor of int | Object of int module Proc_obj_map = Map.Make (struct - type t = key + type t = proc_obj_key let compare t1 t2 = match (t1, t2) with @@ -314,18 +314,17 @@ 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 = - Option.bind proc.obj_ptr (fun ptr -> IntMap.find_opt ptr last_access) - |> Option.value ~default:0 - in - if i != 0 then + match Option.bind proc.obj_ptr (fun ptr -> IntMap.find_opt ptr last_access) with + | None -> () + | Some i -> + assert (i > 0); let pre_s = List.nth state (i - 1) in let happens_before = let cv = Proc_obj_map.find (Processor proc.proc_id) clock_vectors in Clock_vector.get cv ~proc_id:pre_s.run_proc in if i > happens_before 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) From 127f70f4152c69c26576e49ab4c864137e34b0e5 Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Mon, 13 Mar 2023 19:52:30 +0000 Subject: [PATCH 4/4] refactor 2 --- src/tracedAtomic.ml | 189 +++++++++++++++++++++++--------------------- 1 file changed, 100 insertions(+), 89 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 68600e5..8575c6d 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -260,74 +260,111 @@ let do_run init_func init_schedule = backtrack = IntSet.empty; } -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 +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 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 init () = + Proc_obj_map.add (Processor 0) (Clock_vector.make 1) Proc_obj_map.empty -let extend_all desired_size = - Proc_obj_map.map (Clock_vector.extend desired_size) + 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 -> - match Option.bind proc.obj_ptr (fun ptr -> IntMap.find_opt ptr last_access) with - | None -> () + match + Option.bind proc.obj_ptr (fun ptr -> IntMap.find_opt ptr last_access) + with + | None -> () | Some i -> - assert (i > 0); - let pre_s = List.nth state (i - 1) in - let happens_before = - let cv = Proc_obj_map.find (Processor proc.proc_id) clock_vectors in - Clock_vector.get cv ~proc_id:pre_s.run_proc - in - if i > happens_before 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) + 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 ( @@ -345,41 +382,17 @@ let rec explore func state clock_vectors last_access = 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); - (* Start is a no-op for practical reasons. *) let new_last_access = match j_proc.obj_ptr with | Some ptr -> IntMap.add ptr state_time last_access | None -> last_access in (* Update clock vectors *) - let cv_length = List.length current_state.procs in let new_clock_vectors = - 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) + Cvs.update_clock_vectors current_state clock_vectors j j_proc state_time in explore func statedash new_clock_vectors new_last_access done) @@ -417,9 +430,7 @@ let reset_state () = let trace func = reset_state (); let empty_state = do_run func [ (0, Start, None) ] :: [] in - let clock_vectors = - Proc_obj_map.add (Processor 0) (Clock_vector.make 1) Proc_obj_map.empty - in + let clock_vectors = Cvs.init () in let empty_last_access = IntMap.empty in explore func empty_state clock_vectors empty_last_access