diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index b75f749..b8d0712 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -290,7 +290,8 @@ 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_sets = - let sleep = last_element sleep_sets in + let _sleep = last_element sleep_sets in + let sleep = ref IntSet.empty 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); *) @@ -442,17 +443,17 @@ let rec explore_source depth func state sleep_sets = (List.length prefix - 1) prefix_top.run_proc (atomic_op_str prefix_top.run_op); *) - let prefix_top_sleep = + 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))) + (inter prefix_top.backtrack ( initials ))) = 0 then ( let _initial = - match IntSet.(min_elt_opt (diff initials prefix_top_sleep)) with + match IntSet.(min_elt_opt ( initials )) with | Some initial -> initial | None -> IntSet.min_elt initials in diff --git a/tests/test_conditional1.ml b/tests/test_conditional1.ml new file mode 100644 index 0000000..1a8e98e --- /dev/null +++ b/tests/test_conditional1.ml @@ -0,0 +1,20 @@ +module Atomic = Dscheck.TracedAtomic + +let test () = + let c = Atomic.make 0 in + let b = Atomic.make 0 in + let ok = Atomic.make false in + + Atomic.spawn (fun () -> Atomic.set b 1); + Atomic.spawn (fun () -> + Atomic.set c 1; + Atomic.set b 2); + Atomic.spawn (fun () -> + if Atomic.get c = 0 then if Atomic.get b = 0 then Atomic.set ok true); + + Atomic.final (fun () -> + Format.printf "b=%i c=%i ok=%b@." (Atomic.get b) (Atomic.get c) + (Atomic.get ok)) + + +let () = Atomic.trace test diff --git a/tests/test_conditional2.ml b/tests/test_conditional2.ml new file mode 100644 index 0000000..a69a1b0 --- /dev/null +++ b/tests/test_conditional2.ml @@ -0,0 +1,25 @@ +module Atomic = Dscheck.TracedAtomic + +let test () = + let x = Atomic.make 0 in + let y = Atomic.make 0 in + let z = Atomic.make 0 in + + let tmp = ref (-1) in + Atomic.spawn (fun () -> tmp := Atomic.get x); + Atomic.spawn (fun () -> Atomic.set y 1); + + Atomic.spawn (fun () -> + let m = Atomic.get y in + if m = 0 then Atomic.set z 1); + + Atomic.spawn (fun () -> + let n = Atomic.get z in + let l = Atomic.get y in + if n = 1 then if l = 0 then Atomic.set x 1); + + Atomic.final (fun () -> + Format.printf "tmp=%d x=%d y=%d z=%d\n%!" !tmp (Atomic.get x) + (Atomic.get y) (Atomic.get z)) + +let () = Atomic.trace test