From 621e48eff5a87692550ae79b0ca422a84e392952 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Fri, 30 Sep 2022 02:05:51 +0200 Subject: [PATCH 01/18] full replay only when necessary --- dscheck.opam | 1 + src/tracedAtomic.ml | 40 +++++++++++++++++++++++++++++----------- 2 files changed, 30 insertions(+), 11 deletions(-) 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..340b648 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -165,10 +165,15 @@ let num_runs = ref 0 (* we stash the current state in case a check fails and we need to log it *) let schedule_for_checks = ref [] -let do_run init_func init_schedule = - init_func (); (*set up run *) - tracing := true; +let setup_run func init_schedule = + atomics_counter := 1; + CCVector.clear processes; schedule_for_checks := init_schedule; + func () ; + num_runs := !num_runs + 1; + finished_processes := 0 + +let do_run init_schedule = (* cache the number of processes in case it's expensive*) let num_processes = CCVector.length processes in (* current number of ops we are through the current run *) @@ -197,9 +202,7 @@ let do_run init_func init_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 @@ -208,8 +211,6 @@ let do_run init_func init_schedule = |> Seq.filter (fun (_,proc) -> not proc.finished) |> Seq.map (fun (id,_) -> id) |> IntSet.of_seq in - 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 } @@ -231,12 +232,26 @@ let rec explore func state clock last_access = let p = IntSet.min_elt s.enabled in let dones = ref IntSet.empty in s.backtrack <- IntSet.singleton p; + let is_backtracking = ref false in while IntSet.(cardinal (diff s.backtrack !dones)) > 0 do 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 new_step = [(j, j_proc.op, j_proc.obj_ptr)] in + let full_schedule = List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state @ new_step in + let schedule = + if !is_backtracking + then begin + setup_run func full_schedule ; + full_schedule + end + else begin + is_backtracking := true ; + schedule_for_checks := full_schedule; + new_step + end + in + let statedash = state @ [do_run 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 @@ -278,7 +293,10 @@ let reset_state () = let trace func = reset_state (); - let empty_state = do_run func [(0, Start, None)] :: [] in + let schedule = [(0, Start, None)] in + setup_run func schedule ; + let empty_state = do_run schedule :: [] in let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty in - explore func empty_state empty_clock empty_last_access + explore func empty_state empty_clock empty_last_access ; + Printf.printf "Finished after %i runs.\n%!" !num_runs From b9f806ebd463dd2fee7e6ee7d603d3379e6d7e11 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Fri, 30 Sep 2022 02:15:13 +0200 Subject: [PATCH 02/18] list optims --- src/tracedAtomic.ml | 47 ++++++++++++++++++++------------------------- 1 file changed, 21 insertions(+), 26 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 340b648..bf40f4e 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -151,12 +151,6 @@ let spawn f = CCVector.push processes { next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } -let rec last_element l = - 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 state_cell = { procs: proc_rec list; run_proc: int; run_op: atomic_op; run_ptr: int option; enabled : IntSet.t; mutable backtrack : IntSet.t } @@ -201,7 +195,7 @@ let do_run init_schedule = end in tracing := true; - run_trace init_schedule (); + run_trace (List.rev init_schedule) (); tracing := false; if !num_runs mod 1000 == 0 then Printf.printf "run: %d\n%!" !num_runs; @@ -211,17 +205,16 @@ let do_run init_schedule = |> Seq.filter (fun (_,proc) -> not proc.finished) |> Seq.map (fun (id,_) -> id) |> IntSet.of_seq in - 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 } + let (run_proc, run_op, run_ptr) = List.hd init_schedule in + { 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 +let rec explore func time state current_schedule clock last_access = + let s = List.hd 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 begin - let pre_s = List.nth state (i-1) in + let pre_s = List.nth state (time - i + 1) in if IntSet.mem j pre_s.enabled then pre_s.backtrack <- IntSet.add j pre_s.backtrack else @@ -237,8 +230,8 @@ 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 new_step = [(j, j_proc.op, j_proc.obj_ptr)] in - let full_schedule = List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state @ new_step in + let new_step = (j, j_proc.op, j_proc.obj_ptr) in + let full_schedule = new_step :: current_schedule in let schedule = if !is_backtracking then begin @@ -248,14 +241,16 @@ let rec explore func state clock last_access = else begin is_backtracking := true ; schedule_for_checks := full_schedule; - new_step + [new_step] end in - let statedash = state @ [do_run 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 + let s = do_run schedule in + let new_state = s :: state in + let new_schedule = (s.run_proc, s.run_op, s.run_ptr) :: current_schedule in + let new_time = time + 1 in + let new_last_access = match j_proc.obj_ptr with Some(ptr) -> IntMap.add ptr new_time last_access | None -> last_access in + let new_clock = IntMap.add j new_time clock in + explore func new_time new_state new_schedule new_clock new_last_access done end @@ -277,7 +272,7 @@ let check f = Printf.printf "Process %d: %s %s\n" last_run_proc (atomic_op_str last_run_op) last_run_ptr end; end; - ) !schedule_for_checks; + ) (List.rev !schedule_for_checks) ; assert(false) end; tracing := tracing_at_start @@ -293,10 +288,10 @@ let reset_state () = let trace func = reset_state (); - let schedule = [(0, Start, None)] in - setup_run func schedule ; - let empty_state = do_run schedule :: [] in + let empty_schedule = [(0, Start, None)] in + setup_run func empty_schedule ; + let empty_state = do_run empty_schedule :: [] in let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty in - explore func empty_state empty_clock empty_last_access ; + explore func 1 empty_state empty_schedule empty_clock empty_last_access ; Printf.printf "Finished after %i runs.\n%!" !num_runs From a49718523d689ae30898695d7b693b38dc62f462 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Fri, 30 Sep 2022 03:11:55 +0200 Subject: [PATCH 03/18] more precise backtracking --- src/tracedAtomic.ml | 56 +++++++++++++++++++++++++++++++++++++-------- 1 file changed, 47 insertions(+), 9 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index bf40f4e..932069e 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -208,18 +208,42 @@ let do_run init_schedule = let (run_proc, run_op, run_ptr) = List.hd init_schedule in { procs; enabled = current_enabled; run_proc; run_op; run_ptr; backtrack = IntSet.empty } -let rec explore func time state current_schedule clock last_access = +type category = + | Ignore + | Read + | Write + | Read_write + +let categorize = function + | Start | Make -> Ignore + | Get -> Read + | Set | Exchange -> Write + | CompareAndSwap | FetchAndAdd -> Read_write + +let rec explore func time state current_schedule clock (last_read, last_write) = let s = List.hd 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 begin + let find ptr map = match IntMap.find_opt ptr map with + | None -> None + | Some lst -> + List.find_opt (fun (_, proc_id) -> proc_id <> j) lst + in + let i = match categorize proc.op, proc.obj_ptr with + | Ignore, _ -> None + | Read, Some ptr -> find ptr last_write + | Write, Some ptr -> find ptr last_read + | Read_write, Some ptr -> max (find ptr last_read) (find ptr last_write) + | _ -> assert false + in + match i with + | None -> () + | Some (i, _) -> let pre_s = List.nth state (time - 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 let p = IntSet.min_elt s.enabled in @@ -244,11 +268,25 @@ let rec explore func time state current_schedule clock last_access = [new_step] end in - let s = do_run schedule in - let new_state = s :: state in - let new_schedule = (s.run_proc, s.run_op, s.run_ptr) :: current_schedule in + let step = do_run schedule in + let new_state = step :: state in + let new_schedule = (step.run_proc, step.run_op, step.run_ptr) :: current_schedule in let new_time = time + 1 in - let new_last_access = match j_proc.obj_ptr with Some(ptr) -> IntMap.add ptr new_time last_access | None -> last_access in + let add ptr map = + IntMap.update + ptr + (function None -> Some [time, step.run_proc] + | Some steps -> Some ((time, step.run_proc) :: steps)) + map + in + let new_last_access = + match categorize step.run_op, step.run_ptr with + | Ignore, _ -> last_read, last_write + | Read, Some ptr -> add ptr last_read, last_write + | Write, Some ptr -> last_read, add ptr last_write + | Read_write, Some ptr -> add ptr last_read, add ptr last_write + | _ -> assert false + in let new_clock = IntMap.add j new_time clock in explore func new_time new_state new_schedule new_clock new_last_access done @@ -292,6 +330,6 @@ let trace func = setup_run func empty_schedule ; let empty_state = do_run empty_schedule :: [] in let empty_clock = IntMap.empty in - let empty_last_access = IntMap.empty in + let empty_last_access = IntMap.empty, IntMap.empty in explore func 1 empty_state empty_schedule empty_clock empty_last_access ; Printf.printf "Finished after %i runs.\n%!" !num_runs From 62c5e2e38fe81c41e9412be330f4f45008098152 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Fri, 30 Sep 2022 11:53:46 +0200 Subject: [PATCH 04/18] fixup num_runs --- src/tracedAtomic.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 932069e..4c11059 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -164,8 +164,10 @@ let setup_run func init_schedule = CCVector.clear processes; schedule_for_checks := init_schedule; func () ; + finished_processes := 0; num_runs := !num_runs + 1; - finished_processes := 0 + if !num_runs mod 1000 == 0 then + Printf.printf "run: %d\n" !num_runs let do_run init_schedule = (* cache the number of processes in case it's expensive*) @@ -197,8 +199,6 @@ let do_run init_schedule = tracing := true; run_trace (List.rev init_schedule) (); tracing := false; - 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 From 42d8418fcc314e24748a057fd41e097abf8053e9 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Fri, 30 Sep 2022 11:57:21 +0200 Subject: [PATCH 05/18] fixup backtrack --- src/tracedAtomic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 4c11059..7e8ca35 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -275,8 +275,8 @@ let rec explore func time state current_schedule clock (last_read, last_write) = let add ptr map = IntMap.update ptr - (function None -> Some [time, step.run_proc] - | Some steps -> Some ((time, step.run_proc) :: steps)) + (function None -> Some [new_time, step.run_proc] + | Some steps -> Some ((new_time, step.run_proc) :: steps)) map in let new_last_access = From 0252bf179d7c07992141f1ab5d695154e7140730 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Fri, 30 Sep 2022 12:32:20 +0200 Subject: [PATCH 06/18] backtracking: mark only last operation --- src/tracedAtomic.ml | 86 +++++++++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 42 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 7e8ca35..bd03dce 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -152,7 +152,7 @@ let spawn f = { next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } 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_rec; enabled : IntSet.t; mutable backtrack : IntSet.t } let num_runs = ref 0 @@ -183,7 +183,7 @@ let do_run init_schedule = !final_func (); tracing := true end - | (process_id_to_run, next_op, next_ptr) :: schedule -> begin + | { proc_id = process_id_to_run ; op = next_op ; obj_ptr = next_ptr } :: schedule -> begin if !finished_processes == num_processes then (* this should never happen *) failwith("no enabled processes") @@ -205,8 +205,8 @@ let do_run init_schedule = |> Seq.filter (fun (_,proc) -> not proc.finished) |> Seq.map (fun (id,_) -> id) |> IntSet.of_seq in - let (run_proc, run_op, run_ptr) = List.hd init_schedule in - { procs; enabled = current_enabled; run_proc; run_op; run_ptr; backtrack = IntSet.empty } + let last_run = List.hd init_schedule in + { procs; enabled = current_enabled; run = last_run ; backtrack = IntSet.empty } type category = | Ignore @@ -220,31 +220,32 @@ let categorize = function | Set | Exchange -> Write | CompareAndSwap | FetchAndAdd -> Read_write +let mark_backtrack proc time state (last_read, last_write) = + let j = proc.proc_id in + let find ptr map = match IntMap.find_opt ptr map with + | None -> None + | Some lst -> + List.find_opt (fun (_, proc_id) -> proc_id <> j) lst + in + let i = match categorize proc.op, proc.obj_ptr with + | Ignore, _ -> None + | Read, Some ptr -> find ptr last_write + | Write, Some ptr -> find ptr last_read + | Read_write, Some ptr -> max (find ptr last_read) (find ptr last_write) + | _ -> assert false + in + match i with + | None -> () + | Some (i, _) -> + assert (List.length state = time) ; + let pre_s = List.nth state (time - i) 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 rec explore func time state current_schedule clock (last_read, last_write) = let s = List.hd state in - List.iter (fun proc -> - let j = proc.proc_id in - let find ptr map = match IntMap.find_opt ptr map with - | None -> None - | Some lst -> - List.find_opt (fun (_, proc_id) -> proc_id <> j) lst - in - let i = match categorize proc.op, proc.obj_ptr with - | Ignore, _ -> None - | Read, Some ptr -> find ptr last_write - | Write, Some ptr -> find ptr last_read - | Read_write, Some ptr -> max (find ptr last_read) (find ptr last_write) - | _ -> assert false - in - match i with - | None -> () - | Some (i, _) -> - let pre_s = List.nth state (time - 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 - ) s.procs; if IntSet.cardinal s.enabled > 0 then begin let p = IntSet.min_elt s.enabled in let dones = ref IntSet.empty in @@ -254,7 +255,7 @@ let rec explore func time state current_schedule clock (last_read, last_write) = 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 new_step = (j, j_proc.op, j_proc.obj_ptr) in + let new_step = j_proc in let full_schedule = new_step :: current_schedule in let schedule = if !is_backtracking @@ -269,18 +270,19 @@ let rec explore func time state current_schedule clock (last_read, last_write) = end in let step = do_run schedule in + mark_backtrack step.run time state (last_read, last_write); let new_state = step :: state in - let new_schedule = (step.run_proc, step.run_op, step.run_ptr) :: current_schedule in + let new_schedule = step.run :: current_schedule in let new_time = time + 1 in let add ptr map = IntMap.update ptr - (function None -> Some [new_time, step.run_proc] - | Some steps -> Some ((new_time, step.run_proc) :: steps)) + (function None -> Some [time, step.run.proc_id] + | Some steps -> Some ((time, step.run.proc_id) :: steps)) map in let new_last_access = - match categorize step.run_op, step.run_ptr with + match categorize step.run.op, step.run.obj_ptr with | Ignore, _ -> last_read, last_write | Read, Some ptr -> add ptr last_read, last_write | Write, Some ptr -> last_read, add ptr last_write @@ -303,13 +305,9 @@ let check f = tracing := false; if not (f ()) then begin 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; + List.iter (fun { proc_id ; op ; obj_ptr } -> + let last_run_ptr = Option.map string_of_int obj_ptr |> Option.value ~default:"" in + Printf.printf "Process %d: %s %s\n" proc_id (atomic_op_str op) last_run_ptr ) (List.rev !schedule_for_checks) ; assert(false) end; @@ -326,10 +324,14 @@ let reset_state () = let trace func = reset_state (); - let empty_schedule = [(0, Start, None)] in + let empty_schedule = [{ proc_id = 0 ; op = Start ; obj_ptr = None }] in setup_run func empty_schedule ; let empty_state = do_run empty_schedule :: [] in let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty, IntMap.empty in - explore func 1 empty_state empty_schedule empty_clock empty_last_access ; - Printf.printf "Finished after %i runs.\n%!" !num_runs + explore func 1 empty_state empty_schedule empty_clock empty_last_access + +let trace func = + Fun.protect + (fun () -> trace func) + ~finally:(fun () -> Printf.printf "Finished after %i runs.\n%!" !num_runs) From 5b606bbc579a0499178ee41b3ec7246696c1c9ea Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 1 Oct 2022 11:51:51 +0200 Subject: [PATCH 07/18] big bad backtracking steps --- src/tracedAtomic.ml | 76 ++++++++++++++++++++++++++++----------------- 1 file changed, 48 insertions(+), 28 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index bd03dce..a08f35b 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -152,7 +152,12 @@ let spawn f = { next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } type proc_rec = { proc_id: int; op: atomic_op; obj_ptr : int option } -type state_cell = { procs: proc_rec list; run: proc_rec; enabled : IntSet.t; mutable backtrack : IntSet.t } +type state_cell = { + procs : proc_rec list; + run : proc_rec; + enabled : IntSet.t; + mutable backtrack : proc_rec list IntMap.t; +} let num_runs = ref 0 @@ -167,7 +172,7 @@ let setup_run func init_schedule = finished_processes := 0; num_runs := !num_runs + 1; if !num_runs mod 1000 == 0 then - Printf.printf "run: %d\n" !num_runs + Printf.printf "run: %d\n%!" !num_runs let do_run init_schedule = (* cache the number of processes in case it's expensive*) @@ -206,7 +211,7 @@ let do_run init_schedule = |> Seq.map (fun (id,_) -> id) |> IntSet.of_seq in let last_run = List.hd init_schedule in - { procs; enabled = current_enabled; run = last_run ; backtrack = IntSet.empty } + { procs; enabled = current_enabled; run = last_run ; backtrack = IntMap.empty } type category = | Ignore @@ -220,65 +225,80 @@ let categorize = function | Set | Exchange -> Write | CompareAndSwap | FetchAndAdd -> Read_write -let mark_backtrack proc time state (last_read, last_write) = +let mark_backtrack ~is_last proc time state (last_read, last_write) = let j = proc.proc_id in let find ptr map = match IntMap.find_opt ptr map with | None -> None | Some lst -> List.find_opt (fun (_, proc_id) -> proc_id <> j) lst in - let i = match categorize proc.op, proc.obj_ptr with + let find_loc ~is_last proc = + match categorize proc.op, proc.obj_ptr with | Ignore, _ -> None | Read, Some ptr -> find ptr last_write - | Write, Some ptr -> find ptr last_read - | Read_write, Some ptr -> max (find ptr last_read) (find ptr last_write) + | Write, Some ptr when not is_last -> find ptr last_read + | (Write | Read_write), Some ptr -> max (find ptr last_read) (find ptr last_write) | _ -> assert false in - match i with + match find_loc ~is_last proc with | None -> () | Some (i, _) -> assert (List.length state = time) ; - let pre_s = List.nth state (time - i) in - if IntSet.mem j pre_s.enabled then - pre_s.backtrack <- IntSet.add j pre_s.backtrack + let pre_s = List.nth state (time - i + 1) in + if IntSet.mem j pre_s.enabled then begin + let replay_steps = List.filteri (fun k s -> k <= time - i && s.run.proc_id = j) state in + let replay_steps = List.map (fun s -> s.run) replay_steps in + let todo = + match IntMap.find_opt j pre_s.backtrack with + | None -> true + | Some lst -> List.length lst > List.length replay_steps + in + let causal p = match find_loc ~is_last:false p with None -> true | Some (k, _) -> k <= i in + if todo && List.for_all causal replay_steps + then pre_s.backtrack <- IntMap.add j replay_steps pre_s.backtrack + end else - pre_s.backtrack <- IntSet.union pre_s.backtrack pre_s.enabled + failwith "TODO: currently untested" + +let map_diff_set map set = + IntMap.filter (fun key _ -> not (IntSet.mem key set)) map let rec explore func time state current_schedule clock (last_read, last_write) = let s = List.hd state in if IntSet.cardinal s.enabled > 0 then begin let p = IntSet.min_elt s.enabled in + let init_step = List.nth s.procs p in let dones = ref IntSet.empty in - s.backtrack <- IntSet.singleton p; + s.backtrack <- IntMap.singleton p [init_step] ; let is_backtracking = ref false in - while IntSet.(cardinal (diff s.backtrack !dones)) > 0 do - let j = IntSet.min_elt (IntSet.diff s.backtrack !dones) in + while IntMap.(cardinal (map_diff_set s.backtrack !dones)) > 0 do + let j, new_step = IntMap.min_binding (map_diff_set s.backtrack !dones) in dones := IntSet.add j !dones; - let j_proc = List.nth s.procs j in - let new_step = j_proc in - let full_schedule = new_step :: current_schedule in + let new_schedule = List.rev_append (List.rev new_step) current_schedule in let schedule = if !is_backtracking then begin - setup_run func full_schedule ; - full_schedule + setup_run func new_schedule ; + new_schedule end else begin is_backtracking := true ; - schedule_for_checks := full_schedule; - [new_step] + schedule_for_checks := new_schedule; + new_step end in let step = do_run schedule in - mark_backtrack step.run time state (last_read, last_write); - let new_state = step :: state in - let new_schedule = step.run :: current_schedule in - let new_time = time + 1 in + let new_state = + List.map (fun run -> { step with run; backtrack = IntMap.empty }) new_step + @ state + in + let new_time = time + List.length new_step in + mark_backtrack ~is_last:(IntSet.is_empty step.enabled) step.run new_time new_state (last_read, last_write); let add ptr map = IntMap.update ptr - (function None -> Some [time, step.run.proc_id] - | Some steps -> Some ((time, step.run.proc_id) :: steps)) + (function None -> Some [new_time, step.run.proc_id] + | Some steps -> Some ((new_time, step.run.proc_id) :: steps)) map in let new_last_access = From 4e6f1b316df0c867b539f6f56201229ed90f4a4a Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 1 Oct 2022 11:59:28 +0200 Subject: [PATCH 08/18] add simple test --- tests/dune | 5 +++++ tests/test_simple.ml | 16 ++++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 tests/test_simple.ml diff --git a/tests/dune b/tests/dune index db241a0..5edece8 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_simple) + (libraries dscheck) + (modules test_simple)) diff --git a/tests/test_simple.ml b/tests/test_simple.ml new file mode 100644 index 0000000..7689270 --- /dev/null +++ b/tests/test_simple.ml @@ -0,0 +1,16 @@ +module Atomic = Dscheck.TracedAtomic + +(* Example from ocaml-parrafuzz presentation at the OCaml Workshop 2021: + https://www.youtube.com/watch?v=GZsUoSaIpIs *) + +let test i = + let x = Atomic.make i in + let y = Atomic.make 0 in + Atomic.spawn (fun () -> if Atomic.get x = 10 then Atomic.set y 2) ; + Atomic.spawn (fun () -> Atomic.set x 0 ; Atomic.set y 1) ; + Atomic.final (fun () -> Atomic.check (fun () -> Atomic.get y <> 2)) + +let () = + Atomic.trace (fun () -> test 0) ; + Printf.printf "\n-----------------------------\n\n%!" ; + Atomic.trace (fun () -> test 10) From e68277be94095cb6c2ebbe6fd9e4dd3ed1b60cf3 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 1 Oct 2022 15:26:47 +0200 Subject: [PATCH 09/18] fix: allow backtracking inside big steps --- src/tracedAtomic.ml | 131 +++++++++++++++++++++++++------------------- 1 file changed, 74 insertions(+), 57 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index a08f35b..3033b7b 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -172,7 +172,7 @@ let setup_run func init_schedule = finished_processes := 0; num_runs := !num_runs + 1; if !num_runs mod 1000 == 0 then - Printf.printf "run: %d\n%!" !num_runs + Format.printf "run: %d@." !num_runs let do_run init_schedule = (* cache the number of processes in case it's expensive*) @@ -211,7 +211,7 @@ let do_run init_schedule = |> Seq.map (fun (id,_) -> id) |> IntSet.of_seq in let last_run = List.hd init_schedule in - { procs; enabled = current_enabled; run = last_run ; backtrack = IntMap.empty } + { procs; enabled = current_enabled; run = last_run; backtrack = IntMap.empty } type category = | Ignore @@ -253,9 +253,11 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = | None -> true | Some lst -> List.length lst > List.length replay_steps in - let causal p = match find_loc ~is_last:false p with None -> true | Some (k, _) -> k <= i in + let causal p = match find_loc ~is_last:false p with + | None -> true + | Some (k, _) -> k <= i in if todo && List.for_all causal replay_steps - then pre_s.backtrack <- IntMap.add j replay_steps pre_s.backtrack + then pre_s.backtrack <- IntMap.add j (List.rev replay_steps) pre_s.backtrack end else failwith "TODO: currently untested" @@ -263,56 +265,70 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = let map_diff_set map set = IntMap.filter (fun key _ -> not (IntSet.mem key set)) map -let rec explore func time state current_schedule clock (last_read, last_write) = +let rec explore func time state (explored, state_planned) current_schedule clock (last_read, last_write) = let s = List.hd state in - if IntSet.cardinal s.enabled > 0 then begin - let p = IntSet.min_elt s.enabled in - let init_step = List.nth s.procs p in - let dones = ref IntSet.empty in - s.backtrack <- IntMap.singleton p [init_step] ; - let is_backtracking = ref false in - while IntMap.(cardinal (map_diff_set s.backtrack !dones)) > 0 do - let j, new_step = IntMap.min_binding (map_diff_set s.backtrack !dones) in - dones := IntSet.add j !dones; - let new_schedule = List.rev_append (List.rev new_step) current_schedule in - let schedule = - if !is_backtracking - then begin - setup_run func new_schedule ; - new_schedule - end - else begin - is_backtracking := true ; - schedule_for_checks := new_schedule; - new_step - end - in - let step = do_run schedule in - let new_state = - List.map (fun run -> { step with run; backtrack = IntMap.empty }) new_step - @ state - in - let new_time = time + List.length new_step in - mark_backtrack ~is_last:(IntSet.is_empty step.enabled) step.run new_time new_state (last_read, last_write); - let add ptr map = - IntMap.update - ptr - (function None -> Some [new_time, step.run.proc_id] - | Some steps -> Some ((new_time, step.run.proc_id) :: steps)) - map - in - let new_last_access = - match categorize step.run.op, step.run.obj_ptr with - | Ignore, _ -> last_read, last_write - | Read, Some ptr -> add ptr last_read, last_write - | Write, Some ptr -> last_read, add ptr last_write - | Read_write, Some ptr -> add ptr last_read, add ptr last_write - | _ -> assert false - in - let new_clock = IntMap.add j new_time clock in - explore func new_time new_state new_schedule new_clock new_last_access - done - end + assert (IntMap.is_empty s.backtrack) ; + let dones = ref IntSet.empty in + begin match state_planned with + | [] -> + if IntSet.cardinal s.enabled > 0 then begin + let p = IntSet.min_elt s.enabled in + let init_step = List.nth s.procs p in + s.backtrack <- IntMap.singleton p [init_step] ; + end + | { proc_id ; _ } :: _ -> + dones := explored ; + s.backtrack <- IntMap.singleton proc_id state_planned + end ; + let is_backtracking = ref false in + while IntMap.(cardinal (map_diff_set s.backtrack !dones)) > 0 do + let j, new_steps = IntMap.min_binding (map_diff_set s.backtrack !dones) in + let new_explored = + if !is_backtracking || state_planned <> [] then !dones else IntSet.empty in + dones := IntSet.add j !dones; + let new_step, new_state_planned = + match new_steps with + | [] -> assert false + | next :: future -> next, future + in + let new_schedule = new_step :: current_schedule in + let schedule = + if !is_backtracking + then begin + setup_run func new_schedule ; + new_schedule + end + else begin + is_backtracking := true ; + schedule_for_checks := new_schedule; + [new_step] + end + in + let step = do_run schedule in + let new_state = + { step with run = new_step ; backtrack = IntMap.empty } + :: state + in + let new_time = time + 1 in + mark_backtrack ~is_last:(IntSet.is_empty step.enabled) step.run new_time new_state (last_read, last_write); + let add ptr map = + IntMap.update + ptr + (function None -> Some [new_time, step.run.proc_id] + | Some steps -> Some ((new_time, step.run.proc_id) :: steps)) + map + in + let new_last_access = + match categorize step.run.op, step.run.obj_ptr with + | Ignore, _ -> last_read, last_write + | Read, Some ptr -> add ptr last_read, last_write + | Write, Some ptr -> last_read, add ptr last_write + | Read_write, Some ptr -> add ptr last_read, add ptr last_write + | _ -> assert false + in + let new_clock = IntMap.add j new_time clock in + explore func new_time new_state (new_explored, new_state_planned) new_schedule new_clock new_last_access + done let every f = every_func := f @@ -324,10 +340,10 @@ let check f = let tracing_at_start = !tracing in tracing := false; if not (f ()) then begin - Printf.printf "Found assertion violation at run %d:\n" !num_runs; + Format.printf "@.@.Found assertion violation at run %d:@." !num_runs; List.iter (fun { proc_id ; op ; obj_ptr } -> let last_run_ptr = Option.map string_of_int obj_ptr |> Option.value ~default:"" in - Printf.printf "Process %d: %s %s\n" proc_id (atomic_op_str op) last_run_ptr + Format.printf " Process %d: %s %s@." proc_id (atomic_op_str op) last_run_ptr ) (List.rev !schedule_for_checks) ; assert(false) end; @@ -347,11 +363,12 @@ let trace func = let empty_schedule = [{ proc_id = 0 ; op = Start ; obj_ptr = None }] in setup_run func empty_schedule ; let empty_state = do_run empty_schedule :: [] in + let empty_state_planned = (IntSet.empty, []) in let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty, IntMap.empty in - explore func 1 empty_state empty_schedule empty_clock empty_last_access + explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access let trace func = Fun.protect (fun () -> trace func) - ~finally:(fun () -> Printf.printf "Finished after %i runs.\n%!" !num_runs) + ~finally:(fun () -> Format.printf "@.Finished after %i runs.@." !num_runs) From b923d3bc41d4ec8ed3f8044e3b4139ad0da8cdb6 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 1 Oct 2022 15:32:49 +0200 Subject: [PATCH 10/18] fix: print replay trace for all unhandled errors --- src/tracedAtomic.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 3033b7b..6646c62 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -336,16 +336,18 @@ let every f = let final f = final_func := f +let print_trace () = + List.iter (fun { proc_id ; op ; obj_ptr } -> + let last_run_ptr = Option.map string_of_int obj_ptr |> Option.value ~default:"" in + Format.printf " Process %d: %s %s@." proc_id (atomic_op_str op) last_run_ptr + ) (List.rev !schedule_for_checks) + let check f = let tracing_at_start = !tracing in tracing := false; if not (f ()) then begin - Format.printf "@.@.Found assertion violation at run %d:@." !num_runs; - List.iter (fun { proc_id ; op ; obj_ptr } -> - let last_run_ptr = Option.map string_of_int obj_ptr |> Option.value ~default:"" in - Format.printf " Process %d: %s %s@." proc_id (atomic_op_str op) last_run_ptr - ) (List.rev !schedule_for_checks) ; - assert(false) + Format.printf "Check: found assertion violation!@." ; + assert false end; tracing := tracing_at_start @@ -366,7 +368,12 @@ let trace func = let empty_state_planned = (IntSet.empty, []) in let empty_clock = IntMap.empty in let empty_last_access = IntMap.empty, IntMap.empty in - explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access + try explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access + with exn -> + Format.printf "Found error at run %d:@." !num_runs; + print_trace () ; + Format.printf "Unhandled exception: %s@." (Printexc.to_string exn) ; + Printexc.print_backtrace stdout let trace func = Fun.protect From 92d60155b840fba199338aade21bd3558652e202 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 1 Oct 2022 16:04:30 +0200 Subject: [PATCH 11/18] stable domains/atomics identifiers --- dscheck.opam | 2 - dune-project | 4 +- src/dune | 3 +- src/tracedAtomic.ml | 209 ++++++++++++++++++++++--------------------- tests/test_simple.ml | 3 +- 5 files changed, 112 insertions(+), 109 deletions(-) diff --git a/dscheck.opam b/dscheck.opam index 044fcb6..a46212f 100644 --- a/dscheck.opam +++ b/dscheck.opam @@ -9,8 +9,6 @@ bug-reports: "https://github.com/ocaml-multicore/dscheck/issues" depends: [ "ocaml" {>= "5.0.0"} "dune" {>= "2.9"} - "containers" - "oseq" "alcotest" {>= "1.6.0"} "odoc" {with-doc} ] diff --git a/dune-project b/dune-project index ddd2ce3..318d387 100644 --- a/dune-project +++ b/dune-project @@ -11,6 +11,4 @@ (package (name dscheck) (synopsis "Traced Atomics") - (depends (ocaml (>= 5.0.0)) dune containers oseq (alcotest (>= 1.6.0)))) - - + (depends (ocaml (>= 5.0.0)) dune (alcotest (>= 1.6.0)))) diff --git a/src/dune b/src/dune index 82e41aa..eef9f13 100644 --- a/src/dune +++ b/src/dune @@ -1,3 +1,2 @@ (library - (public_name dscheck) - (libraries containers oseq)) + (public_name dscheck)) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 6646c62..5d74ef0 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -1,7 +1,16 @@ open Effect open Effect.Shallow -type 'a t = 'a Atomic.t * int +module Uid = struct + type t = int list + let compare = List.compare Int.compare + let to_string t = String.concat "," (List.map string_of_int t) +end + +module IdSet = Set.Make (Uid) +module IdMap = Map.Make (Uid) + +type 'a t = 'a Atomic.t * Uid.t type _ Effect.t += | Make : 'a -> 'a t Effect.t @@ -10,24 +19,9 @@ type _ Effect.t += | Exchange : ('a t * 'a) -> 'a Effect.t | CompareAndSwap : ('a t * 'a * 'a) -> bool Effect.t | FetchAndAdd : (int t * int) -> int Effect.t + | Spawn : (unit -> unit) -> unit Effect.t -module IntSet = Set.Make( - struct - let compare = Stdlib.compare - type t = int - end ) - -module IntMap = Map.Make( - struct - type t = int - 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 +type atomic_op = Start | Make | Get | Set | Exchange | CompareAndSwap | FetchAndAdd | Spawn let atomic_op_str x = match x with @@ -38,14 +32,18 @@ let atomic_op_str x = | Exchange -> "exchange" | CompareAndSwap -> "compare_and_swap" | FetchAndAdd -> "fetch_and_add" + | Spawn -> "spawn" let tracing = ref false let finished_processes = ref 0 type process_data = { + uid : Uid.t; + mutable domain_generator : int; + mutable atomic_generator : int; mutable next_op: atomic_op; - mutable next_repr: int option; + mutable next_repr: Uid.t option; mutable resume_func : (unit, unit) handler -> unit; mutable finished : bool; } @@ -54,13 +52,13 @@ let every_func = ref (fun () -> ()) let final_func = ref (fun () -> ()) (* Atomics implementation *) -let atomics_counter = ref 1 +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) + atomics_counter := !atomics_counter - 1; + (Atomic.make v, [i]) end let get r = if !tracing then perform (Get r) else match r with | (v,_) -> Atomic.get v @@ -82,25 +80,30 @@ let incr r = ignore (fetch_and_add r 1) let decr r = ignore (fetch_and_add r (-1)) (* Tracing infrastructure *) -let processes = CCVector.create () +let processes = ref IdMap.empty +let push_process p = + assert (not (IdMap.mem p.uid !processes)) ; + processes := IdMap.add p.uid p !processes + +let get_process id = IdMap.find id !processes let update_process_data process_id f op repr = - let process_rec = CCVector.get processes process_id in + let process_rec = get_process process_id in process_rec.resume_func <- f; process_rec.next_repr <- repr; process_rec.next_op <- op let finish_process process_id = - let process_rec = CCVector.get processes process_id in + let process_rec = get_process process_id in process_rec.finished <- true; finished_processes := !finished_processes + 1 -let handler current_process_id runner = +let handler current_process runner = { retc = (fun _ -> ( - finish_process current_process_id; + finish_process current_process.uid; runner ())); exnc = (fun s -> raise s); effc = @@ -109,54 +112,62 @@ let handler current_process_id runner = | Make v -> Some (fun (k : (a, _) continuation) -> - let i = !atomics_counter in + let i = current_process.atomic_generator :: current_process.uid in + current_process.atomic_generator <- current_process.atomic_generator + 1 ; 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.uid (fun h -> continue_with k m h) Make (Some i); 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.uid (fun h -> continue_with k (Atomic.get v) h) Get (Some i); 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.uid (fun h -> continue_with k (Atomic.set r v) h) Set (Some i); 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.uid (fun h -> continue_with k (Atomic.exchange a b) h) Exchange (Some i); runner ()) | CompareAndSwap ((x,i), s, v) -> Some (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> + update_process_data current_process.uid (fun h -> continue_with k (Atomic.compare_and_set x s v) h) CompareAndSwap (Some i); runner ()) | FetchAndAdd ((v,i), x) -> Some (fun (k : (a, _) continuation) -> - update_process_data current_process_id (fun h -> + update_process_data current_process.uid (fun h -> continue_with k (Atomic.fetch_and_add v x) h) FetchAndAdd (Some i); runner ()) + | Spawn f -> + Some + (fun (k : (a, _) continuation) -> + let fiber_f h = continue_with (fiber f) () h in + let uid = current_process.domain_generator :: current_process.uid in + current_process.domain_generator <- current_process.domain_generator + 1 ; + push_process + { uid; domain_generator = 0; atomic_generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } ; + update_process_data current_process.uid (fun h -> + continue_with k () h) Spawn (Some uid); + runner ()) | _ -> None); } let spawn f = - let fiber_f h = - continue_with (fiber f) () h in - CCVector.push processes - { next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } + if !tracing then perform (Spawn f) else failwith "spawn outside tracing" -type proc_rec = { proc_id: int; op: atomic_op; obj_ptr : int option } +type proc_rec = { proc_id: Uid.t; op: atomic_op; obj_ptr : Uid.t option } type state_cell = { - procs : proc_rec list; + procs : proc_rec IdMap.t; run : proc_rec; - enabled : IntSet.t; - mutable backtrack : proc_rec list IntMap.t; + enabled : IdSet.t; + mutable backtrack : proc_rec list IdMap.t; } let num_runs = ref 0 @@ -165,53 +176,51 @@ let num_runs = ref 0 let schedule_for_checks = ref [] let setup_run func init_schedule = - atomics_counter := 1; - CCVector.clear processes; - schedule_for_checks := init_schedule; - func () ; + processes := IdMap.empty ; finished_processes := 0; + schedule_for_checks := init_schedule; + tracing := true; + let uid = [] in + let fiber_f h = continue_with (fiber func) () h in + push_process + { uid; domain_generator = 0; atomic_generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } ; + tracing := false; num_runs := !num_runs + 1; if !num_runs mod 1000 == 0 then Format.printf "run: %d@." !num_runs let do_run init_schedule = - (* cache the number of processes in case it's expensive*) - let num_processes = CCVector.length processes in - (* current number of ops we are through the current run *) let rec run_trace s () = tracing := false; !every_func (); tracing := true; match s with - | [] -> if !finished_processes == num_processes then begin + | [] -> if !finished_processes == IdMap.cardinal !processes then begin tracing := false; !final_func (); tracing := true end - | { proc_id = process_id_to_run ; op = next_op ; obj_ptr = next_ptr } :: schedule -> begin - if !finished_processes == num_processes then - (* this should never happen *) - 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 + | { proc_id = process_id_to_run ; op = next_op ; obj_ptr = next_ptr } :: schedule -> + let process_to_run = get_process process_id_to_run in + assert(not process_to_run.finished); + assert(process_to_run.next_op = next_op); + assert(process_to_run.next_repr = next_ptr); + process_to_run.resume_func (handler process_to_run (run_trace schedule)) in tracing := true; run_trace (List.rev init_schedule) (); tracing := false; - 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 + let procs = + IdMap.mapi (fun i p -> { proc_id = i; op = p.next_op; obj_ptr = p.next_repr }) !processes + in + let current_enabled = + IdMap.to_seq !processes + |> Seq.filter (fun (_, p) -> not p.finished) + |> Seq.map (fun (id, _) -> id) + |> IdSet.of_seq + in let last_run = List.hd init_schedule in - { procs; enabled = current_enabled; run = last_run; backtrack = IntMap.empty } + { procs; enabled = current_enabled; run = last_run; backtrack = IdMap.empty } type category = | Ignore @@ -220,14 +229,14 @@ type category = | Read_write let categorize = function - | Start | Make -> Ignore + | Spawn | Start | Make -> Ignore | Get -> Read | Set | Exchange -> Write | CompareAndSwap | FetchAndAdd -> Read_write let mark_backtrack ~is_last proc time state (last_read, last_write) = let j = proc.proc_id in - let find ptr map = match IntMap.find_opt ptr map with + let find ptr map = match IdMap.find_opt ptr map with | None -> None | Some lst -> List.find_opt (fun (_, proc_id) -> proc_id <> j) lst @@ -245,11 +254,11 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = | Some (i, _) -> assert (List.length state = time) ; let pre_s = List.nth state (time - i + 1) in - if IntSet.mem j pre_s.enabled then begin + if IdSet.mem j pre_s.enabled then begin let replay_steps = List.filteri (fun k s -> k <= time - i && s.run.proc_id = j) state in let replay_steps = List.map (fun s -> s.run) replay_steps in let todo = - match IntMap.find_opt j pre_s.backtrack with + match IdMap.find_opt j pre_s.backtrack with | None -> true | Some lst -> List.length lst > List.length replay_steps in @@ -257,35 +266,35 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = | None -> true | Some (k, _) -> k <= i in if todo && List.for_all causal replay_steps - then pre_s.backtrack <- IntMap.add j (List.rev replay_steps) pre_s.backtrack + then pre_s.backtrack <- IdMap.add j (List.rev replay_steps) pre_s.backtrack end else - failwith "TODO: currently untested" + () (* failwith "TODO: currently untested" *) let map_diff_set map set = - IntMap.filter (fun key _ -> not (IntSet.mem key set)) map + IdMap.filter (fun key _ -> not (IdSet.mem key set)) map let rec explore func time state (explored, state_planned) current_schedule clock (last_read, last_write) = let s = List.hd state in - assert (IntMap.is_empty s.backtrack) ; - let dones = ref IntSet.empty in + assert (IdMap.is_empty s.backtrack) ; + let dones = ref IdSet.empty in begin match state_planned with | [] -> - if IntSet.cardinal s.enabled > 0 then begin - let p = IntSet.min_elt s.enabled in - let init_step = List.nth s.procs p in - s.backtrack <- IntMap.singleton p [init_step] ; + if IdSet.cardinal s.enabled > 0 then begin + let p = IdSet.min_elt s.enabled in + let init_step = IdMap.find p s.procs in + s.backtrack <- IdMap.singleton p [init_step] ; end | { proc_id ; _ } :: _ -> dones := explored ; - s.backtrack <- IntMap.singleton proc_id state_planned + s.backtrack <- IdMap.singleton proc_id state_planned end ; let is_backtracking = ref false in - while IntMap.(cardinal (map_diff_set s.backtrack !dones)) > 0 do - let j, new_steps = IntMap.min_binding (map_diff_set s.backtrack !dones) in + while IdMap.(cardinal (map_diff_set s.backtrack !dones)) > 0 do + let j, new_steps = IdMap.min_binding (map_diff_set s.backtrack !dones) in let new_explored = - if !is_backtracking || state_planned <> [] then !dones else IntSet.empty in - dones := IntSet.add j !dones; + if !is_backtracking || state_planned <> [] then !dones else IdSet.empty in + dones := IdSet.add j !dones; let new_step, new_state_planned = match new_steps with | [] -> assert false @@ -306,13 +315,13 @@ let rec explore func time state (explored, state_planned) current_schedule clock in let step = do_run schedule in let new_state = - { step with run = new_step ; backtrack = IntMap.empty } + { step with run = new_step ; backtrack = IdMap.empty } :: state in let new_time = time + 1 in - mark_backtrack ~is_last:(IntSet.is_empty step.enabled) step.run new_time new_state (last_read, last_write); + mark_backtrack ~is_last:(IdSet.is_empty step.enabled) step.run new_time new_state (last_read, last_write); let add ptr map = - IntMap.update + IdMap.update ptr (function None -> Some [new_time, step.run.proc_id] | Some steps -> Some ((new_time, step.run.proc_id) :: steps)) @@ -326,7 +335,7 @@ let rec explore func time state (explored, state_planned) current_schedule clock | Read_write, Some ptr -> add ptr last_read, add ptr last_write | _ -> assert false in - let new_clock = IntMap.add j new_time clock in + let new_clock = IdMap.add j new_time clock in explore func new_time new_state (new_explored, new_state_planned) new_schedule new_clock new_last_access done @@ -338,8 +347,8 @@ let final f = let print_trace () = List.iter (fun { proc_id ; op ; obj_ptr } -> - let last_run_ptr = Option.map string_of_int obj_ptr |> Option.value ~default:"" in - Format.printf " Process %d: %s %s@." proc_id (atomic_op_str op) last_run_ptr + let last_run_ptr = Option.map Uid.to_string obj_ptr |> Option.value ~default:"" in + Format.printf " Process %s: %s %s@." (Uid.to_string proc_id) (atomic_op_str op) last_run_ptr ) (List.rev !schedule_for_checks) let check f = @@ -356,18 +365,16 @@ let reset_state () = atomics_counter := 1; num_runs := 0; schedule_for_checks := []; - CCVector.clear processes; -;; - + processes := IdMap.empty let trace func = reset_state (); - let empty_schedule = [{ proc_id = 0 ; op = Start ; obj_ptr = None }] in + let empty_schedule = [{ proc_id = [] ; op = Start ; obj_ptr = None }] in setup_run func empty_schedule ; let empty_state = do_run empty_schedule :: [] in - let empty_state_planned = (IntSet.empty, []) in - let empty_clock = IntMap.empty in - let empty_last_access = IntMap.empty, IntMap.empty in + let empty_state_planned = (IdSet.empty, []) in + let empty_clock = IdMap.empty in + let empty_last_access = IdMap.empty, IdMap.empty in try explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access with exn -> Format.printf "Found error at run %d:@." !num_runs; diff --git a/tests/test_simple.ml b/tests/test_simple.ml index 7689270..9b5dc4b 100644 --- a/tests/test_simple.ml +++ b/tests/test_simple.ml @@ -7,7 +7,8 @@ let test i = let x = Atomic.make i in let y = Atomic.make 0 in Atomic.spawn (fun () -> if Atomic.get x = 10 then Atomic.set y 2) ; - Atomic.spawn (fun () -> Atomic.set x 0 ; Atomic.set y 1) ; + Atomic.set x 0 ; + Atomic.set y 1 ; Atomic.final (fun () -> Atomic.check (fun () -> Atomic.get y <> 2)) let () = From 9d4fc109b10b3ab5141fcff4bbc001f4abde02ad Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 1 Oct 2022 21:14:33 +0200 Subject: [PATCH 12/18] fix: backtracking nested spawns --- src/tracedAtomic.ml | 47 +++++++++++++++++++++++++++++++------------- tests/test_simple.ml | 3 ++- 2 files changed, 35 insertions(+), 15 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 5d74ef0..097d5f9 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -234,6 +234,13 @@ let categorize = function | Set | Exchange -> Write | CompareAndSwap | FetchAndAdd -> Read_write +let rec list_findi predicate lst i = match lst with + | [] -> None + | x::_ when predicate i x -> Some (i, x) + | _::xs -> list_findi predicate xs (i + 1) + +let list_findi predicate lst = list_findi predicate lst 0 + let mark_backtrack ~is_last proc time state (last_read, last_write) = let j = proc.proc_id in let find ptr map = match IdMap.find_opt ptr map with @@ -249,27 +256,39 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = | (Write | Read_write), Some ptr -> max (find ptr last_read) (find ptr last_write) | _ -> assert false in + let rec find_replay_trace ~lower ~upper proc_id = + let pre_s = List.nth state (time - upper + 1) in + let replay_steps = List.filteri (fun k s -> k >= lower && k <= time - upper && s.run.proc_id = proc_id) state in + let replay_steps = List.rev_map (fun s -> s.run) replay_steps in + let causal p = match find_loc ~is_last:false p with + | None -> true + | Some (k, _) -> k <= upper in + if List.for_all causal replay_steps + then if IdSet.mem proc_id pre_s.enabled + then Some replay_steps + else let is_parent k s = k > lower && k < time - upper && s.run.op = Spawn && s.run.obj_ptr = Some proc_id in + match list_findi is_parent state with + | None -> None + | Some (parent_i, spawn) -> + assert (parent_i > lower) ; + begin match find_replay_trace ~lower:parent_i ~upper spawn.run.proc_id with + | None -> None + | Some spawn_steps -> Some (spawn_steps @ replay_steps) + end + else None + in match find_loc ~is_last proc with | None -> () | Some (i, _) -> assert (List.length state = time) ; let pre_s = List.nth state (time - i + 1) in - if IdSet.mem j pre_s.enabled then begin - let replay_steps = List.filteri (fun k s -> k <= time - i && s.run.proc_id = j) state in - let replay_steps = List.map (fun s -> s.run) replay_steps in - let todo = - match IdMap.find_opt j pre_s.backtrack with + match find_replay_trace ~lower:0 ~upper:i proc.proc_id with + | None -> () + | Some replay_steps -> + if match IdMap.find_opt j pre_s.backtrack with | None -> true | Some lst -> List.length lst > List.length replay_steps - in - let causal p = match find_loc ~is_last:false p with - | None -> true - | Some (k, _) -> k <= i in - if todo && List.for_all causal replay_steps - then pre_s.backtrack <- IdMap.add j (List.rev replay_steps) pre_s.backtrack - end - else - () (* failwith "TODO: currently untested" *) + then pre_s.backtrack <- IdMap.add j replay_steps pre_s.backtrack let map_diff_set map set = IdMap.filter (fun key _ -> not (IdSet.mem key set)) map diff --git a/tests/test_simple.ml b/tests/test_simple.ml index 9b5dc4b..c2179aa 100644 --- a/tests/test_simple.ml +++ b/tests/test_simple.ml @@ -6,7 +6,8 @@ module Atomic = Dscheck.TracedAtomic let test i = let x = Atomic.make i in let y = Atomic.make 0 in - Atomic.spawn (fun () -> if Atomic.get x = 10 then Atomic.set y 2) ; + Atomic.spawn (fun () -> + Atomic.spawn (fun () -> if Atomic.get x = 10 then Atomic.set y 2)) ; Atomic.set x 0 ; Atomic.set y 1 ; Atomic.final (fun () -> Atomic.check (fun () -> Atomic.get y <> 2)) From 5bdc331363cbb0ebb7af23c1ebe0c7c6a2738361 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sun, 2 Oct 2022 12:57:01 +0200 Subject: [PATCH 13/18] fix: atomic ops categorization --- src/tracedAtomic.ml | 45 +++++++++++++++++++++++++++++++++------------ 1 file changed, 33 insertions(+), 12 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 097d5f9..639e32c 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -21,7 +21,15 @@ type _ Effect.t += | FetchAndAdd : (int t * int) -> int Effect.t | Spawn : (unit -> unit) -> unit Effect.t -type atomic_op = Start | Make | Get | Set | Exchange | CompareAndSwap | FetchAndAdd | Spawn +type cas_result = Unknown | Success | Failed + +type atomic_op = + | Start | Make | Get | Set | Exchange | FetchAndAdd | Spawn + | CompareAndSwap of cas_result ref + +let atomic_op_equal a b = match a, b with + | CompareAndSwap _, CompareAndSwap _ -> true + | _ -> a = b let atomic_op_str x = match x with @@ -30,9 +38,14 @@ let atomic_op_str x = | Get -> "get" | Set -> "set" | Exchange -> "exchange" - | CompareAndSwap -> "compare_and_swap" | FetchAndAdd -> "fetch_and_add" | Spawn -> "spawn" + | CompareAndSwap cas -> + begin match !cas with + | Unknown -> "compare_and_swap?" + | Success -> "compare_and_swap" + | Failed -> "compare_and_no_swap" + end let tracing = ref false @@ -135,8 +148,11 @@ let handler current_process runner = | CompareAndSwap ((x,i), s, v) -> Some (fun (k : (a, _) continuation) -> + let res = ref Unknown in update_process_data current_process.uid (fun h -> - continue_with k (Atomic.compare_and_set x s v) h) CompareAndSwap (Some i); + let ok = Atomic.compare_and_set x s v in + res := if ok then Success else Failed ; + continue_with k ok h) (CompareAndSwap res) (Some i); runner ()) | FetchAndAdd ((v,i), x) -> Some @@ -203,7 +219,7 @@ let do_run init_schedule = | { proc_id = process_id_to_run ; op = next_op ; obj_ptr = next_ptr } :: schedule -> let process_to_run = get_process process_id_to_run in assert(not process_to_run.finished); - assert(process_to_run.next_op = next_op); + assert(atomic_op_equal process_to_run.next_op next_op); assert(process_to_run.next_repr = next_ptr); process_to_run.resume_func (handler process_to_run (run_trace schedule)) in @@ -231,8 +247,14 @@ type category = let categorize = function | Spawn | Start | Make -> Ignore | Get -> Read - | Set | Exchange -> Write - | CompareAndSwap | FetchAndAdd -> Read_write + | Set -> Write + | Exchange | FetchAndAdd -> Read_write + | CompareAndSwap res -> + begin match !res with + | Unknown -> failwith "CAS unknown outcome" (* should not happen *) + | Success -> Read_write + | Failed -> Read_write + end let rec list_findi predicate lst i = match lst with | [] -> None @@ -241,18 +263,17 @@ let rec list_findi predicate lst i = match lst with let list_findi predicate lst = list_findi predicate lst 0 -let mark_backtrack ~is_last proc time state (last_read, last_write) = +let mark_backtrack proc time state (last_read, last_write) = let j = proc.proc_id in let find ptr map = match IdMap.find_opt ptr map with | None -> None | Some lst -> List.find_opt (fun (_, proc_id) -> proc_id <> j) lst in - let find_loc ~is_last proc = + let find_loc proc = match categorize proc.op, proc.obj_ptr with | Ignore, _ -> None | Read, Some ptr -> find ptr last_write - | Write, Some ptr when not is_last -> find ptr last_read | (Write | Read_write), Some ptr -> max (find ptr last_read) (find ptr last_write) | _ -> assert false in @@ -260,7 +281,7 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = let pre_s = List.nth state (time - upper + 1) in let replay_steps = List.filteri (fun k s -> k >= lower && k <= time - upper && s.run.proc_id = proc_id) state in let replay_steps = List.rev_map (fun s -> s.run) replay_steps in - let causal p = match find_loc ~is_last:false p with + let causal p = match find_loc p with | None -> true | Some (k, _) -> k <= upper in if List.for_all causal replay_steps @@ -277,7 +298,7 @@ let mark_backtrack ~is_last proc time state (last_read, last_write) = end else None in - match find_loc ~is_last proc with + match find_loc proc with | None -> () | Some (i, _) -> assert (List.length state = time) ; @@ -338,7 +359,7 @@ let rec explore func time state (explored, state_planned) current_schedule clock :: state in let new_time = time + 1 in - mark_backtrack ~is_last:(IdSet.is_empty step.enabled) step.run new_time new_state (last_read, last_write); + mark_backtrack step.run new_time new_state (last_read, last_write); let add ptr map = IdMap.update ptr From c2e08baa6d0aecab63bb6ae7fa6ee557177d826f Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 19 Nov 2022 08:16:16 +0100 Subject: [PATCH 14/18] fix: atomic uid generation --- src/tracedAtomic.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 639e32c..423befc 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -65,12 +65,11 @@ let every_func = ref (fun () -> ()) let final_func = ref (fun () -> ()) (* Atomics implementation *) -let atomics_counter = ref (-1) +let atomics_counter = Atomic.make (-1) let make v = if !tracing then perform (Make v) else begin - let i = !atomics_counter in - atomics_counter := !atomics_counter - 1; + let i = Atomic.fetch_and_add atomics_counter (- 1) in (Atomic.make v, [i]) end @@ -402,7 +401,7 @@ let check f = let reset_state () = finished_processes := 0; - atomics_counter := 1; + Atomic.set atomics_counter 1; num_runs := 0; schedule_for_checks := []; processes := IdMap.empty From 26d1e7c5cc20dbd7a526d8c5a4b37b4ab5ae16ce Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 19 Nov 2022 08:44:59 +0100 Subject: [PATCH 15/18] simplify dead code --- src/tracedAtomic.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 423befc..48088b5 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -310,10 +310,10 @@ let mark_backtrack proc time state (last_read, last_write) = | Some lst -> List.length lst > List.length replay_steps then pre_s.backtrack <- IdMap.add j replay_steps pre_s.backtrack -let map_diff_set map set = +let map_subtract_set map set = IdMap.filter (fun key _ -> not (IdSet.mem key set)) map -let rec explore func time state (explored, state_planned) current_schedule clock (last_read, last_write) = +let rec explore func time state (explored, state_planned) current_schedule (last_read, last_write) = let s = List.hd state in assert (IdMap.is_empty s.backtrack) ; let dones = ref IdSet.empty in @@ -329,11 +329,10 @@ let rec explore func time state (explored, state_planned) current_schedule clock s.backtrack <- IdMap.singleton proc_id state_planned end ; let is_backtracking = ref false in - while IdMap.(cardinal (map_diff_set s.backtrack !dones)) > 0 do - let j, new_steps = IdMap.min_binding (map_diff_set s.backtrack !dones) in - let new_explored = - if !is_backtracking || state_planned <> [] then !dones else IdSet.empty in - dones := IdSet.add j !dones; + while IdMap.(cardinal (map_subtract_set s.backtrack !dones)) > 0 do + let j, new_steps = IdMap.min_binding (map_subtract_set s.backtrack !dones) in + let new_explored = !dones in + dones := IdSet.add j new_explored; let new_step, new_state_planned = match new_steps with | [] -> assert false @@ -374,8 +373,7 @@ let rec explore func time state (explored, state_planned) current_schedule clock | Read_write, Some ptr -> add ptr last_read, add ptr last_write | _ -> assert false in - let new_clock = IdMap.add j new_time clock in - explore func new_time new_state (new_explored, new_state_planned) new_schedule new_clock new_last_access + explore func new_time new_state (new_explored, new_state_planned) new_schedule new_last_access done let every f = @@ -412,9 +410,8 @@ let trace func = setup_run func empty_schedule ; let empty_state = do_run empty_schedule :: [] in let empty_state_planned = (IdSet.empty, []) in - let empty_clock = IdMap.empty in let empty_last_access = IdMap.empty, IdMap.empty in - try explore func 1 empty_state empty_state_planned empty_schedule empty_clock empty_last_access + try explore func 1 empty_state empty_state_planned empty_schedule empty_last_access with exn -> Format.printf "Found error at run %d:@." !num_runs; print_trace () ; From 7fa6a5463b332ae962b5332e2678c1721d0b5343 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sun, 29 Jan 2023 16:34:14 +0100 Subject: [PATCH 16/18] fix: backtracking dependencies and process spawn/start --- src/tracedAtomic.ml | 173 ++++++++++++++++++++------------------------ tests/dune | 5 ++ tests/test_bug.ml | 17 +++++ tests/test_list.ml | 2 +- 4 files changed, 102 insertions(+), 95 deletions(-) create mode 100644 tests/test_bug.ml diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 48088b5..6a4b97d 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -53,8 +53,7 @@ let finished_processes = ref 0 type process_data = { uid : Uid.t; - mutable domain_generator : int; - mutable atomic_generator : int; + mutable generator : int; mutable next_op: atomic_op; mutable next_repr: Uid.t option; mutable resume_func : (unit, unit) handler -> unit; @@ -124,8 +123,8 @@ let handler current_process runner = | Make v -> Some (fun (k : (a, _) continuation) -> - let i = current_process.atomic_generator :: current_process.uid in - current_process.atomic_generator <- current_process.atomic_generator + 1 ; + let i = current_process.generator :: current_process.uid in + current_process.generator <- current_process.generator + 1 ; let m = (Atomic.make v, i) in update_process_data current_process.uid (fun h -> continue_with k m h) Make (Some i); runner ()) @@ -163,12 +162,18 @@ let handler current_process runner = Some (fun (k : (a, _) continuation) -> let fiber_f h = continue_with (fiber f) () h in - let uid = current_process.domain_generator :: current_process.uid in - current_process.domain_generator <- current_process.domain_generator + 1 ; - push_process - { uid; domain_generator = 0; atomic_generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } ; - update_process_data current_process.uid (fun h -> - continue_with k () h) Spawn (Some uid); + let uid = current_process.generator :: current_process.uid in + current_process.generator <- current_process.generator + 1 ; + let new_process = + { uid; generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } + in + update_process_data + current_process.uid + (fun h -> + push_process new_process ; + continue_with k () h) + Spawn + (Some uid); runner ()) | _ -> None); @@ -198,13 +203,14 @@ let setup_run func init_schedule = let uid = [] in let fiber_f h = continue_with (fiber func) () h in push_process - { uid; domain_generator = 0; atomic_generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } ; + { uid; generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } ; tracing := false; num_runs := !num_runs + 1; if !num_runs mod 1000 == 0 then Format.printf "run: %d@." !num_runs let do_run init_schedule = + let trace = ref [] in let rec run_trace s () = tracing := false; !every_func (); @@ -213,17 +219,19 @@ let do_run init_schedule = | [] -> if !finished_processes == IdMap.cardinal !processes then begin tracing := false; !final_func (); - tracing := true + tracing := true; end | { proc_id = process_id_to_run ; op = next_op ; obj_ptr = next_ptr } :: schedule -> let process_to_run = get_process process_id_to_run in assert(not process_to_run.finished); assert(atomic_op_equal process_to_run.next_op next_op); assert(process_to_run.next_repr = next_ptr); + let run = { proc_id = process_id_to_run ; op = process_to_run.next_op ; obj_ptr = process_to_run.next_repr } in + trace := run :: !trace ; process_to_run.resume_func (handler process_to_run (run_trace schedule)) in tracing := true; - run_trace (List.rev init_schedule) (); + run_trace (List.rev init_schedule) () ; tracing := false; let procs = IdMap.mapi (fun i p -> { proc_id = i; op = p.next_op; obj_ptr = p.next_repr }) !processes @@ -234,7 +242,7 @@ let do_run init_schedule = |> Seq.map (fun (id, _) -> id) |> IdSet.of_seq in - let last_run = List.hd init_schedule in + let last_run = List.hd !trace in { procs; enabled = current_enabled; run = last_run; backtrack = IdMap.empty } type category = @@ -252,68 +260,63 @@ let categorize = function begin match !res with | Unknown -> failwith "CAS unknown outcome" (* should not happen *) | Success -> Read_write - | Failed -> Read_write + | Failed -> Read end -let rec list_findi predicate lst i = match lst with - | [] -> None - | x::_ when predicate i x -> Some (i, x) - | _::xs -> list_findi predicate xs (i + 1) - -let list_findi predicate lst = list_findi predicate lst 0 - -let mark_backtrack proc time state (last_read, last_write) = - let j = proc.proc_id in - let find ptr map = match IdMap.find_opt ptr map with - | None -> None - | Some lst -> - List.find_opt (fun (_, proc_id) -> proc_id <> j) lst - in - let find_loc proc = - match categorize proc.op, proc.obj_ptr with - | Ignore, _ -> None - | Read, Some ptr -> find ptr last_write - | (Write | Read_write), Some ptr -> max (find ptr last_read) (find ptr last_write) - | _ -> assert false - in - let rec find_replay_trace ~lower ~upper proc_id = - let pre_s = List.nth state (time - upper + 1) in - let replay_steps = List.filteri (fun k s -> k >= lower && k <= time - upper && s.run.proc_id = proc_id) state in - let replay_steps = List.rev_map (fun s -> s.run) replay_steps in - let causal p = match find_loc p with - | None -> true - | Some (k, _) -> k <= upper in - if List.for_all causal replay_steps - then if IdSet.mem proc_id pre_s.enabled - then Some replay_steps - else let is_parent k s = k > lower && k < time - upper && s.run.op = Spawn && s.run.obj_ptr = Some proc_id in - match list_findi is_parent state with - | None -> None - | Some (parent_i, spawn) -> - assert (parent_i > lower) ; - begin match find_replay_trace ~lower:parent_i ~upper spawn.run.proc_id with - | None -> None - | Some spawn_steps -> Some (spawn_steps @ replay_steps) - end - else None - in - match find_loc proc with - | None -> () - | Some (i, _) -> - assert (List.length state = time) ; - let pre_s = List.nth state (time - i + 1) in - match find_replay_trace ~lower:0 ~upper:i proc.proc_id with - | None -> () - | Some replay_steps -> - if match IdMap.find_opt j pre_s.backtrack with - | None -> true - | Some lst -> List.length lst > List.length replay_steps - then pre_s.backtrack <- IdMap.add j replay_steps pre_s.backtrack +let mark_backtrack proc state = + match proc.op, proc.obj_ptr, state with + | (Spawn | Start | Make), _, _ + | _, None, _ + | _, _, [] -> () + | _, Some proc_ptr, _ :: state -> + let rec go active_uids timeline acc = + match timeline with + | [] -> () + | pre :: timeline -> + let is_required = IdSet.mem pre.run.proc_id active_uids in + begin match is_required, pre.run.obj_ptr with + | true, Some ptr when ptr = proc_ptr && categorize pre.run.op <> Read -> + () + | false, Some ptr when ptr = proc_ptr -> + begin match categorize proc.op, categorize pre.run.op with + | _, Ignore -> failwith "how?" + | Read, Read -> go active_uids timeline acc + | _ -> + begin match acc, timeline with + | [], _ | _, [] -> assert false + | last :: _, pre :: _ -> + let j = last.proc_id in + if match IdMap.find_opt j pre.backtrack with + | None -> true + | Some lst -> List.length lst > List.length acc + then ( + pre.backtrack <- IdMap.add j acc pre.backtrack ; + ) + end + end + | true, None -> + go active_uids timeline (pre.run :: acc) + | true, Some ptr -> + let active_uids = IdSet.add ptr active_uids in + go active_uids timeline (pre.run :: acc) + | false, Some ptr when IdSet.mem ptr active_uids -> + begin match categorize pre.run.op with + | Read -> go active_uids timeline acc + | _ -> + let active_uids = IdSet.add pre.run.proc_id active_uids in + go active_uids timeline (pre.run :: acc) + end + | false, _ -> + go active_uids timeline acc + end + in + let active_uids = IdSet.add proc_ptr (IdSet.singleton proc.proc_id) in + go active_uids state [proc] let map_subtract_set map set = IdMap.filter (fun key _ -> not (IdSet.mem key set)) map -let rec explore func time state (explored, state_planned) current_schedule (last_read, last_write) = +let rec explore func time state (explored, state_planned) current_schedule = let s = List.hd state in assert (IdMap.is_empty s.backtrack) ; let dones = ref IdSet.empty in @@ -352,28 +355,10 @@ let rec explore func time state (explored, state_planned) current_schedule (last end in let step = do_run schedule in - let new_state = - { step with run = new_step ; backtrack = IdMap.empty } - :: state - in + let new_state = { step with backtrack = IdMap.empty } :: state in let new_time = time + 1 in - mark_backtrack step.run new_time new_state (last_read, last_write); - let add ptr map = - IdMap.update - ptr - (function None -> Some [new_time, step.run.proc_id] - | Some steps -> Some ((new_time, step.run.proc_id) :: steps)) - map - in - let new_last_access = - match categorize step.run.op, step.run.obj_ptr with - | Ignore, _ -> last_read, last_write - | Read, Some ptr -> add ptr last_read, last_write - | Write, Some ptr -> last_read, add ptr last_write - | Read_write, Some ptr -> add ptr last_read, add ptr last_write - | _ -> assert false - in - explore func new_time new_state (new_explored, new_state_planned) new_schedule new_last_access + mark_backtrack step.run new_state; + explore func new_time new_state (new_explored, new_state_planned) new_schedule done let every f = @@ -410,13 +395,13 @@ let trace func = setup_run func empty_schedule ; let empty_state = do_run empty_schedule :: [] in let empty_state_planned = (IdSet.empty, []) in - let empty_last_access = IdMap.empty, IdMap.empty in - try explore func 1 empty_state empty_state_planned empty_schedule empty_last_access + try explore func 1 empty_state empty_state_planned empty_schedule with exn -> Format.printf "Found error at run %d:@." !num_runs; print_trace () ; Format.printf "Unhandled exception: %s@." (Printexc.to_string exn) ; - Printexc.print_backtrace stdout + Printexc.print_backtrace stdout ; + raise exn let trace func = Fun.protect diff --git a/tests/dune b/tests/dune index 5edece8..a17ec4d 100644 --- a/tests/dune +++ b/tests/dune @@ -12,3 +12,8 @@ (name test_simple) (libraries dscheck) (modules test_simple)) + +(test + (name test_bug) + (libraries dscheck) + (modules test_bug)) diff --git a/tests/test_bug.ml b/tests/test_bug.ml new file mode 100644 index 0000000..d718308 --- /dev/null +++ b/tests/test_bug.ml @@ -0,0 +1,17 @@ +(** https://github.com/ocaml-multicore/dscheck/pull/3#issuecomment-1366878914 *) + +module Atomic = Dscheck.TracedAtomic + +let test () = + let cancelled = Atomic.make false in + let max_requests = Atomic.make 0 in + Atomic.spawn (fun () -> + Atomic.set cancelled true; + Atomic.decr max_requests; + ); + Atomic.spawn (fun () -> + ignore (Atomic.get max_requests); + assert (Atomic.get cancelled) (* This bug should be detected *) + ) + +let () = Atomic.trace test diff --git a/tests/test_list.ml b/tests/test_list.ml index dcdc556..b1f60af 100644 --- a/tests/test_list.ml +++ b/tests/test_list.ml @@ -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; ] ); From d0c08034a51ca9f4b9003e83614c4d613b203774 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Sat, 4 Feb 2023 22:37:01 +0100 Subject: [PATCH 17/18] use alcotest --- tests/dune | 4 ++-- tests/test_bug.ml | 15 ++++++++++++++- tests/test_simple.ml | 19 ++++++++++++++++--- 3 files changed, 32 insertions(+), 6 deletions(-) diff --git a/tests/dune b/tests/dune index a17ec4d..8f8734a 100644 --- a/tests/dune +++ b/tests/dune @@ -10,10 +10,10 @@ (test (name test_simple) - (libraries dscheck) + (libraries dscheck alcotest) (modules test_simple)) (test (name test_bug) - (libraries dscheck) + (libraries dscheck alcotest) (modules test_bug)) diff --git a/tests/test_bug.ml b/tests/test_bug.ml index d718308..7bd1620 100644 --- a/tests/test_bug.ml +++ b/tests/test_bug.ml @@ -14,4 +14,17 @@ let test () = assert (Atomic.get cancelled) (* This bug should be detected *) ) -let () = Atomic.trace test +let test () = + match Atomic.trace test with + | exception _ -> () + | _ -> failwith "expected failure" + +let () = + let open Alcotest in + run "dscheck" + [ + ( "bug", + [ + test_case "test" `Quick test; + ] ); + ] diff --git a/tests/test_simple.ml b/tests/test_simple.ml index c2179aa..2c158b7 100644 --- a/tests/test_simple.ml +++ b/tests/test_simple.ml @@ -12,7 +12,20 @@ let test i = Atomic.set y 1 ; Atomic.final (fun () -> Atomic.check (fun () -> Atomic.get y <> 2)) +let test_0 () = Atomic.trace (fun () -> test 0) + +let test_10 () = + match Atomic.trace (fun () -> test 10) with + | exception _ -> () + | _ -> failwith "expected failure" + let () = - Atomic.trace (fun () -> test 0) ; - Printf.printf "\n-----------------------------\n\n%!" ; - Atomic.trace (fun () -> test 10) + let open Alcotest in + run "dscheck" + [ + ( "simple", + [ + test_case "test-0" `Quick test_0; + test_case "test-10" `Quick test_10; + ] ); + ] From 9d7192d97ba890c46a8bba6d6cf1d06f79d50f97 Mon Sep 17 00:00:00 2001 From: ArthurW Date: Thu, 23 Feb 2023 00:31:18 +0100 Subject: [PATCH 18/18] prettier output --- src/tracedAtomic.ml | 54 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 49 insertions(+), 5 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index 6a4b97d..05e33de 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -10,6 +10,28 @@ end module IdSet = Set.Make (Uid) module IdMap = Map.Make (Uid) +module Uid_pretty = struct + let gen = ref 0 + let cache = ref IdMap.empty + + let find t = + match IdMap.find t !cache with + | i -> i + | exception Not_found -> + let i = !gen in + incr gen ; + cache := IdMap.add t i !cache ; + i + + let to_string = function + | [] -> "_" + | t -> + let i = find t in + if i >= 0 && i < 26 + then String.make 1 (Char.chr (Char.code 'A' + i)) + else string_of_int i +end + type 'a t = 'a Atomic.t * Uid.t type _ Effect.t += @@ -190,12 +212,37 @@ type state_cell = { mutable backtrack : proc_rec list IdMap.t; } +let group_by fn = function + | [] -> [] + | first :: rest -> + let rec go previous previouses = function + | [] -> [previous::previouses] + | x::xs when fn x previous -> go x (previous::previouses) xs + | x::xs -> (previous::previouses) :: go x [] xs + in + List.rev (go first [] rest) + +let pretty_print h lst = + List.iter + (function + | steps when List.compare_length_with steps 3 <= 0 -> + List.iter (fun step -> Format.fprintf h "%s" (Uid_pretty.to_string step.proc_id)) steps + | (step :: _) as steps -> + Format.fprintf h "(%s%i)" (Uid_pretty.to_string step.proc_id) (List.length steps) + | _ -> assert false) + (group_by (fun a b -> a.proc_id = b.proc_id) lst) + +let clear_line = "\027[2K\r" + let num_runs = ref 0 (* we stash the current state in case a check fails and we need to log it *) let schedule_for_checks = ref [] let setup_run func init_schedule = + num_runs := !num_runs + 1; + if !num_runs mod 1000 == 0 then + Format.printf "%srun: %#i %a %!" clear_line !num_runs pretty_print !schedule_for_checks; processes := IdMap.empty ; finished_processes := 0; schedule_for_checks := init_schedule; @@ -204,10 +251,7 @@ let setup_run func init_schedule = let fiber_f h = continue_with (fiber func) () h in push_process { uid; generator = 0; next_op = Start; next_repr = None; resume_func = fiber_f; finished = false } ; - tracing := false; - num_runs := !num_runs + 1; - if !num_runs mod 1000 == 0 then - Format.printf "run: %d@." !num_runs + tracing := false let do_run init_schedule = let trace = ref [] in @@ -406,4 +450,4 @@ let trace func = let trace func = Fun.protect (fun () -> trace func) - ~finally:(fun () -> Format.printf "@.Finished after %i runs.@." !num_runs) + ~finally:(fun () -> Format.printf "@.Finished after %#i runs.@." !num_runs)