From ad7855f99a40ba7be953abc57d6e4b352a47b199 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Tue, 21 Jan 2025 12:12:48 +0000 Subject: [PATCH] Add `Rwlock` --- bench/bench_hashtbl.ml | 47 ++++++- bench/bench_lock_yield.ml | 20 ++- bench/bench_ref.ml | 34 ++++- lib/picos_std.sync/picos_std_sync.ml | 1 + lib/picos_std.sync/picos_std_sync.mli | 174 ++++++++++++++++++++++++- lib/picos_std.sync/rwlock.ml | 179 ++++++++++++++++++++++++++ test/dune | 13 ++ test/test_rwlock.ml | 80 ++++++++++++ test/test_sync.ml | 144 +++++++++++++++++++++ 9 files changed, 684 insertions(+), 8 deletions(-) create mode 100644 lib/picos_std.sync/rwlock.ml create mode 100644 test/test_rwlock.ml diff --git a/bench/bench_hashtbl.ml b/bench/bench_hashtbl.ml index 419d05c4..ce3be979 100644 --- a/bench/bench_hashtbl.ml +++ b/bench/bench_hashtbl.ml @@ -21,6 +21,7 @@ let run_one ~budgetf ~n_domains ?(n_ops = 100 * Util.iter_factor) let t = Hashtbl.create 1000 in let lock = Lock.create ~padded:true () in + let rwlock = Rwlock.create ~padded:true () in let sem = Sem.create ~padded:true 1 in let n_ops = (100 + percent_mem) * n_ops / 100 in @@ -41,6 +42,16 @@ let run_one ~budgetf ~n_domains ?(n_ops = 100 * Util.iter_factor) Hashtbl.replace t key value done end + | `Rwlock -> + Rwlock.holding rwlock @@ fun () -> + Hashtbl.clear t; + if prepopulate then begin + for _ = 1 to n_keys do + let value = Random.bits () in + let key = value mod n_keys in + Hashtbl.replace t key value + done + end | `Sem -> Sem.acquire sem; Hashtbl.clear t; @@ -87,6 +98,34 @@ let run_one ~budgetf ~n_domains ?(n_ops = 100 * Util.iter_factor) end in work () + | `Rwlock -> + let rec work () = + let n = Countdown.alloc n_ops_todo ~domain_index ~batch:1000 in + if n <> 0 then begin + for _ = 1 to n do + let value = Random.State.bits state in + let op = (value asr 20) mod 100 in + let key = value mod n_keys in + if op < percent_mem then begin + Rwlock.acquire_shared rwlock; + Hashtbl.find_opt t key |> ignore; + Rwlock.release_shared rwlock + end + else if op < limit_add then begin + Rwlock.acquire rwlock; + Hashtbl.replace t key value; + Rwlock.release rwlock + end + else begin + Rwlock.acquire rwlock; + Hashtbl.remove t key; + Rwlock.release rwlock + end + done; + work () + end + in + work () | `Sem -> let rec work () = let n = Countdown.alloc n_ops_todo ~domain_index ~batch:1000 in @@ -121,14 +160,18 @@ let run_one ~budgetf ~n_domains ?(n_ops = 100 * Util.iter_factor) Printf.sprintf "%d worker%s, %d%% reads with %s" n_domains (if n_domains = 1 then "" else "s") percent_mem - (match lock_type with `Lock -> "Lock" | `Sem -> "Sem") + (match lock_type with + | `Lock -> "Lock" + | `Rwlock -> "Rwlock" + | `Sem -> "Sem") in Times.record ~budgetf ~n_domains ~n_warmups:1 ~n_runs_min:1 ~before ~init ~wrap ~work () |> Times.to_thruput_metrics ~n:n_ops ~singular:"operation" ~config let run_suite ~budgetf = - Util.cross [ 1; 2; 4; 8 ] (Util.cross [ `Lock; `Sem ] [ 10; 50; 90; 95; 100 ]) + Util.cross [ 1; 2; 4; 8 ] + (Util.cross [ `Lock; `Rwlock; `Sem ] [ 10; 50; 90; 95; 100 ]) |> List.concat_map @@ fun (n_domains, (lock_type, percent_mem)) -> if Picos_domain.recommended_domain_count () < n_domains then [] else run_one ~budgetf ~n_domains ~percent_mem ~lock_type () diff --git a/bench/bench_lock_yield.ml b/bench/bench_lock_yield.ml index aeef9561..a8b1cc9c 100644 --- a/bench/bench_lock_yield.ml +++ b/bench/bench_lock_yield.ml @@ -20,6 +20,7 @@ let run_one ~budgetf ~n_fibers ~use_domains ~lock_type () = let n_ops_todo = Countdown.create ~n_domains () in let lock = Lock.create ~padded:true () in + let rwlock = Rwlock.create ~padded:true () in let sem = Sem.create ~padded:true (match lock_type with `Sem_n n -> n | _ -> 1) in @@ -53,6 +54,22 @@ let run_one ~budgetf ~n_fibers ~use_domains ~lock_type () = else work () in loop n + | `Rwlock -> + if n <> 0 then + let rec loop n = + if 0 < n then begin + Rwlock.acquire rwlock; + let x = !v in + v := x + 1; + Control.yield (); + assert (!v = x + 1); + v := x; + Rwlock.release rwlock; + loop (n - 1) + end + else work () + in + loop n | `Sem -> if n <> 0 then let rec loop n = @@ -102,6 +119,7 @@ let run_one ~budgetf ~n_fibers ~use_domains ~lock_type () = (if n_fibers = 1 then "" else "s") (match lock_type with | `Lock -> "Lock" + | `Rwlock -> "Rwlock" | `Sem -> "Sem" | `Sem_n n -> Printf.sprintf "Sem %d" n) in @@ -112,7 +130,7 @@ let run_one ~budgetf ~n_fibers ~use_domains ~lock_type () = let run_suite ~budgetf = Util.cross [ false; true ] (Util.cross - [ `Lock; `Sem; `Sem_n 2; `Sem_n 3; `Sem_n 4 ] + [ `Lock; `Rwlock; `Sem; `Sem_n 2; `Sem_n 3; `Sem_n 4 ] [ 1; 2; 3; 4; 8; 256; 512; 1024 ]) |> List.concat_map @@ fun (use_domains, (lock_type, n_fibers)) -> if diff --git a/bench/bench_ref.ml b/bench/bench_ref.ml index 98c55d54..5aebfbf2 100644 --- a/bench/bench_ref.ml +++ b/bench/bench_ref.ml @@ -26,6 +26,7 @@ let run_one ~budgetf ?(n_iter = 250 * Util.iter_factor) ~lock_type (Op (name, value, op1, op2, op_kind)) = let lock = Lock.create () in let sem = Sem.create 1 in + let rwlock = Rwlock.create () in let loc = Ref.make value in @@ -46,6 +47,32 @@ let run_one ~budgetf ?(n_iter = 250 * Util.iter_factor) ~lock_type end in loop n_iter + | `Rwlock, `RW -> + let rec loop i = + if i > 0 then begin + Rwlock.acquire rwlock; + op1 loc |> ignore; + Rwlock.release rwlock; + Rwlock.acquire rwlock; + op2 loc |> ignore; + Rwlock.release rwlock; + loop (i - 2) + end + in + loop n_iter + | `Rwlock, `RO -> + let rec loop i = + if i > 0 then begin + Rwlock.acquire_shared rwlock; + op1 loc |> ignore; + Rwlock.release_shared rwlock; + Rwlock.acquire_shared rwlock; + op2 loc |> ignore; + Rwlock.release_shared rwlock; + loop (i - 2) + end + in + loop n_iter | `Sem, _ -> let rec loop i = if i > 0 then begin @@ -63,13 +90,16 @@ let run_one ~budgetf ?(n_iter = 250 * Util.iter_factor) ~lock_type let config = Printf.sprintf "%s with %s" name - (match lock_type with `Lock -> "Lock" | `Sem -> "Sem") + (match lock_type with + | `Lock -> "Lock" + | `Rwlock -> "Rwlock" + | `Sem -> "Sem") in Times.record ~budgetf ~n_domains:1 ~init ~wrap ~work () |> Times.to_thruput_metrics ~n:n_iter ~singular:"op" ~config let run_suite ~budgetf = - Util.cross [ `Lock; `Sem ] + Util.cross [ `Lock; `Rwlock; `Sem ] [ (let get x = !x in Op ("get", 42, get, get, `RO)); diff --git a/lib/picos_std.sync/picos_std_sync.ml b/lib/picos_std.sync/picos_std_sync.ml index 02dcd455..164daea2 100644 --- a/lib/picos_std.sync/picos_std_sync.ml +++ b/lib/picos_std.sync/picos_std_sync.ml @@ -2,6 +2,7 @@ module Mutex = Mutex module Condition = Condition module Semaphore = Semaphore module Lock = Lock +module Rwlock = Rwlock module Sem = Sem module Lazy = Lazy module Latch = Latch diff --git a/lib/picos_std.sync/picos_std_sync.mli b/lib/picos_std.sync/picos_std_sync.mli index ca320d1d..ed0e067f 100644 --- a/lib/picos_std.sync/picos_std_sync.mli +++ b/lib/picos_std.sync/picos_std_sync.mli @@ -30,7 +30,7 @@ module Mutex : sig [~checked:false] on an operation may prevent error checking also on a subsequent operation. - See also {!Lock}. *) + See also {!Lock}, and {!Rwlock}. *) type t (** Represents a mutual-exclusion lock or mutex. *) @@ -162,9 +162,10 @@ module Lock : sig 🏎ī¸ This uses a low overhead, optimistic, and unfair implementation that also does not perform runtime ownership error checking. In most cases this - should be the mutual exclusion lock you will want to use. + should be the mutual exclusion lock you will want to use. Consider using + {!Rwlock} in case most operations are reads. - See also {!Mutex}. *) + See also {!Mutex}, and {!Rwlock}. *) type t (** Represents a mutual exclusion lock. *) @@ -247,6 +248,173 @@ module Lock : sig in case the [lock] is not currently held exclusively. *) end +module Rwlock : sig + (** A read-write lock. + + 🏎ī¸ This uses a low overhead, optimistic, and unfair implementation that + also does not perform runtime ownership error checking. In most cases this + should be the read-write lock you will want to use and should give roughly + equal or better performance than {!Lock} in cases where the majority of + operations are reads. + + 🐌 This is a "slim" lock. Acquiring the lock in read mode has low overhead, + but limited scalability. For highly parallel use cases you will either + want to use sharding or a "fat" scalable read-write lock. + + ⚠ī¸ The current implementation allows readers to bypass the queue and does + not prevent writers from starvation. For example, a pair of readers + running concurrently, acquiring and releasing the lock such that there is + never a point where the lock is fully released, prevents writers from + acquiring the lock. This might be changed in the future such that neither + readers nor writers should starve assuming no single party holds the lock + indefinitely. + + See also {!Lock}, and {!Mutex}. *) + + type t + (** Represents a read-write lock. *) + + (** {1 Basic API} *) + + val create : ?padded:bool -> unit -> t + (** [create ()] returns a new read-write lock that is initially unlocked. *) + + exception Poisoned + (** Exception raised in case the read-write lock has been + {{!poison} poisoned}. *) + + val sharing : t -> (unit -> 'a) -> 'a + (** [sharing rwlock thunk] acquires a read lock on the [rwlock] and calls + [thunk ()]. Whether [thunk ()] returns a value or raises an exception, the + [rwlock] will be unlocked. + + A single fiber may acquire a read lock on a specific [rwlock] multiple + times and other fibers may concurrently acquire read locks on the [rwlock] + as well. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. *) + + exception Frozen + (** Exception raised in case the read-write lock has been {{!freeze} frozen}. + *) + + val holding : t -> (unit -> 'a) -> 'a + (** [holding rwlock thunk] acquires a write lock on the [rwlock] and calls + [thunk ()]. In case [thunk ()] returns a value, the read-write lock is + release and the value is returned. Otherwise the read-write lock is + poisoned and the exception is reraised. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. + @raise Frozen in case the [rwlock] has been {{!freeze} frozen}. *) + + val freeze : t -> unit + (** [freeze rwlock] marks a [rwlock] as frozen, which means that one can no + longer acquire a write lock on the [rwlock]. + + ℹī¸ Freezing a [rwlock] does not improve the scalability of acquiring read + locks on the [rwlock]. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. *) + + val protect : t -> (unit -> 'a) -> 'a + (** [protect rwlock thunk] acquires a write lock the [rwlock], runs + [thunk ()], and releases the [rwlock] after [thunk ()] returns or raises. + + @raise Poisoned in case the lock has been {{!poison} poisoned}. + @raise Frozen in case the [rwlock] has been {{!freeze} frozen}. *) + + module Condition : sig + (** A condition variable. + + ⚠ī¸ The associated read-write lock must be held exclusively via {!acquire} + when used with a condition variable. *) + + include Intf.Condition with type lock = t + + val wait_shared : t -> lock -> unit + (** [wait_shared condition lock] releases the shared [lock], waits for the + [condition], and acquires the shared [lock] before returning or raising + due to the operation being canceled. + + ℹī¸ If the lock is {{!poison} poisoned} during the {!wait_shared}, then + the {!Poisoned} exception will be raised. *) + end + + (** {1 State query API} *) + + val is_locked_shared : t -> bool + (** [is_locked_shared rwlock] determines whether the [rwlock] is currently + read locked or not. + + ⚠ī¸ [is_locked_shared rwlock] will return [false] in case the [rwlock] is + write locked. *) + + val is_frozen : t -> bool + (** [is_frozen rwlock] determines whether the [rwlock] has been + {{!freeze} frozen}. *) + + val is_locked : t -> bool + (** [is_locked rwlock] determines whether the [rwlock] is currently write + locked or not. + + ⚠ī¸ [is_locked rwlock] will return [false] in case the [rwlock] is read + locked. *) + + val is_poisoned : t -> bool + (** [is_poisoned rwlock] determines whether the [rwlock] has been + {{!poison} poisoned}. *) + + (** {1 Expert API} + + ⚠ī¸ The calls in this section must be matched correctly or the state of the + read-write lock may become corrupted. *) + + val acquire_shared : t -> unit + (** [acquire_shared rwlock] acquires a read lock on the [rwlock]. + + A single fiber may acquire a read lock on a specific [rwlock] multiple + times and other fibers may concurrently acquire read locks on the [rwlock] + as well. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. *) + + val try_acquire_shared : t -> bool + (** [try_acquire_shared rwlock] attempts to acquire a read lock on the + [rwlock]. Returns [true] in case of success and [false] in case of + failure. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. *) + + val release_shared : t -> unit + (** [release_shared rwlock] release one read lock on the read-write lock or + does nothing in case the lock has been {{!poison} poisoned}. *) + + val acquire : t -> unit + (** [acquire rwlock] acquires a write lock on the [rwlock]. + + A fiber may acquire a write lock on a specific [rwlock] once at a time. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. + @raise Frozen in case the [rwlock] has been {{!freeze} frozen}. *) + + val try_acquire : t -> bool + (** [try_acquire rwlock] attempts to acquire a write lock on the [rwlock]. + Returns [true] in case of success and [false] in case of failure. + + @raise Poisoned in case the [rwlock] has been {{!poison} poisoned}. + @raise Frozen in case the [rwlock] has been {{!freeze} frozen}. *) + + val release : t -> unit + (** [release rwlock] releases the write lock on the read-write lock or does + nothing in case the read-write lock has been {{!poison} poisoned}. *) + + val poison : t -> unit + (** [poison rwlock] marks a write locked [rwlock] as poisoned. + + @raise Invalid_argument + in case the [rwlock] is not currently write locked. *) +end + module Sem : sig (** A counting semaphore. diff --git a/lib/picos_std.sync/rwlock.ml b/lib/picos_std.sync/rwlock.ml new file mode 100644 index 00000000..24610281 --- /dev/null +++ b/lib/picos_std.sync/rwlock.ml @@ -0,0 +1,179 @@ +open Picos_std_awaitable + +(** TODO: Should we try to prevent writers from starvation? *) + +type t = int Awaitable.t + +let no_writers = 1 lsl 0 +let no_readers = 1 lsl 1 +let no_awaiters = no_readers lor no_writers +let shared = 1 lsl 2 +let shared_permanently = 1 lsl (Sys.int_size - 5) +let exclusive = 1 lsl (Sys.int_size - 4) +let exclusive_permanently = 1 lsl (Sys.int_size - 2) + +exception Poisoned +exception Frozen + +let acquire t = + let before = no_awaiters in + let after = exclusive lor no_awaiters in + if not (Awaitable.compare_and_set t before after) then + let rec acquire_awaiting t = + let before = Awaitable.get t in + if before < shared then begin + let after = before land lnot no_writers lor exclusive in + if not (Awaitable.compare_and_set t before after) then + acquire_awaiting t + end + else if shared_permanently / 2 <= before land lnot exclusive then + raise (if exclusive < before then Poisoned else Frozen) + else + let after = before land lnot no_writers in + if before = after || Awaitable.compare_and_set t before after then + Awaitable.await t after; + acquire_awaiting t + in + acquire_awaiting t + +let acquire_shared t = + let prior = Awaitable.fetch_and_add t shared in + if exclusive <= prior then + let rec acquire_shared_awaiting t = + let before = Awaitable.get t in + if before < exclusive then begin + let after = (before + shared) land lnot no_readers in + if not (Awaitable.compare_and_set t before after) then + acquire_shared_awaiting t + end + else if exclusive_permanently / 2 <= before then raise Poisoned + else + let after = before land lnot no_readers in + if before = after || Awaitable.compare_and_set t before after then + Awaitable.await t after; + acquire_shared_awaiting t + in + let rec acquire_shared_contended t = + let before = Awaitable.get t in + if exclusive <= before then + let after = (before - shared) land lnot no_readers in + if Awaitable.compare_and_set t before after then + acquire_shared_awaiting t + else acquire_shared_contended t + in + acquire_shared_contended t + +let release t = + let before = exclusive lor no_awaiters in + let after = no_awaiters in + if not (Awaitable.compare_and_set t before after) then + let rec release_contended t = + let before = Awaitable.get t in + if before land lnot exclusive < shared_permanently / 2 then + let after = before land lnot exclusive lor no_awaiters in + if Awaitable.compare_and_set t before after then begin + if before land no_awaiters <> no_awaiters then + if before land no_readers = 0 then Awaitable.broadcast t + else Awaitable.signal t + end + else release_contended t + in + release_contended t + +let release_shared t = + let prior = Awaitable.fetch_and_add t (-shared) in + if prior < shared lor no_awaiters then + let rec signal_awaiters t = + let before = Awaitable.get t in + if before < no_awaiters then + if Awaitable.compare_and_set t before (before lor no_awaiters) then + if no_readers <= before then Awaitable.signal t + else Awaitable.broadcast t + else signal_awaiters t + in + signal_awaiters t + else if exclusive_permanently / 2 < prior then + let undo_release t = + let _ : int = Awaitable.fetch_and_add t shared in + () + in + undo_release t + +let rec poison t = + let before = Awaitable.get t in + if before < exclusive then invalid_arg "not write locked"; + (* Unfortunately we cannot check ownership at this point. *) + if before < exclusive_permanently / 2 then + let after = exclusive_permanently lor no_awaiters in + if Awaitable.compare_and_set t before after then Awaitable.broadcast t + else poison t + +let freeze t = + acquire_shared t; + let before = ref (Awaitable.get t) in + while + !before < shared_permanently / 2 + && + let after = (!before + shared_permanently) lor no_awaiters in + (* This leaves the rwlock as read locked. *) + not (Awaitable.compare_and_set t !before after) + do + before := Awaitable.get t + done; + (* We must wake up any writers waiting to obtain the lock. *) + if !before land no_awaiters <> no_awaiters then Awaitable.broadcast t; + release_shared t + +let holding t thunk = Locks.holding t thunk ~acquire ~release ~poison +let protect t thunk = Locks.protect t thunk ~acquire ~release + +let sharing t thunk = + acquire_shared t; + match thunk () with + | value -> + release_shared t; + value + | exception exn -> + let bt = Printexc.get_raw_backtrace () in + release_shared t; + Printexc.raise_with_backtrace exn bt + +let try_acquire t = + let before = Awaitable.get t in + (before < shared + && + let after = before + exclusive in + Awaitable.compare_and_set t before after) + || shared_permanently / 2 <= before land lnot exclusive + && raise (if exclusive < before then Poisoned else Frozen) + +let try_acquire_shared t = + let prior = Awaitable.fetch_and_add t shared in + prior < exclusive + || + let prior = Awaitable.fetch_and_add t (-shared) in + exclusive_permanently / 2 <= prior && raise Poisoned + +let[@inline] create ?padded () = Awaitable.make ?padded no_awaiters +let[@inline] is_locked t = exclusive <= Awaitable.get t + +let[@inline] is_frozen t = + let state = Awaitable.get t in + shared_permanently / 2 <= state && state < exclusive + +let[@inline] is_poisoned t = exclusive_permanently / 2 <= Awaitable.get t + +let[@inline] is_locked_shared t = + let state = Awaitable.get t in + shared <= state && state < exclusive + +module Condition = struct + type lock = t + + include Conditions + + let wait_shared condition lock = + wait condition lock ~acquire:acquire_shared ~release:release_shared + + let wait condition lock = wait condition lock ~acquire ~release +end diff --git a/test/dune b/test/dune index 19846d25..72824f54 100644 --- a/test/dune +++ b/test/dune @@ -45,6 +45,13 @@ (run %{test} -- "^Lock and Lock.Condition$" 1) (run %{test} -- "^Lock and Lock.Condition$" 2) (run %{test} -- "^Lock and Lock.Condition$" 3) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 0) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 1) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 2) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 3) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 4) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 5) + (run %{test} -- "^Rwlock and Rwlock.Condition$" 6) ;; ))) @@ -66,6 +73,12 @@ (modules test_sem) (libraries picos picos_std.sync stm_run stm_wrap)) +(test + (package picos_meta) + (name test_rwlock) + (modules test_rwlock) + (libraries picos picos_std.sync stm_run stm_wrap)) + ;; (test diff --git a/test/test_rwlock.ml b/test/test_rwlock.ml new file mode 100644 index 00000000..88bdf5f7 --- /dev/null +++ b/test/test_rwlock.ml @@ -0,0 +1,80 @@ +open QCheck +open STM +open Picos_std_sync + +module Spec = struct + include SpecDefaults + include Stm_wrap + + 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 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.acquire d.rwlock; + Stack.push x d.stack; + Rwlock.release d.rwlock; + Res (unit, ()) + | Pop_opt -> + Rwlock.acquire d.rwlock; + let result = Stack.pop_opt d.stack in + Rwlock.release d.rwlock; + Res (option int, result) + | Top_opt -> + Rwlock.acquire_shared d.rwlock; + let result = Stack.top_opt d.stack in + Rwlock.release_shared d.rwlock; + Res (option int, result) + | Length -> + Rwlock.acquire_shared d.rwlock; + let result = Stack.length d.stack in + Rwlock.release_shared 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 +end + +let () = Stm_run.run ~name:"Rwlock" (module Spec) |> exit diff --git a/test/test_sync.ml b/test/test_sync.ml index dfd018c7..b219e277 100644 --- a/test/test_sync.ml +++ b/test/test_sync.ml @@ -480,6 +480,133 @@ module Lock_and_condition_tests = struct include Make_lock_tests (Lock) end +module Rwlock_and_condition_tests = struct + include + Make_mutex_and_condition_tests + (struct + include Rwlock + + let lock ?checked:_ = acquire + let unlock ?checked:_ = release + let protect ?checked:_ = holding + end) + (Rwlock.Condition) + + include Make_lock_tests (Rwlock) + + let test_sharing () = + Test_scheduler.run @@ fun () -> + begin + let lock = Rwlock.create () in + Flock.join_after @@ fun () -> + Rwlock.acquire lock; + for _ = 0 to Random.int 3 do + Flock.fork @@ fun () -> + match Rwlock.acquire_shared lock with + | () -> assert false + | exception Rwlock.Poisoned -> () + done; + Rwlock.poison lock; + assert (not (Rwlock.is_locked_shared lock)); + assert (Rwlock.is_locked lock); + assert (Rwlock.is_poisoned lock); + Rwlock.release lock; + assert (Rwlock.is_locked lock); + assert (Rwlock.is_poisoned lock) + end; + begin + let lock = Rwlock.create () in + let condition = Rwlock.Condition.create () in + Flock.join_after @@ fun () -> + begin + Flock.fork @@ fun () -> + match + Rwlock.sharing lock @@ fun () -> + assert (Rwlock.is_locked_shared lock); + while true do + Rwlock.Condition.wait_shared condition lock + done + with + | () -> assert false + | exception Rwlock.Poisoned -> () + end; + begin + match Rwlock.holding lock @@ fun () -> raise Exit with + | () -> assert false + | exception Exit -> assert (Rwlock.is_poisoned lock) + end; + Rwlock.Condition.broadcast condition; + begin + match Rwlock.acquire lock with + | () -> assert false + | exception Rwlock.Poisoned -> () + end; + begin + match + Rwlock.sharing lock @@ fun () -> + while true do + Rwlock.Condition.wait_shared condition lock + done + with + | () -> assert false + | exception Rwlock.Poisoned -> () + end; + assert (not (Rwlock.is_locked_shared lock)); + assert (Rwlock.is_locked lock); + assert (Rwlock.is_poisoned lock) + end; + () + + let test_freezing () = + Test_scheduler.run @@ fun () -> + begin + let rwlock = Rwlock.create () in + Flock.join_after @@ fun () -> + Rwlock.acquire_shared rwlock; + for _ = 0 to Random.int 3 do + Flock.fork @@ fun () -> + match Rwlock.acquire rwlock with + | () -> assert false + | exception Rwlock.Frozen -> () + done; + Rwlock.freeze rwlock; + for _ = 0 to Random.int 3 do + Flock.fork @@ fun () -> + match Rwlock.acquire_shared rwlock with + | () -> Rwlock.release_shared rwlock + | (exception Rwlock.Frozen) | (exception Rwlock.Poisoned) -> + assert false + done + end + + let test_try_acquire_shared () = + Test_scheduler.run ~max_domains:2 @@ fun () -> + begin + let lock = Rwlock.create () in + assert (Rwlock.try_acquire_shared lock); + assert (Rwlock.try_acquire_shared lock); + Rwlock.release_shared lock; + Rwlock.release_shared lock; + Rwlock.acquire lock; + assert (not (Rwlock.try_acquire_shared lock)); + Rwlock.poison lock; + match Rwlock.try_acquire_shared lock with + | _ -> assert false + | exception Rwlock.Poisoned -> () + end; + begin + let lock = Rwlock.create () in + assert (Rwlock.try_acquire_shared lock); + Rwlock.freeze lock; + match Rwlock.try_acquire lock with + | _ -> assert false + | exception Rwlock.Frozen -> () + end; + () +end + +module Rwlock_is_a_submodule_of_Lock : module type of Lock = Rwlock + let () = try [ @@ -502,6 +629,23 @@ let () = Alcotest.test_case "try_acquire" `Quick Lock_and_condition_tests.test_try_acquire; ] ); + ( "Rwlock and Rwlock.Condition", + [ + Alcotest.test_case "basics" `Quick + Rwlock_and_condition_tests.test_basics; + Alcotest.test_case "cancelation" `Quick + Rwlock_and_condition_tests.test_cancelation; + Alcotest.test_case "poisoning" `Quick + Rwlock_and_condition_tests.test_poisoning; + Alcotest.test_case "freezing" `Quick + Rwlock_and_condition_tests.test_freezing; + Alcotest.test_case "try_acquire" `Quick + Rwlock_and_condition_tests.test_try_acquire; + Alcotest.test_case "try_acquire_shared" `Quick + Rwlock_and_condition_tests.test_try_acquire_shared; + Alcotest.test_case "sharing" `Quick + Rwlock_and_condition_tests.test_sharing; + ] ); ( "Semaphore", [ Alcotest.test_case "basics" `Quick Semaphore_tests.test_basics;