Omit buffer test

lib/STM.ml

@@ -219,23 +219,24 @@ struct
     make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
 
   (* Parallel agreement property based on [Domain] *)
-  let agree_prop_par =
-    (fun (seq_pref,cmds1,cmds2) ->
-      assume (cmds_ok Spec.init_state (seq_pref@cmds1));
-      assume (cmds_ok Spec.init_state (seq_pref@cmds2));
-      let sut = Spec.init_sut () in
-      let pref_obs = interp_sut_res sut seq_pref in
-      let wait = Atomic.make true in
-      let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; interp_sut_res sut cmds1) in
-      let dom2 = Domain.spawn (fun () -> Atomic.set wait false; interp_sut_res sut cmds2) in
-      let obs1 = Domain.join dom1 in
-      let obs2 = Domain.join dom2 in
-      let ()   = Spec.cleanup sut in
-      check_obs pref_obs obs1 obs2 Spec.init_state
+  let agree_prop_par (seq_pref,cmds1,cmds2) =
+    assume (cmds_ok Spec.init_state (seq_pref@cmds1));
+    assume (cmds_ok Spec.init_state (seq_pref@cmds2));
+    let sut = Spec.init_sut () in
+    let pref_obs = interp_sut_res sut seq_pref in
+    let wait = Atomic.make true in
+    let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in
+    let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in
+    let obs1 = Domain.join dom1 in
+    let obs2 = Domain.join dom2 in
+    let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
+    let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
+    let ()   = Spec.cleanup sut in
+    check_obs pref_obs obs1 obs2 Spec.init_state
       || Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
-              (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-              (pref_obs,obs1,obs2))
+           (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
+           (pref_obs,obs1,obs2)
 
   (* Parallel agreement test based on [Domain] and [repeat] *)
   let agree_test_par ~count ~name =

lib/lin.ml

@@ -121,22 +121,22 @@ module MakeDomThr(Spec : CmdSpec)
                  else (Spec.cleanup seq_sut'; false))
 
   (* Linearizability property based on [Domain] and an Atomic flag *)
-  let lin_prop_domain =
-    (fun (seq_pref,cmds1,cmds2) ->
-      let sut = Spec.init () in
-      let pref_obs = interp_plain sut seq_pref in
-      let wait = Atomic.make true in
-      let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; interp sut cmds1) in
-      let dom2 = Domain.spawn (fun () -> Atomic.set wait false; interp sut cmds2) in
-      let obs1 = Domain.join dom1 in
-      let obs2 = Domain.join dom2 in
-      let ()   = Spec.cleanup sut in
-      let seq_sut = Spec.init () in
-      check_seq_cons pref_obs obs1 obs2 seq_sut []
+  let lin_prop_domain (seq_pref,cmds1,cmds2) =
+    let sut = Spec.init () in
+    let pref_obs = interp sut seq_pref in
+    let wait = Atomic.make true in
+    let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp sut cmds1) with exn -> Error exn) in
+    let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in
+    let obs1 = Domain.join dom1 in
+    let obs2 = Domain.join dom2 in
+    let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
+    let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
+    let seq_sut = Spec.init () in
+    check_seq_cons pref_obs obs1 obs2 seq_sut []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
               (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-              (pref_obs,obs1,obs2))
+              (pref_obs,obs1,obs2)
 
   (* Linearizability property based on [Thread] *)
   let lin_prop_thread =

src/buffer/dune

@@ -11,12 +11,13 @@
  (libraries qcheck STM)
  (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
-(rule
- (alias runtest)
- (package multicoretests)
- (deps buffer_stm_test.exe)
- (action
-  (progn
-   (bash "(./buffer_stm_test.exe --no-colors --verbose || echo 'test run triggered an error') | tee stm-output.txt")
-   (run %{bin:check_error_count} "buffer/buffer_stm_test" 1 stm-output.txt))))
+; disable segfaulting buffer test for now
+; (rule
+;  (alias runtest)
+;  (package multicoretests)
+;  (deps buffer_stm_test.exe)
+;  (action
+;   (progn
+;    (bash "(./buffer_stm_test.exe --no-colors --verbose || echo 'test run triggered an error') | tee stm-output.txt")
+;    (run %{bin:check_error_count} "buffer/buffer_stm_test" 1 stm-output.txt))))
 

src/dune

@@ -6,7 +6,7 @@
        (alias neg_tests/default)
        ;; stdlib, in alphabetic order
        (alias atomic/default)
-       (alias buffer/default)
+       ;; (alias buffer/default)  -- disable buffer test causing segfault
        (alias domain/default)
        (alias hashtbl/default)
        (alias lazy/default)

src/lazy/lazy_lin_test.ml

@@ -1,4 +1,5 @@
 open QCheck
+open Lin
 
 (** parallel linearization tests of Lazy *)
 
@@ -44,19 +45,22 @@ struct
 
   let cleanup _ = ()
 
+  let equal_exn = (=)
   type res =
-    | RForce of int
-    | RForce_val of int
+    | RForce of (int,exn) result
+    | RForce_val of (int,exn) result
     | RIs_val of bool
-    | RMap of int
-    | RMap_val of int [@@deriving show { with_path = false }, eq]
+    | RMap of (int,exn) result
+    | RMap_val of (int,exn) result [@@deriving show { with_path = false }, eq]
 
   let run c l = match c with
-    | Force               -> RForce (Lazy.force l)
-    | Force_val           -> RForce_val (Lazy.force_val l)
+    | Force               -> RForce (Util.protect Lazy.force l)
+    | Force_val           -> RForce_val (Util.protect Lazy.force_val l)
     | Is_val              -> RIs_val (Lazy.is_val l)
-    | Map (Fun (_,f))     -> RMap (Lazy.force (Lazy.map f l)) (*we force the "new lazy"*)
-    | Map_val (Fun (_,f)) -> RMap_val (Lazy.force (Lazy.map_val f l)) (*we force the "new lazy"*)
+    | Map (Fun (_,f))     -> RMap (try Ok (Lazy.force (Lazy.map f l))
+                                   with exn -> Error exn) (*we force the "new lazy"*)
+    | Map_val (Fun (_,f)) -> RMap_val (try Ok (Lazy.force (Lazy.map_val f l))
+                                       with exn -> Error exn) (*we force the "new lazy"*)
 end