From ea53d04d0df60ce49a368b2cd7cec3c35b96a71f Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Thu, 9 Feb 2023 15:24:03 +0000 Subject: [PATCH 1/4] Fix continuations leak in processes cleanup --- dscheck.opam | 1 + src/tracedAtomic.ml | 39 +++++++++++++------ tests/dune | 5 +++ tests/michael_scott_queue.ml | 62 +++++++++++++++++++++++++++++++ tests/test_list.ml | 6 +-- tests/test_michael_scott_queue.ml | 39 +++++++++++++++++++ 6 files changed, 138 insertions(+), 14 deletions(-) create mode 100644 tests/michael_scott_queue.ml create mode 100644 tests/test_michael_scott_queue.ml diff --git a/dscheck.opam b/dscheck.opam index 242a1eb..044fcb6 100644 --- a/dscheck.opam +++ b/dscheck.opam @@ -11,6 +11,7 @@ depends: [ "dune" {>= "2.9"} "containers" "oseq" + "alcotest" {>= "1.6.0"} "odoc" {with-doc} ] build: [ diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 8ec2c3d..b39a777 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -48,6 +48,7 @@ type process_data = { mutable next_repr: int option; mutable resume_func : (unit, unit) handler -> unit; mutable finished : bool; + mutable discontinue_f : unit -> unit; } let every_func = ref (fun () -> ()) @@ -82,18 +83,33 @@ let incr r = ignore (fetch_and_add r 1) let decr r = ignore (fetch_and_add r (-1)) (* Tracing infrastructure *) + +exception Terminated_early + +let discontinue k () = + discontinue_with k Terminated_early ({ + retc = (fun _ -> ()); + exnc = (function Terminated_early -> () | e -> raise e); + effc = (fun (type a) (_ : a Effect.t) -> None); + }) +;; + let processes = CCVector.create () -let update_process_data process_id f op repr = +let update_process_data process_id f op repr k = let process_rec = CCVector.get processes process_id in process_rec.resume_func <- f; process_rec.next_repr <- repr; - process_rec.next_op <- op + process_rec.next_op <- op; + process_rec.discontinue_f <- discontinue k +;; let finish_process process_id = let process_rec = CCVector.get processes process_id in process_rec.finished <- true; + process_rec.discontinue_f <- (fun () -> ()); finished_processes := !finished_processes + 1 +;; let handler current_process_id runner = { @@ -112,44 +128,44 @@ let handler current_process_id runner = let i = !atomics_counter in let m = (Atomic.make v, i) in atomics_counter := !atomics_counter + 1; - update_process_data current_process_id (fun h -> continue_with k m h) Make (Some i); + update_process_data current_process_id (fun h -> continue_with k m h) Make (Some i) k; runner ()) | Get (v,i) -> Some (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> continue_with k (Atomic.get v) h) Get (Some i); + update_process_data current_process_id (fun h -> continue_with k (Atomic.get v) h) Get (Some i) k; runner ()) | Set ((r,i), v) -> Some (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> continue_with k (Atomic.set r v) h) Set (Some i); + update_process_data current_process_id (fun h -> continue_with k (Atomic.set r v) h) Set (Some i) k; runner ()) | Exchange ((a,i), b) -> Some (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> continue_with k (Atomic.exchange a b) h) Exchange (Some i); + update_process_data current_process_id (fun h -> continue_with k (Atomic.exchange a b) h) Exchange (Some i) k; runner ()) | CompareAndSwap ((x,i), s, v) -> Some (fun (k : (a, _) continuation) -> update_process_data current_process_id (fun h -> - continue_with k (Atomic.compare_and_set x s v) h) CompareAndSwap (Some i); + continue_with k (Atomic.compare_and_set x s v) h) CompareAndSwap (Some i) k; runner ()) | FetchAndAdd ((v,i), x) -> Some (fun (k : (a, _) continuation) -> update_process_data current_process_id (fun h -> - continue_with k (Atomic.fetch_and_add v x) h) FetchAndAdd (Some i); + continue_with k (Atomic.fetch_and_add v x) h) FetchAndAdd (Some i) k; runner ()) | _ -> None); } let spawn f = - let fiber_f h = - continue_with (fiber f) () h in + let fiber_f = fiber f in + let resume_func = continue_with fiber_f () in CCVector.push processes - { next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } + { next_op = Start; next_repr = None; resume_func; finished = false; discontinue_f = discontinue fiber_f} let rec last_element l = match l with @@ -208,6 +224,7 @@ let do_run init_func init_schedule = |> Seq.filter (fun (_,proc) -> not proc.finished) |> Seq.map (fun (id,_) -> id) |> IntSet.of_seq in + CCVector.iter (fun proc -> proc.discontinue_f ()) processes; CCVector.clear processes; atomics_counter := 1; match last_element init_schedule with diff --git a/tests/dune b/tests/dune index db241a0..9d006d4 100644 --- a/tests/dune +++ b/tests/dune @@ -7,3 +7,8 @@ (name test_naive_counter) (libraries dscheck alcotest) (modules test_naive_counter)) + +(test + (name test_michael_scott_queue) + (libraries dscheck alcotest) + (modules test_michael_scott_queue michael_scott_queue)) diff --git a/tests/michael_scott_queue.ml b/tests/michael_scott_queue.ml new file mode 100644 index 0000000..8edbeea --- /dev/null +++ b/tests/michael_scott_queue.ml @@ -0,0 +1,62 @@ +(* + * Copyright (c) 2015, Théo Laurent + * Copyright (c) 2015, KC Sivaramakrishnan + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + *) + +(* Michael-Scott queue copied over from [lockfree](github.com/ocaml-multicore/lockfree) *) +module Atomic = Dscheck.TracedAtomic + +type 'a node = Nil | Next of 'a * 'a node Atomic.t +type 'a t = { head : 'a node Atomic.t; tail : 'a node Atomic.t } + +let create () = + let head = Next (Obj.magic (), Atomic.make Nil) in + { head = Atomic.make head; tail = Atomic.make head } + +let is_empty q = + match Atomic.get q.head with + | Nil -> failwith "MSQueue.is_empty: impossible" + | Next (_, x) -> ( match Atomic.get x with Nil -> true | _ -> false) + +let pop q = + let rec loop () = + let s = Atomic.get q.head in + let nhead = + match s with + | Nil -> failwith "MSQueue.pop: impossible" + | Next (_, x) -> Atomic.get x + in + match nhead with + | Nil -> None + | Next (v, _) when Atomic.compare_and_set q.head s nhead -> Some v + | _ -> loop () + in + loop () + +let push q v = + let rec find_tail_and_enq curr_end node = + if Atomic.compare_and_set curr_end Nil node then () + else + match Atomic.get curr_end with + | Nil -> find_tail_and_enq curr_end node + | Next (_, n) -> find_tail_and_enq n node + in + let newnode = Next (v, Atomic.make Nil) in + let tail = Atomic.get q.tail in + match tail with + | Nil -> failwith "HW_MSQueue.push: impossible" + | Next (_, n) -> + find_tail_and_enq n newnode; + ignore (Atomic.compare_and_set q.tail tail newnode) diff --git a/tests/test_list.ml b/tests/test_list.ml index dcdc556..8ed65b0 100644 --- a/tests/test_list.ml +++ b/tests/test_list.ml @@ -50,8 +50,8 @@ let test_list_naive domains () = | exception _ -> () | _ -> failwith "expected failure" -let test_list_safe () = Atomic.trace (create_test add_node_safe 3) -(* 4 takes over 10 Gb of RAM *) +let test_list_safe () = + Atomic.trace (create_test add_node_safe 3) let () = let open Alcotest in @@ -60,7 +60,7 @@ let () = ( "list", [ test_case "naive-1-domain" `Quick (test_list_naive_single_domain); - test_case "naive-2-domains" `Quick (test_list_naive 8); + test_case "naive-2-domains" `Quick (test_list_naive 2); test_case "naive-8-domains" `Quick (test_list_naive 8); test_case "safe" `Quick test_list_safe; ] ); diff --git a/tests/test_michael_scott_queue.ml b/tests/test_michael_scott_queue.ml new file mode 100644 index 0000000..081643b --- /dev/null +++ b/tests/test_michael_scott_queue.ml @@ -0,0 +1,39 @@ +module Atomic = Dscheck.TracedAtomic + +let drain queue = + let remaining = ref 0 in + while not (Michael_scott_queue.is_empty queue) do + remaining := !remaining + 1; + assert (Option.is_some (Michael_scott_queue.pop queue)) + done; + !remaining + +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 + done); + + (* 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 + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = drain queue in + !popped + remaining = items_total))) + +let () = + let open Alcotest in + run "michael_scott_queue_dscheck" + [ ("basic", [ test_case "1-producer-1-consumer" `Slow producer_consumer ]) ] From 174ecb3251619c6ff455847b8a201945d281af13 Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Thu, 9 Feb 2023 21:58:43 +0000 Subject: [PATCH 2/4] ocamlformat --- .ocamlformat | 2 + src/dune | 4 +- src/tracedAtomic.ml | 321 ++++++++++++++++++++++++------------------- src/tracedAtomic.mli | 2 +- tests/test_list.ml | 5 +- 5 files changed, 188 insertions(+), 146 deletions(-) create mode 100644 .ocamlformat diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..9d647c5 --- /dev/null +++ b/.ocamlformat @@ -0,0 +1,2 @@ +profile = default +version = 0.24.1 \ No newline at end of file diff --git a/src/dune b/src/dune index 82e41aa..f9072c1 100644 --- a/src/dune +++ b/src/dune @@ -1,3 +1,3 @@ (library - (public_name dscheck) - (libraries containers oseq)) + (public_name dscheck) + (libraries containers oseq)) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index b39a777..bcf7da3 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -11,23 +11,28 @@ type _ Effect.t += | CompareAndSwap : ('a t * 'a * 'a) -> bool Effect.t | FetchAndAdd : (int t * int) -> int Effect.t -module IntSet = Set.Make( - struct - let compare = Stdlib.compare - type t = int - end ) +module IntSet = Set.Make (struct + let compare = Stdlib.compare -module IntMap = Map.Make( - struct - type t = int - let compare = Int.compare - end - ) + type t = int +end) -let _string_of_set s = - IntSet.fold (fun y x -> (string_of_int y) ^ "," ^ x) s "" +module IntMap = Map.Make (struct + type t = int -type atomic_op = Start | Make | Get | Set | Exchange | CompareAndSwap | FetchAndAdd + let compare = Int.compare +end) + +let _string_of_set s = IntSet.fold (fun y x -> string_of_int y ^ "," ^ x) s "" + +type atomic_op = + | Start + | Make + | Get + | Set + | Exchange + | CompareAndSwap + | FetchAndAdd let atomic_op_str x = match x with @@ -40,12 +45,11 @@ let atomic_op_str x = | FetchAndAdd -> "fetch_and_add" let tracing = ref false - let finished_processes = ref 0 type process_data = { - mutable next_op: atomic_op; - mutable next_repr: int option; + mutable next_op : atomic_op; + mutable next_repr : int option; mutable resume_func : (unit, unit) handler -> unit; mutable finished : bool; mutable discontinue_f : unit -> unit; @@ -57,43 +61,47 @@ let final_func = ref (fun () -> ()) (* Atomics implementation *) let atomics_counter = ref 1 -let make v = if !tracing then perform (Make v) else - begin - let i = !atomics_counter in - atomics_counter := !atomics_counter + 1; - (Atomic.make v, i) - end +let make v = + if !tracing then perform (Make v) + else + let i = !atomics_counter in + atomics_counter := !atomics_counter + 1; + (Atomic.make v, i) -let get r = if !tracing then perform (Get r) else match r with | (v,_) -> Atomic.get v +let get r = + if !tracing then perform (Get r) else match r with v, _ -> Atomic.get v -let set r v = if !tracing then perform (Set (r, v)) else match r with | (x,_) -> Atomic.set x v +let set r v = + if !tracing then perform (Set (r, v)) + else match r with x, _ -> Atomic.set x v let exchange r v = - if !tracing then perform (Exchange (r, v)) else match r with | (x,_) -> Atomic.exchange x v + if !tracing then perform (Exchange (r, v)) + else match r with x, _ -> Atomic.exchange x v let compare_and_set r seen v = if !tracing then perform (CompareAndSwap (r, seen, v)) - else match r with | (x,_) -> Atomic.compare_and_set x seen v + else match r with x, _ -> Atomic.compare_and_set x seen v let fetch_and_add r n = - if !tracing then perform (FetchAndAdd (r, n)) else match r with | (x,_) -> Atomic.fetch_and_add x n + if !tracing then perform (FetchAndAdd (r, n)) + else match r with x, _ -> Atomic.fetch_and_add x n let incr r = ignore (fetch_and_add r 1) - let decr r = ignore (fetch_and_add r (-1)) (* Tracing infrastructure *) exception Terminated_early -let discontinue k () = - discontinue_with k Terminated_early ({ - retc = (fun _ -> ()); - exnc = (function Terminated_early -> () | e -> raise e); - effc = (fun (type a) (_ : a Effect.t) -> None); - }) -;; - +let discontinue k () = + discontinue_with k Terminated_early + { + retc = (fun _ -> ()); + exnc = (function Terminated_early -> () | e -> raise e); + effc = (fun (type a) (_ : a Effect.t) -> None); + } + let processes = CCVector.create () let update_process_data process_id f op repr k = @@ -102,79 +110,96 @@ let update_process_data process_id f op repr k = process_rec.next_repr <- repr; process_rec.next_op <- op; process_rec.discontinue_f <- discontinue k -;; let finish_process process_id = let process_rec = CCVector.get processes process_id in process_rec.finished <- true; process_rec.discontinue_f <- (fun () -> ()); finished_processes := !finished_processes + 1 -;; let handler current_process_id runner = { retc = (fun _ -> - ( - finish_process current_process_id; - runner ())); + finish_process current_process_id; + runner ()); exnc = (fun s -> raise s); effc = (fun (type a) (e : a Effect.t) -> - match e with - | Make v -> - Some - (fun (k : (a, _) continuation) -> + match e with + | Make v -> + Some + (fun (k : (a, _) continuation) -> let i = !atomics_counter in let m = (Atomic.make v, i) in atomics_counter := !atomics_counter + 1; - update_process_data current_process_id (fun h -> continue_with k m h) Make (Some i) k; + update_process_data current_process_id + (fun h -> continue_with k m h) + Make (Some i) k; runner ()) - | Get (v,i) -> - Some - (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> continue_with k (Atomic.get v) h) Get (Some i) k; + | Get (v, i) -> + Some + (fun (k : (a, _) continuation) -> + update_process_data current_process_id + (fun h -> continue_with k (Atomic.get v) h) + Get (Some i) k; runner ()) - | Set ((r,i), v) -> - Some - (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> continue_with k (Atomic.set r v) h) Set (Some i) k; + | Set ((r, i), v) -> + Some + (fun (k : (a, _) continuation) -> + update_process_data current_process_id + (fun h -> continue_with k (Atomic.set r v) h) + Set (Some i) k; runner ()) - | Exchange ((a,i), b) -> - Some - (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> continue_with k (Atomic.exchange a b) h) Exchange (Some i) k; + | Exchange ((a, i), b) -> + Some + (fun (k : (a, _) continuation) -> + update_process_data current_process_id + (fun h -> continue_with k (Atomic.exchange a b) h) + Exchange (Some i) k; runner ()) - | CompareAndSwap ((x,i), s, v) -> - Some - (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> - continue_with k (Atomic.compare_and_set x s v) h) CompareAndSwap (Some i) k; + | CompareAndSwap ((x, i), s, v) -> + Some + (fun (k : (a, _) continuation) -> + update_process_data current_process_id + (fun h -> continue_with k (Atomic.compare_and_set x s v) h) + CompareAndSwap (Some i) k; runner ()) - | FetchAndAdd ((v,i), x) -> - Some - (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> - continue_with k (Atomic.fetch_and_add v x) h) FetchAndAdd (Some i) k; + | FetchAndAdd ((v, i), x) -> + Some + (fun (k : (a, _) continuation) -> + update_process_data current_process_id + (fun h -> continue_with k (Atomic.fetch_and_add v x) h) + FetchAndAdd (Some i) k; runner ()) - | _ -> - None); + | _ -> None); } let spawn f = let fiber_f = fiber f in let resume_func = continue_with fiber_f () in CCVector.push processes - { next_op = Start; next_repr = None; resume_func; finished = false; discontinue_f = discontinue fiber_f} + { + next_op = Start; + next_repr = None; + resume_func; + finished = false; + discontinue_f = discontinue fiber_f; + } let rec last_element l = - match l with - | h :: [] -> h - | [] -> assert(false) - | _ :: tl -> last_element tl + match l with h :: [] -> h | [] -> assert false | _ :: tl -> last_element tl + +type proc_rec = { proc_id : int; op : atomic_op; obj_ptr : int option } -type proc_rec = { proc_id: int; op: atomic_op; obj_ptr : int option } -type state_cell = { procs: proc_rec list; run_proc: int; run_op: atomic_op; run_ptr: int option; enabled : IntSet.t; mutable backtrack : IntSet.t } +type state_cell = { + procs : proc_rec list; + run_proc : int; + run_op : atomic_op; + run_ptr : int option; + enabled : IntSet.t; + mutable backtrack : IntSet.t; +} let num_runs = ref 0 @@ -182,7 +207,8 @@ let num_runs = ref 0 let schedule_for_checks = ref [] let do_run init_func init_schedule = - init_func (); (*set up run *) + init_func (); + (*set up run *) tracing := true; schedule_for_checks := init_schedule; (* cache the number of processes in case it's expensive*) @@ -193,58 +219,70 @@ let do_run init_func init_schedule = !every_func (); tracing := true; match s with - | [] -> if !finished_processes == num_processes then begin - tracing := false; - !final_func (); - tracing := true - end - | (process_id_to_run, next_op, next_ptr) :: schedule -> begin + | [] -> + if !finished_processes == num_processes then ( + tracing := false; + !final_func (); + tracing := true) + | (process_id_to_run, next_op, next_ptr) :: schedule -> if !finished_processes == num_processes then (* this should never happen *) - failwith("no enabled processes") + failwith "no enabled processes" else - begin - let process_to_run = CCVector.get processes process_id_to_run in - assert(process_to_run.next_op = next_op); - assert(process_to_run.next_repr = next_ptr); - process_to_run.resume_func (handler process_id_to_run (run_trace schedule)) - end - end + let process_to_run = CCVector.get processes process_id_to_run in + assert (process_to_run.next_op = next_op); + assert (process_to_run.next_repr = next_ptr); + process_to_run.resume_func + (handler process_id_to_run (run_trace schedule)) in tracing := true; run_trace init_schedule (); finished_processes := 0; tracing := false; num_runs := !num_runs + 1; - if !num_runs mod 1000 == 0 then - Printf.printf "run: %d\n%!" !num_runs; - let procs = CCVector.mapi (fun i p -> { proc_id = i; op = p.next_op; obj_ptr = p.next_repr }) processes |> CCVector.to_list in - let current_enabled = CCVector.to_seq processes - |> OSeq.zip_index - |> Seq.filter (fun (_,proc) -> not proc.finished) - |> Seq.map (fun (id,_) -> id) - |> IntSet.of_seq in + if !num_runs mod 1000 == 0 then Printf.printf "run: %d\n%!" !num_runs; + let procs = + CCVector.mapi + (fun i p -> { proc_id = i; op = p.next_op; obj_ptr = p.next_repr }) + processes + |> CCVector.to_list + in + let current_enabled = + CCVector.to_seq processes |> OSeq.zip_index + |> Seq.filter (fun (_, proc) -> not proc.finished) + |> Seq.map (fun (id, _) -> id) + |> IntSet.of_seq + in CCVector.iter (fun proc -> proc.discontinue_f ()) processes; CCVector.clear processes; atomics_counter := 1; match last_element init_schedule with - | (run_proc, run_op, run_ptr) -> - { procs; enabled = current_enabled; run_proc; run_op; run_ptr; backtrack = IntSet.empty } + | run_proc, run_op, run_ptr -> + { + procs; + enabled = current_enabled; + run_proc; + run_op; + run_ptr; + backtrack = IntSet.empty; + } let rec explore func state clock last_access = let s = last_element state in - List.iter (fun proc -> + 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 begin - let pre_s = List.nth state (i-1) 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 + 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 - end - ) s.procs; - if IntSet.cardinal s.enabled > 0 then begin + else pre_s.backtrack <- IntSet.union pre_s.backtrack pre_s.enabled) + s.procs; + if IntSet.cardinal s.enabled > 0 then ( let p = IntSet.min_elt s.enabled in let dones = ref IntSet.empty in s.backtrack <- IntSet.singleton p; @@ -252,50 +290,53 @@ let rec explore func state clock last_access = let j = IntSet.min_elt (IntSet.diff s.backtrack !dones) in dones := IntSet.add j !dones; let j_proc = List.nth s.procs j in - let schedule = (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 new_last_access = match j_proc.obj_ptr with Some(ptr) -> IntMap.add ptr state_time last_access | None -> last_access in + let schedule = + 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 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 - done - end - -let every f = - every_func := f + done) -let final f = - final_func := f +let every f = every_func := f +let final f = final_func := f let check f = let tracing_at_start = !tracing in tracing := false; - if not (f ()) then begin + if not (f ()) then ( Printf.printf "Found assertion violation at run %d:\n" !num_runs; - List.iter (fun s -> - begin match s with - | (last_run_proc, last_run_op, last_run_ptr) -> begin - 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 - end; - end; - ) !schedule_for_checks; - assert(false) - end; + 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; + assert false); tracing := tracing_at_start -let reset_state () = - finished_processes := 0; +let reset_state () = + finished_processes := 0; atomics_counter := 1; num_runs := 0; schedule_for_checks := []; - CCVector.clear processes; -;; - + CCVector.clear processes let trace func = reset_state (); - let empty_state = do_run func [(0, Start, None)] :: [] in + 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 diff --git a/src/tracedAtomic.mli b/src/tracedAtomic.mli index 3f6ee63..4e0b8e3 100644 --- a/src/tracedAtomic.mli +++ b/src/tracedAtomic.mli @@ -59,4 +59,4 @@ val final : (unit -> unit) -> unit (** run [f] after all processes complete *) val every : (unit -> unit) -> unit -(** run [f] between every possible interleaving *) \ No newline at end of file +(** run [f] between every possible interleaving *) diff --git a/tests/test_list.ml b/tests/test_list.ml index 8ed65b0..aceaa21 100644 --- a/tests/test_list.ml +++ b/tests/test_list.ml @@ -50,8 +50,7 @@ let test_list_naive domains () = | exception _ -> () | _ -> failwith "expected failure" -let test_list_safe () = - Atomic.trace (create_test add_node_safe 3) +let test_list_safe () = Atomic.trace (create_test add_node_safe 3) let () = let open Alcotest in @@ -59,7 +58,7 @@ let () = [ ( "list", [ - test_case "naive-1-domain" `Quick (test_list_naive_single_domain); + test_case "naive-1-domain" `Quick test_list_naive_single_domain; test_case "naive-2-domains" `Quick (test_list_naive 2); test_case "naive-8-domains" `Quick (test_list_naive 8); test_case "safe" `Quick test_list_safe; From be3f15de86cbda2913183cb1c2c5482455fb5a4a Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Mon, 13 Feb 2023 13:45:11 +0000 Subject: [PATCH 3/4] mark alcotest with-test --- dscheck.opam | 2 +- dune-project | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dscheck.opam b/dscheck.opam index 044fcb6..35ce478 100644 --- a/dscheck.opam +++ b/dscheck.opam @@ -11,7 +11,7 @@ depends: [ "dune" {>= "2.9"} "containers" "oseq" - "alcotest" {>= "1.6.0"} + "alcotest" {>= "1.6.0" & with-test} "odoc" {with-doc} ] build: [ diff --git a/dune-project b/dune-project index ddd2ce3..52f2b8a 100644 --- a/dune-project +++ b/dune-project @@ -11,6 +11,6 @@ (package (name dscheck) (synopsis "Traced Atomics") - (depends (ocaml (>= 5.0.0)) dune containers oseq (alcotest (>= 1.6.0)))) + (depends (ocaml (>= 5.0.0)) dune containers oseq (alcotest (and (>= 1.6.0) :with-test)))) From 12177fb47df1213b67b9de70096359bba98b5cec Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Thu, 23 Feb 2023 14:07:29 +0000 Subject: [PATCH 4/4] use Int module to create IntSet, IntMap --- src/tracedAtomic.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index bcf7da3..dc7de29 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -11,17 +11,9 @@ type _ Effect.t += | CompareAndSwap : ('a t * 'a * 'a) -> bool Effect.t | FetchAndAdd : (int t * int) -> int Effect.t -module IntSet = Set.Make (struct - let compare = Stdlib.compare +module IntSet = Set.Make (Int) - type t = int -end) - -module IntMap = Map.Make (struct - type t = int - - let compare = Int.compare -end) +module IntMap = Map.Make (Int) let _string_of_set s = IntSet.fold (fun y x -> string_of_int y ^ "," ^ x) s ""