From 858271fa91d4cee407408a15d584c0629cdc0740 Mon Sep 17 00:00:00 2001 From: Bartosz Modelski Date: Wed, 5 Apr 2023 16:05:43 +0100 Subject: [PATCH] possible fix . --- src/tracedAtomic.ml | 140 +++++++++++++++++++++++++----------------- tests/test_simple2.ml | 1 + 2 files changed, 85 insertions(+), 56 deletions(-) diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index f4ffa50..b75f749 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -198,26 +198,26 @@ let num_traces = ref 0 (* we stash the current state in case a check fails and we need to log it *) let schedule_for_checks = ref [] +let var_name i = + match i with + | None -> "" + | Some i -> + let c = Char.chr (i + 97) in + let seq = Seq.cons c Seq.empty in + String.of_seq seq + let print_trace () = Printf.printf "-----------------------\n"; - List.iter - (fun s -> + List.iteri + (fun i s -> match s with | last_run_proc, last_run_op, last_run_ptr -> - let var_name i = - let c = Char.chr (i + 97) in - let seq = Seq.cons c Seq.empty in - String.of_seq seq - in + let last_run_ptr = var_name last_run_ptr in - let last_run_ptr = - Option.map (* string_of_int *) var_name last_run_ptr - |> Option.value ~default:"" - in let tabs = List.init last_run_proc (fun _ -> "\t\t") |> String.concat "" in - Printf.printf "%sP%d: %s %s\n" tabs last_run_proc + Printf.printf "[depth=%d] %sP%d: %s %s\n" i tabs last_run_proc (atomic_op_str last_run_op) last_run_ptr) !schedule_for_checks; @@ -239,7 +239,7 @@ let do_run init_func init_schedule = | [] -> if !finished_processes == num_processes then ( tracing := false; - print_trace (); + (* print_trace (); *) num_traces := !num_traces + 1; !final_func (); tracing := true) @@ -289,24 +289,26 @@ let do_run init_func init_schedule = let _set_to_str s = IntSet.to_seq s |> List.of_seq |> List.map Int.to_string |> String.concat ", " -let rec explore_source depth func state sleep = - (* sleep := IntSet.empty; *) +let rec explore_source depth func state sleep_sets = + let sleep = last_element sleep_sets in let s = last_element state in (* Printf.printf "[depth=%d] explore (backtrack=[%s], sleep=[%s], enabled=[%s])\n%!" depth (set_to_str s.backtrack) (set_to_str !sleep) (set_to_str s.enabled); *) let p_maybe = IntSet.min_elt_opt (IntSet.diff s.enabled !sleep) in match p_maybe with - | None -> () (* Printf.printf "[depth=%d] rtn\n%!" depth *) + | None -> () + (* Printf.printf "[depth=%d] rtn\n%!" depth *) | Some p -> s.backtrack <- IntSet.singleton p; while IntSet.(cardinal (diff s.backtrack !sleep)) > 0 do (* Printf.printf "[depth=%d] loop (backtrack=[%s], sleep=[%s])\n%!" depth - (set_to_str s.backtrack) (set_to_str !sleep); *) + (_set_to_str s.backtrack) (_set_to_str !sleep); *) let p = IntSet.min_elt (IntSet.diff s.backtrack !sleep) in let proc = List.nth s.procs p in - (* Printf.printf "[depth=%d] p=%d, %s\n%!" depth p (atomic_op_str proc.op); *) + (* Printf.printf "[depth=%d] p=%d, %s, %s\n%!" depth p + (atomic_op_str proc.op) (var_name proc.obj_ptr); *) (* run *) let state_top = let schedule = @@ -323,10 +325,12 @@ let rec explore_source depth func state sleep = let reversible_races = List.filter (fun proc' -> - let run_ptr = Option.value proc'.run_ptr ~default:(-2) in - obj_ptr = run_ptr && proc'.run_proc <> p) + match proc'.run_ptr with + | None -> false + | Some run_ptr -> obj_ptr = run_ptr && proc'.run_proc <> p) new_state in + let reversible_races = match reversible_races with | [] -> [] @@ -337,8 +341,9 @@ let rec explore_source depth func state sleep = (List.length reversible_races); *) for i = 0 to List.length reversible_races - 1 do let e = List.nth reversible_races i in - (* Printf.printf "[depth=%d] inner loop, racing op: e=(q=%d, %s)\n%!" - depth e.run_proc (atomic_op_str e.run_op); *) + (* Printf.printf + "[depth=%d] inner loop, racing op: e=(p'=%d, %s, %s)\n%!" depth + e.run_proc (atomic_op_str e.run_op) (var_name e.run_ptr); *) let found_e, prefix_rev, suffix_rev = List.fold_left (fun (seen_e, prefix, suffix) proc' -> @@ -351,29 +356,31 @@ let rec explore_source depth func state sleep = List.length prefix_rev + List.length suffix_rev = List.length state - 1); assert found_e; - let prefix (* E' *) = List.rev prefix_rev in - if List.length prefix > 0 then + if List.length prefix_rev > 0 then ( + let prefix (* E' *) = List.rev prefix_rev in (* List.iter - (fun proc -> - Printf.printf "[depth=%d] ::prefix:: (p=%d, %s)\n%!" depth - proc.run_proc - (atomic_op_str proc.run_op)) - prefix; *) + (fun proc -> + Printf.printf "[depth=%d] ::prefix:: (p=%d, %s, %s)\n%!" + depth proc.run_proc + (atomic_op_str proc.run_op) + (var_name proc.run_ptr)) + prefix; *) let suffix = List.rev suffix_rev in (* List.iter - (fun proc -> - Printf.printf "[depth=%d] ::suffix:: (p=%d, %s)\n%!" depth - proc.run_proc - (atomic_op_str proc.run_op)) - suffix; *) + (fun proc -> + Printf.printf "[depth=%d] ::suffix:: (p=%d, %s, %s)\n%!" + depth proc.run_proc + (atomic_op_str proc.run_op) + (var_name proc.run_ptr)) + suffix; *) let prefix_top = last_element prefix in (* Printf.printf - "[depth=%d] nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth - prefix_top.run_proc - (atomic_op_str prefix_top.run_op); *) + "[depth=%d] nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth + prefix_top.run_proc + (atomic_op_str prefix_top.run_op); *) let v_E (* occurs after e but independent of e *) = List.filter (fun proc' -> @@ -393,11 +400,11 @@ let rec explore_source depth func state sleep = let v = v_E @ [ state_top ] in (* List.iter - (fun proc -> - Printf.printf "[depth=%d] ::v:: (p=%d, %s)\n%!" depth - proc.run_proc - (atomic_op_str proc.run_op)) - v; *) + (fun proc -> + Printf.printf "[depth=%d] ::v:: (p=%d, %s)\n%!" depth + proc.run_proc + (atomic_op_str proc.run_op)) + v; *) let initials = let initials_map, initials_spawns = List.fold_left @@ -413,7 +420,7 @@ let rec explore_source depth func state sleep = IntMap.update obj_ptr (function | Some v -> Some v - | None -> Some state_cell.run_proc) + | None -> Some (`Run_proc state_cell.run_proc)) first_accesses in (new_first_accesses, spawns)) @@ -421,19 +428,38 @@ let rec explore_source depth func state sleep = v in IntMap.fold - (fun _ run_proc initials_set -> + (fun _obj_ptr (`Run_proc run_proc) initials_set -> IntSet.add run_proc initials_set) initials_map initials_spawns in - - (* Printf.printf "[depth=%d] initials=[%s], backtrack=[%s]\n%!" - depth (set_to_str initials) - (set_to_str prefix_top.backtrack); *) - if IntSet.(cardinal (inter prefix_top.backtrack initials)) = 0 then - let _initial = IntSet.min_elt initials in - (* Printf.printf "[depth=%d] adding initial to backtrack\n%!" - depth; *) - prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack +(* + Printf.printf + "[depth=%d] initials=[%s], backtrack=[%s] at depth=%d, p=%d, \ + op=%s \n\ + %!" + depth (_set_to_str initials) + (_set_to_str prefix_top.backtrack) + (List.length prefix - 1) + prefix_top.run_proc + (atomic_op_str prefix_top.run_op); *) + let prefix_top_sleep = + !(List.nth sleep_sets (List.length prefix - 1)) + in + if + IntSet.( + cardinal + (inter prefix_top.backtrack (diff initials prefix_top_sleep))) + = 0 + then ( + let _initial = + match IntSet.(min_elt_opt (diff initials prefix_top_sleep)) with + | Some initial -> initial + | None -> IntSet.min_elt initials + in +(* + Printf.printf "[depth=%d] adding initial to backtrack\n%!" + depth; *) + prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack)) done; let sleep' = @@ -448,9 +474,11 @@ let rec explore_source depth func state sleep = | Some obj_ptr' -> obj_ptr' <> obj_ptr) !sleep in - explore_source (depth + 1) func new_state (ref sleep'); + explore_source (depth + 1) func new_state (sleep_sets @ [ ref sleep' ]); sleep := IntSet.add p !sleep - done + done;; + (* Printf.printf "[depth=%d] exit (backtrack=[%s], sleep=[%s])\n%!" depth + (_set_to_str s.backtrack) (_set_to_str !sleep) *) let rec explore func state clock last_access = let s = last_element state in @@ -519,7 +547,7 @@ let _trace func = let _trace_source func = reset_state (); let empty_state = do_run func [ (0, Start, None) ] in - explore_source 0 func [ empty_state ] (ref IntSet.empty) + explore_source 1 func [ empty_state ] [ ref IntSet.empty ] let trace func = _trace_source func; diff --git a/tests/test_simple2.ml b/tests/test_simple2.ml index 7d2a5ed..1a8e98e 100644 --- a/tests/test_simple2.ml +++ b/tests/test_simple2.ml @@ -16,4 +16,5 @@ let test () = Format.printf "b=%i c=%i ok=%b@." (Atomic.get b) (Atomic.get c) (Atomic.get ok)) + let () = Atomic.trace test