Skip to content

Commit

Permalink
possible fix
Browse files Browse the repository at this point in the history 
.
  • Loading branch information
@bartoszmodelski
bartoszmodelski committed Apr 5, 2023
1 parent 813a8cb commit 858271f
Show file tree
Hide file tree
Showing 2 changed files with 85 additions and 56 deletions.
140 changes: 84 additions & 56 deletions src/tracedAtomic.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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)
Expand Down Expand Up @@ -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 =
Expand All @@ -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
| [] -> []
Expand All @@ -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' ->
Expand All @@ -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' ->
Expand All @@ -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
Expand All @@ -413,27 +420,46 @@ 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))
(IntMap.empty, IntSet.empty)
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' =
Expand All @@ -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
Expand Down Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions tests/test_simple2.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 858271f

Please sign in to comment.