Test Rwlock

picos_meta.opam

@@ -55,3 +55,7 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/ocaml-multicore/picos.git"
+pin-depends: [
+  [ "qcheck-stm.dev" "git+https://github.com/ocaml-multicore/multicoretests#19a43c238fee7fd56fac32519a53240b52a00303" ]
+  [ "qcheck-multicoretests-util.dev" "git+https://github.com/ocaml-multicore/multicoretests#19a43c238fee7fd56fac32519a53240b52a00303" ]
+]

picos_meta.opam.template

@@ -0,0 +1,4 @@
+pin-depends: [
+  [ "qcheck-stm.dev" "git+https://github.com/ocaml-multicore/multicoretests#19a43c238fee7fd56fac32519a53240b52a00303" ]
+  [ "qcheck-multicoretests-util.dev" "git+https://github.com/ocaml-multicore/multicoretests#19a43c238fee7fd56fac32519a53240b52a00303" ]
+]

test/dune

@@ -66,6 +66,18 @@
    ;;
    )))
 
+(test
+ (package picos_meta)
+ (name test_rwlock)
+ (modules test_rwlock)
+ (libraries
+  picos
+  picos_std.sync
+  qcheck-core
+  qcheck-multicoretests-util
+  qcheck-stm.stm
+  stm_run))
+
 ;;
 
 (test

test/stm_run/stm_run.ocaml5.ml

@@ -2,14 +2,14 @@ include Intf
 
 let run (type cmd state sut) ?(verbose = true) ?(count = default_count)
     ?(budgetf = default_budgetf) ~name ?make_domain
-    (module Spec : STM.Spec
+    (module Spec : STM.SpecExt
       with type cmd = cmd
        and type state = state
        and type sut = sut) =
-  let module Seq = STM_sequential.Make (Spec) in
+  let module Seq = STM_sequential.MakeExt (Spec) in
   let module Dom = struct
     module Spec = Spec
-    include STM_domain.Make (Spec)
+    include STM_domain.MakeExt (Spec)
   end in
   Util.run_with_budget ~budgetf ~count @@ fun count ->
   [

test/test_htbl.ml

@@ -26,6 +26,8 @@ module Int = struct
 end
 
 module Spec = struct
+  include SpecDefaults
+
   type cmd =
     | Try_add of int
     | Mem of int
@@ -61,7 +63,6 @@ module Spec = struct
 
   let init_state = State.empty
   let init_sut () = Htbl.create ~hashed_type:(module Int) ()
-  let cleanup _ = ()
 
   let next_state c s =
     match c with
@@ -72,8 +73,6 @@ module Spec = struct
     | To_keys -> s
     | Remove_all -> State.empty
 
-  let precond _ _ = true
-
   let run c d =
     match c with
     | Try_add x -> Res (bool, Htbl.try_add d x x)

test/test_mpmcq.ml

@@ -13,6 +13,8 @@ let () =
   match Queue.pop_exn q with _ -> assert false | exception Queue.Empty -> ()
 
 module Spec = struct
+  include SpecDefaults
+
   type cmd = Push of int | Push_head of int | Pop_opt | Length
 
   let show_cmd = function
@@ -48,7 +50,6 @@ module Spec = struct
 
   let init_state = ([], [])
   let init_sut () = Queue.create ~padded:true ()
-  let cleanup _ = ()
 
   let next_state c s =
     match c with
@@ -57,8 +58,6 @@ module Spec = struct
     | Pop_opt -> State.drop s
     | Length -> s
 
-  let precond _ _ = true
-
   let run c d =
     match c with
     | Push x -> Res (unit, Queue.push d x)

test/test_mpscq.ml

@@ -1,6 +1,9 @@
+open STM
 module Queue = Picos_aux_mpscq
 
 module Spec = struct
+  include SpecDefaults
+
   type cmd = Push of int | Push_head of int | Pop | Pop_all
 
   let show_cmd c =
@@ -35,7 +38,6 @@ module Spec = struct
 
   let init_state = []
   let init_sut () = Queue.create ()
-  let cleanup _ = ()
 
   let next_state c s =
     match c with
@@ -44,10 +46,7 @@ module Spec = struct
     | Pop -> ( match s with _ :: s -> s | [] -> [])
     | Pop_all -> []
 
-  let precond _ _ = true
-
   let run c d =
-    let open STM in
     match c with
     | Push i -> Res (unit, Queue.push d i)
     | Push_head i -> Res (unit, Queue.push_head d i)
@@ -60,7 +59,6 @@ module Spec = struct
     | Pop_all -> Res (list int, Queue.pop_all d |> List.of_seq)
 
   let postcond c (s : state) res =
-    let open STM in
     match (c, res) with
     | Push _, Res ((Unit, _), ()) -> true
     | Push_head _, Res ((Unit, _), ()) -> true

test/test_rwlock.ml

@@ -0,0 +1,96 @@
+open QCheck
+open STM
+module Rwlock = Picos_std_sync.Rwlock
+
+module Spec = struct
+  include SpecDefaults
+
+  type cmd = Push of int | Pop_opt | Top_opt | Length
+
+  let show_cmd = function
+    | Push x -> "Push " ^ string_of_int x
+    | Pop_opt -> "Pop_opt"
+    | Top_opt -> "Top_opt"
+    | Length -> "Length"
+
+  module State = struct
+    type t = int list
+
+    let push x xs = x :: xs
+    let pop_opt = function _ :: xs -> xs | [] -> []
+    let top_opt = function x :: _ -> Some x | [] -> None
+    let length = List.length
+  end
+
+  type state = State.t
+  type sut = { stack : int Stack.t; rwlock : Rwlock.t }
+
+  let arb_cmd _s =
+    [
+      Gen.int_range 1 1000 |> Gen.map (fun x -> Push x);
+      Gen.return Pop_opt;
+      Gen.return Top_opt;
+      Gen.return Length;
+    ]
+    |> Gen.oneof |> make ~print:show_cmd
+
+  let init_state = []
+  let init_sut () = { stack = Stack.create (); rwlock = Rwlock.create () }
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Push x -> State.push x s
+    | Pop_opt -> State.pop_opt s
+    | Top_opt -> s
+    | Length -> s
+
+  let run c d =
+    match c with
+    | Push x ->
+        Rwlock.wrlock d.rwlock;
+        Stack.push x d.stack;
+        Rwlock.unlock d.rwlock;
+        Res (unit, ())
+    | Pop_opt ->
+        Rwlock.wrlock d.rwlock;
+        let result = Stack.pop_opt d.stack in
+        Rwlock.unlock d.rwlock;
+        Res (option int, result)
+    | Top_opt ->
+        Rwlock.rdlock d.rwlock;
+        let result = Stack.top_opt d.stack in
+        Rwlock.unlock d.rwlock;
+        Res (option int, result)
+    | Length ->
+        Rwlock.rdlock d.rwlock;
+        let result = Stack.length d.stack in
+        Rwlock.unlock d.rwlock;
+        Res (int, result)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Push _x, Res ((Unit, _), ()) -> true
+    | Pop_opt, Res ((Option Int, _), res) -> res = State.top_opt s
+    | Top_opt, Res ((Option Int, _), res) -> res = State.top_opt s
+    | Length, Res ((Int, _), res) -> res = State.length s
+    | _, _ -> false
+
+  let wrap th =
+    let open Picos in
+    let effc (type a) (e : a Effect.t) :
+        ((a, _) Effect.Deep.continuation -> _) option =
+      match e with
+      | Trigger.Await t ->
+          Some
+            (fun k ->
+              while not (Trigger.is_signaled t) do
+                Domain.cpu_relax ()
+              done;
+              Effect.Deep.continue k None)
+      | _ -> None
+    in
+    Effect.Deep.match_with th () { effc; exnc = raise; retc = Fun.id }
+end
+
+let () = Stm_run.run ~name:"Rwlock" (module Spec) |> exit