another conditional test

Author: bartoszmodelski

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

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

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