From 0c1f13422cb5e7601dbddd771a7977a0d54f5cc1 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Mon, 9 Sep 2024 13:59:02 +0200 Subject: [PATCH 01/16] Hashtable --- src/saturn.ml | 2 + src/saturn.mli | 2 + src_lockfree/htbl/htbl.ml | 542 ++++++++++++++++++++++++++++++ src_lockfree/htbl/htbl.mli | 1 + src_lockfree/htbl/htbl_intf.ml | 124 +++++++ src_lockfree/htbl/htbl_unsafe.ml | 517 ++++++++++++++++++++++++++++ src_lockfree/htbl/htbl_unsafe.mli | 1 + src_lockfree/saturn_lockfree.ml | 2 + src_lockfree/saturn_lockfree.mli | 2 + test/htbl/dune | 48 +++ test/htbl/htbls/dune | 10 + test/htbl/htbls/htbls.ml | 17 + test/htbl/stm_htbl.ml | 96 ++++++ 13 files changed, 1364 insertions(+) create mode 100644 src_lockfree/htbl/htbl.ml create mode 100644 src_lockfree/htbl/htbl.mli create mode 100644 src_lockfree/htbl/htbl_intf.ml create mode 100644 src_lockfree/htbl/htbl_unsafe.ml create mode 100644 src_lockfree/htbl/htbl_unsafe.mli create mode 100644 test/htbl/dune create mode 100644 test/htbl/htbls/dune create mode 100644 test/htbl/htbls/htbls.ml create mode 100644 test/htbl/stm_htbl.ml diff --git a/src/saturn.ml b/src/saturn.ml index b278fd7f..f8464bae 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -40,3 +40,5 @@ module Single_prod_single_cons_queue_unsafe = module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue module Relaxed_queue = Mpmc_relaxed_queue module Skiplist = Saturn_lockfree.Skiplist +module Htbl = Saturn_lockfree.Htbl +module Htbl_unsafe = Saturn_lockfree.Htbl_unsafe diff --git a/src/saturn.mli b/src/saturn.mli index fe22808a..2906447c 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -44,3 +44,5 @@ module Single_prod_single_cons_queue_unsafe = module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue module Relaxed_queue = Mpmc_relaxed_queue module Skiplist = Saturn_lockfree.Skiplist +module Htbl = Saturn_lockfree.Htbl +module Htbl_unsafe = Saturn_lockfree.Htbl_unsafe diff --git a/src_lockfree/htbl/htbl.ml b/src_lockfree/htbl/htbl.ml new file mode 100644 index 00000000..f7aea678 --- /dev/null +++ b/src_lockfree/htbl/htbl.ml @@ -0,0 +1,542 @@ +(* Copyright (c) 2023 Vesa Karvonen + + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. + + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH + REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY + AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, + INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM + LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR + OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR + PERFORMANCE OF THIS SOFTWARE. *) + +let[@inline never] impossible () = failwith "impossible" + +let ceil_pow_2_minus_1 n = + let n = Nativeint.of_int n in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 1) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 2) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 4) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 8) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 16) in + Nativeint.to_int + (if Sys.int_size > 32 then + Nativeint.logor n (Nativeint.shift_right_logical n 32) + else n) + +module Atomic_array = struct + type 'a t = 'a Atomic.t array + + let[@inline] at (xs : 'a t) i : 'a Atomic.t = Array.get xs i + let[@inline] make n v = Array.init n @@ fun _ -> Atomic.make v + + external length : 'a array -> int = "%array_length" + + let unsafe_fenceless_get xs i = Atomic.get xs.(i) + + let[@inline] unsafe_compare_and_set xs i b a = + Atomic.compare_and_set (at xs i) b a +end + +type 'k hashed_type = (module Stdlib.Hashtbl.HashedType with type t = 'k) + +type ('k, 'v, _) tdt = + | Nil : ('k, 'v, [> `Nil ]) tdt + | Cons : { + key : 'k; + value : 'v; + rest : ('k, 'v, [ `Nil | `Cons ]) tdt; + } + -> ('k, 'v, [> `Cons ]) tdt + | Resize : { + spine : ('k, 'v, [ `Nil | `Cons ]) tdt; + } + -> ('k, 'v, [> `Resize ]) tdt + (** During resizing and snapshotting target buckets will be initialized + with a physically unique [Resize] value and the source buckets will + then be gradually updated to [Resize] values and the target buckets + updated with data from the source buckets. *) + +type ('k, 'v) bucket = + | B : ('k, 'v, [< `Nil | `Cons | `Resize ]) tdt -> ('k, 'v) bucket +[@@unboxed] + +type ('k, 'v) pending = + | Nothing + | Resize of { + buckets : ('k, 'v) bucket Atomic_array.t; + non_linearizable_size : int Atomic.t array; + } + +type ('k, 'v) state = { + hash : 'k -> int; + buckets : ('k, 'v) bucket Atomic_array.t; + equal : 'k -> 'k -> bool; + non_linearizable_size : int Atomic.t array; + pending : ('k, 'v) pending; + min_buckets : int; + max_buckets : int; +} +(** This record is [7 + 1] words and should be aligned on such a boundary on the + second generation heap. It is probably not worth it to pad it further. *) + +type ('k, 'v) t = ('k, 'v) state Atomic.t + +(* *) + +let lo_buckets = 1 lsl 3 + +and hi_buckets = + (* floor_pow_2 *) + let mask = ceil_pow_2_minus_1 Sys.max_array_length in + mask lxor (mask lsr 1) + +let min_buckets_default = 1 lsl 4 +and max_buckets_default = Int.min hi_buckets (1 lsl 30 (* Limit of [hash] *)) + +let create (type k) ?hashed_type ?min_buckets ?max_buckets () = + let min_buckets = + match min_buckets with + | None -> min_buckets_default + | Some n -> + let n = Int.max lo_buckets n |> Int.min hi_buckets in + ceil_pow_2_minus_1 (n - 1) + 1 + in + let max_buckets = + match max_buckets with + | None -> Int.max min_buckets max_buckets_default + | Some n -> + let n = Int.max min_buckets n |> Int.min hi_buckets in + ceil_pow_2_minus_1 (n - 1) + 1 + in + let equal, hash = + match hashed_type with + | None -> + (( = ), Stdlib.Hashtbl.seeded_hash (Int64.to_int (Random.bits64 ()))) + | Some ((module Hashed_type) : k hashed_type) -> + (Hashed_type.equal, Hashed_type.hash) + in + { + hash; + buckets = Atomic_array.make min_buckets (B Nil); + equal; + non_linearizable_size = + Array.init + (ceil_pow_2_minus_1 + (Multicore_magic.instantaneous_domain_index () lor 1) + (* Calling [...index ()] helps to ensure [at_exit] processing does + not raise. This also potentially adjusts the counter width for + the number of domains. *)) + (fun _ -> Atomic.make_contended 0); + pending = Nothing; + min_buckets; + max_buckets; + } + |> Atomic.make_contended + +(* *) + +let hashed_type_of (type k) (t : (k, _) t) : k hashed_type = + let r = Atomic.get t in + (module struct + type t = k + + let hash = r.hash + and equal = r.equal + end) + +let min_buckets_of t = (Atomic.get t).min_buckets +let max_buckets_of t = (Atomic.get t).max_buckets + +(* *) + +let rec take_at backoff bs i = + match Atomic_array.unsafe_fenceless_get bs i with + | B ((Nil | Cons _) as spine) -> + if + Atomic_array.unsafe_compare_and_set bs i (B spine) + (B (Resize { spine })) + then spine + else take_at (Backoff.once backoff) bs i + | B (Resize spine_r) -> spine_r.spine + +let rec copy_all r target i t step = + let i = (i + step) land (Atomic_array.length target - 1) in + let spine = take_at Backoff.default r.buckets i in + let (B before) = Atomic_array.unsafe_fenceless_get target i in + (* The [before] value is physically different for each resize and so checking + that the resize has not finished is sufficient to ensure that the + [compare_and_set] below does not disrupt the next resize. *) + Atomic.get t == r + && begin + begin + match before with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target i (B before) (B spine) + |> ignore + | Nil | Cons _ -> () + end; + i = 0 || copy_all r target i t step + end + +(* *) + +let[@tail_mod_cons] rec filter t msk chk = function + | Nil -> Nil + | Cons r -> + if t r.key land msk = chk then + Cons { r with rest = filter t msk chk r.rest } + else filter t msk chk r.rest + +let rec split_all r target i t step = + let i = (i + step) land (Atomic_array.length r.buckets - 1) in + let spine = take_at Backoff.default r.buckets i in + let high = Atomic_array.length r.buckets in + let after_lo = filter r.hash high 0 spine in + let after_hi = filter r.hash high high spine in + let (B before_lo) = Atomic_array.unsafe_fenceless_get target i in + let (B before_hi) = Atomic_array.unsafe_fenceless_get target (i + high) in + (* The [before_lo] and [before_hi] values are physically different for each + resize and so checking that the resize has not finished is sufficient to + ensure that the [compare_and_set] below does not disrupt the next + resize. *) + Atomic.get t == r + && begin + begin + match before_lo with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target i (B before_lo) + (B after_lo) + |> ignore + | Nil | Cons _ -> () + end; + begin + match before_hi with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target (i + high) (B before_hi) + (B after_hi) + |> ignore + | Nil | Cons _ -> () + end; + i = 0 || split_all r target i t step + end + +(* *) + +let[@tail_mod_cons] rec merge rest = function + | Nil -> rest + | Cons r -> Cons { r with rest = merge rest r.rest } + +let rec merge_all r target i t step = + let i = (i + step) land (Atomic_array.length target - 1) in + let spine_lo = take_at Backoff.default r.buckets i in + let spine_hi = + take_at Backoff.default r.buckets (i + Atomic_array.length target) + in + let ((Nil | Cons _) as after) = merge spine_lo spine_hi in + let (B before) = Atomic_array.unsafe_fenceless_get target i in + (* The [before] value is physically different for each resize and so checking + that the resize has not finished is sufficient to ensure that the + [compare_and_set] below does not disrupt the next resize. *) + Atomic.get t == r + && begin + begin + match before with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target i (B before) (B after) + |> ignore + | Nil | Cons _ -> () + end; + i = 0 || merge_all r target i t step + end + +(* *) + +let[@inline never] rec finish t r = + match r.pending with + | Nothing -> r + | Resize { buckets; non_linearizable_size } -> + let high_source = Atomic_array.length r.buckets in + let high_target = Atomic_array.length buckets in + (* We step by random amount to better allow cores to work in parallel. + The number of buckets is always a power of two, so any odd number is + relatively prime or coprime. *) + let step = Int64.to_int (Random.bits64 ()) lor 1 in + if + if high_source < high_target then begin + (* We are growing the table. *) + split_all r buckets 0 t step + end + else if high_target < high_source then begin + (* We are shrinking the table. *) + merge_all r buckets 0 t step + end + else begin + (* We are snaphotting the table. *) + copy_all r buckets 0 t step + end + then + let new_r = + { r with buckets; non_linearizable_size; pending = Nothing } + in + if Atomic.compare_and_set t r new_r then new_r + else finish t (Atomic.get t) + else finish t (Atomic.get t) + +(* *) + +let rec estimated_size cs n sum = + let n = n - 1 in + if 0 <= n then estimated_size cs n (sum + Atomic.get (Array.unsafe_get cs n)) + else sum + +(** This only gives an "estimate" of the size, which can be off by one or more + and even be negative, so this must be used with care. *) +let estimated_size r = + let cs = r.non_linearizable_size in + let n = Array.length cs - 1 in + estimated_size cs n (Atomic.get (Array.unsafe_get cs n)) + +(** This must be called with [r.pending == Nothing]. *) +let[@inline never] try_resize t r new_capacity ~clear = + (* We must make sure that on every resize we use a physically different + [Resize _] value to indicate unprocessed target buckets. The use of + [Sys.opaque_identity] below ensures that a new value is allocated. *) + let resize_avoid_aba = + if clear then B Nil else B (Resize { spine = Sys.opaque_identity Nil }) + in + let buckets = Atomic_array.make new_capacity resize_avoid_aba in + let non_linearizable_size = + if clear then + Array.init (Array.length r.non_linearizable_size) @@ fun _ -> + Atomic.make_contended 0 + else r.non_linearizable_size + in + let new_r = { r with pending = Resize { buckets; non_linearizable_size } } in + Atomic.compare_and_set t r new_r + && begin + finish t new_r |> ignore; + true + end + +let rec adjust_estimated_size t r mask delta result = + let i = Multicore_magic.instantaneous_domain_index () in + let n = Array.length r.non_linearizable_size in + if i < n then begin + Atomic.fetch_and_add (Array.unsafe_get r.non_linearizable_size i) delta + |> ignore; + (* Reading the size is potentially expensive, so we only check it + occasionally. The bigger the table the less frequently we should need to + resize. *) + if + r.pending == Nothing + && Int64.to_int (Random.bits64 ()) land mask = 0 + && Atomic.get t == r + then begin + let estimated_size = estimated_size r in + let capacity = Atomic_array.length r.buckets in + if capacity < estimated_size && capacity < r.max_buckets then + try_resize t r (capacity + capacity) ~clear:false |> ignore + else if + r.min_buckets < capacity + && estimated_size + estimated_size + estimated_size < capacity + then try_resize t r (capacity lsr 1) ~clear:false |> ignore + end; + result + end + else + let new_cs = + (* We use [n + n + 1] as it keeps the length of the array as a power of 2 + minus 1 and so the size of the array/block including header word will + be a power of 2. *) + Array.init (n + n + 1) @@ fun i -> + if i < n then Array.unsafe_get r.non_linearizable_size i + else Atomic.make_contended 0 + in + let new_r = { r with non_linearizable_size = new_cs } in + let r = if Atomic.compare_and_set t r new_r then new_r else Atomic.get t in + adjust_estimated_size t r mask delta result + +(* *) + +(** [get] only returns with a state where [pending = Nothing]. *) +let[@inline] get t = + let r = Atomic.get t in + if r.pending == Nothing then r else finish t r + +(* *) + +let rec assoc_node t key = function + | Nil -> (Nil : (_, _, [< `Nil | `Cons ]) tdt) + | Cons r as cons -> if t r.key key then cons else assoc_node t key r.rest + +let find_node t key = + (* Reads can proceed in parallel with writes. *) + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + match Atomic_array.unsafe_fenceless_get r.buckets i with + | B Nil -> Nil + | B (Cons cons_r as cons) -> + if r.equal cons_r.key key then cons + else assoc_node r.equal key cons_r.rest + | B (Resize resize_r) -> + (* A resize is in progress. The spine of the resize still holds what was + in the bucket before resize reached that bucket. *) + assoc_node r.equal key resize_r.spine + +(* *) + +let find_exn t key = + match find_node t key with + | Nil -> raise_notrace Not_found + | Cons r -> r.value + +let mem t key = find_node t key != Nil + +(* *) + +let rec try_add t key value backoff = + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + match Atomic_array.unsafe_fenceless_get r.buckets i with + | B Nil -> + let after = Cons { key; value; rest = Nil } in + if Atomic_array.unsafe_compare_and_set r.buckets i (B Nil) (B after) then + adjust_estimated_size t r mask 1 true + else try_add t key value (Backoff.once backoff) + | B (Cons _ as before) -> + if assoc_node r.equal key before != Nil then false + else + let after = Cons { key; value; rest = before } in + if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) + then adjust_estimated_size t r mask 1 true + else try_add t key value (Backoff.once backoff) + | B (Resize _) -> + let _ = finish t (Atomic.get t) in + try_add t key value Backoff.default + +let[@inline] try_add t key value = try_add t key value Backoff.default + +(* *) + +let[@tail_mod_cons] rec dissoc t key = function + | Nil -> raise_notrace Not_found + | Cons r -> + if t key r.key then r.rest else Cons { r with rest = dissoc t key r.rest } + +let rec remove_node t key backoff = + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + match Atomic_array.unsafe_fenceless_get r.buckets i with + | B Nil -> Nil + | B (Cons cons_r as before) -> begin + if r.equal cons_r.key key then + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B cons_r.rest) + then adjust_estimated_size t r mask (-1) before + else remove_node t key (Backoff.once backoff) + else + match dissoc r.equal key cons_r.rest with + | (Nil | Cons _) as rest -> + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B (Cons { cons_r with rest })) + then + assoc_node r.equal key cons_r.rest + |> adjust_estimated_size t r mask (-1) + else remove_node t key (Backoff.once backoff) + | exception Not_found -> Nil + end + | B (Resize _) -> + let _ = finish t (Atomic.get t) in + remove_node t key Backoff.default + +let try_remove t key = remove_node t key Backoff.default != Nil + +let remove_exn t key = + match remove_node t key Backoff.default with + | Nil -> raise_notrace Not_found + | Cons r -> r.value + +(* *) + +let rec snapshot t ~clear backoff = + let r = get t in + if try_resize t r (Atomic_array.length r.buckets) ~clear then begin + (* At this point the resize has been completed and a new array is used for + buckets and [r.buckets] now has an immutable copy of what was in the hash + table. *) + let snapshot = r.buckets in + let rec loop i kvs () = + match kvs with + | Nil -> + if i = Atomic_array.length snapshot then Seq.Nil + else + loop (i + 1) + (match Atomic_array.unsafe_fenceless_get snapshot i with + | B (Resize spine_r) -> spine_r.spine + | B (Nil | Cons _) -> + (* After resize only [Resize] values should be left in the old + buckets. *) + assert false) + () + | Cons r -> Seq.Cons ((r.key, r.value), loop i r.rest) + in + loop 0 Nil + end + else snapshot t ~clear (Backoff.once backoff) + +let to_seq t = snapshot t ~clear:false Backoff.default +let remove_all t = snapshot t ~clear:true Backoff.default + +(* *) + +let rec try_find_random_non_empty_bucket buckets seed i = + match Atomic_array.unsafe_fenceless_get buckets i with + | B Nil | B (Resize { spine = Nil }) -> + let mask = Atomic_array.length buckets - 1 in + let i = (i + 1) land mask in + if i <> seed land mask then + try_find_random_non_empty_bucket buckets seed i + else Nil + | B (Cons cons_r) | B (Resize { spine = Cons cons_r }) -> Cons cons_r + +let try_find_random_non_empty_bucket t = + let buckets = (Atomic.get t).buckets in + let seed = Int64.to_int (Random.bits64 ()) in + try_find_random_non_empty_bucket buckets seed + (seed land (Atomic_array.length buckets - 1)) + +let rec length spine n = + match spine with Nil -> n | Cons r -> length r.rest (n + 1) + +let length spine = length spine 0 + +let rec nth spine i = + match spine with + | Nil -> impossible () + | Cons r -> if i <= 0 then r.key else nth r.rest (i - 1) + +let find_random_exn t = + match try_find_random_non_empty_bucket t with + | (Cons cons_r as spine : (_, _, [< `Nil | `Cons ]) tdt) -> + (* We found a non-empty bucket - the fast way. *) + if cons_r.rest == Nil then cons_r.key + else + let n = length spine in + nth spine (Random.int n) + | Nil -> + (* We couldn't find a non-empty bucket - the slow way. *) + let bindings = to_seq t |> Array.of_seq in + let n = Array.length bindings in + if n <> 0 then fst (Array.unsafe_get bindings (Random.int n)) + else raise_notrace Not_found diff --git a/src_lockfree/htbl/htbl.mli b/src_lockfree/htbl/htbl.mli new file mode 100644 index 00000000..ba768a89 --- /dev/null +++ b/src_lockfree/htbl/htbl.mli @@ -0,0 +1 @@ +include Htbl_intf.HTBL diff --git a/src_lockfree/htbl/htbl_intf.ml b/src_lockfree/htbl/htbl_intf.ml new file mode 100644 index 00000000..af31dbfc --- /dev/null +++ b/src_lockfree/htbl/htbl_intf.ml @@ -0,0 +1,124 @@ +module type HTBL = sig + (** Lock-free hash table. + + 🏎ī¸ Single key reads with this hash table are actually wait-free rather than + just lock-free. Internal resizing automatically uses all the threads that + are trying to write to the hash table. *) + + (** {1 API} *) + + type (!'k, !'v) t + (** Represents a lock-free hash table mapping keys of type ['k] to values of + type ['v]. *) + + type 'k hashed_type = (module Stdlib.Hashtbl.HashedType with type t = 'k) + (** First-class module type abbreviation. *) + + val create : + ?hashed_type:'k hashed_type -> + ?min_buckets:int -> + ?max_buckets:int -> + unit -> + ('k, 'v) t + (** [create ~hashed_type:(module Key) ()] creates a new empty lock-free hash + table. + + - The optional [hashed_type] argument can and usually should be used to + specify the [equal] and [hash] operations on keys. Slow polymorphic + equality [(=)] and slow polymorphic {{!Stdlib.Hashtbl.seeded_hash} [seeded_hash (Bits64.to_int (Random.bits64 ()))]} + is used by default. + - The default [min_buckets] is unspecified and a given [min_buckets] may be + adjusted by the implementation. + - The default [max_buckets] is unspecified and a given [max_buckets] may be + adjusted by the implementation. *) + + val hashed_type_of : ('k, 'v) t -> 'k hashed_type + (** [hashed_type_of htbl] returns a copy of the hashed type used when the hash + table [htbl] was created. *) + + val min_buckets_of : ('k, 'v) t -> int + (** [min_buckets_of htbl] returns the minimum number of buckets of the hash + table [htbl]. + + ℹī¸ The returned value may not be the same as given to {!create}. *) + + val max_buckets_of : ('k, 'v) t -> int + (** [max_buckets_of htbl] returns the maximum number of buckets of the hash + table [htbl]. + + ℹī¸ The returned value may not be the same as given to {!create}. *) + + (** {2 Looking up bindings} *) + + val find_exn : ('k, 'v) t -> 'k -> 'v + (** [find_exn htbl key] returns the current binding of [key] in the hash table + [htbl] or raises {!Not_found} if no such binding exists. *) + + val mem : ('k, 'v) t -> 'k -> bool + (** [mem htbl key] determines whether the hash table [htbl] has a binding for + the [key]. *) + + val to_seq : ('k, 'v) t -> ('k * 'v) Seq.t + (** [to_seq htbl] takes a snapshot of the bindings in the hash table and returns + them as an association sequence. + + 🐌 This is a linear time operation. *) + + val find_random_exn : ('k, 'v) t -> 'k + (** [find_random_exn htbl] tries to find a random binding from the hash table + and returns the key of the binding or raises {!Not_found} in case the hash + table is empty. + + 🐌 This is an expected constant time operation with worst case linear time + complexity. *) + + (** {2 Adding bindings} *) + + val try_add : ('k, 'v) t -> 'k -> 'v -> bool + (** [try_add htbl key value] tries to add a new binding of [key] to [value] to + the hash table [htbl]. Returns [true] on success and [false] in case the + hash table already contained a binding for [key]. *) + + (** {2 Removing bindings} *) + + val try_remove : ('k, 'v) t -> 'k -> bool + (** [try_remove htbl key] tries to remove a binding of [key] from the hash table + [htbl]. Returns [true] on success and [false] in case the hash table did + not contain a binding for [key]. *) + + val remove_exn : ('k, 'v) t -> 'k -> 'v + (** [remove_exn htbl key] tries to remove a binding of [key] from the hash table + [htbl] and return it or raise {!Not_found} if no such binding exists. *) + + val remove_all : ('k, 'v) t -> ('k * 'v) Seq.t + (** [remove_all htbl] takes a snapshot of the bindings in the hash table, + removes the bindings from the hash table, and returns the snapshot as an + association sequence. + + 🐌 This is a linear time operation. *) + + (** {1 Examples} + + An example top-level session: + {[ + # let t : (int, string) Picos_aux_htbl.t = + Picos_aux_htbl.create + ~hashed_type:(module Int) () + val t : (int, string) Picos_aux_htbl.t = + + # Picos_aux_htbl.try_add t 42 "The answer" + - : bool = true + + # Picos_aux_htbl.try_add t 101 "Basics" + - : bool = true + + # Picos_aux_htbl.find_exn t 42 + - : string = "The answer" + + # Picos_aux_htbl.try_add t 101 "The basics" + - : bool = false + + # Picos_aux_htbl.remove_all t |> List.of_seq + - : (int * string) list = [(101, "Basics"); (42, "The answer")] + ]} *) +end diff --git a/src_lockfree/htbl/htbl_unsafe.ml b/src_lockfree/htbl/htbl_unsafe.ml new file mode 100644 index 00000000..0ed91d60 --- /dev/null +++ b/src_lockfree/htbl/htbl_unsafe.ml @@ -0,0 +1,517 @@ +let[@inline never] impossible () = failwith "impossible" + +let ceil_pow_2_minus_1 n = + let n = Nativeint.of_int n in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 1) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 2) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 4) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 8) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 16) in + Nativeint.to_int + (if Sys.int_size > 32 then + Nativeint.logor n (Nativeint.shift_right_logical n 32) + else n) + +module Atomic = Multicore_magic.Transparent_atomic +module Atomic_array = Multicore_magic.Atomic_array + +type 'k hashed_type = (module Stdlib.Hashtbl.HashedType with type t = 'k) + +type ('k, 'v, _) tdt = + | Nil : ('k, 'v, [> `Nil ]) tdt + | Cons : { + key : 'k; + value : 'v; + rest : ('k, 'v, [ `Nil | `Cons ]) tdt; + } + -> ('k, 'v, [> `Cons ]) tdt + | Resize : { + spine : ('k, 'v, [ `Nil | `Cons ]) tdt; + } + -> ('k, 'v, [> `Resize ]) tdt + (** During resizing and snapshotting target buckets will be initialized + with a physically unique [Resize] value and the source buckets will + then be gradually updated to [Resize] values and the target buckets + updated with data from the source buckets. *) + +type ('k, 'v) bucket = + | B : ('k, 'v, [< `Nil | `Cons | `Resize ]) tdt -> ('k, 'v) bucket +[@@unboxed] + +type ('k, 'v) pending = + | Nothing + | Resize of { + buckets : ('k, 'v) bucket Atomic_array.t; + non_linearizable_size : int Atomic.t array; + } + +type ('k, 'v) state = { + hash : 'k -> int; + buckets : ('k, 'v) bucket Atomic_array.t; + equal : 'k -> 'k -> bool; + non_linearizable_size : int Atomic.t array; + pending : ('k, 'v) pending; + min_buckets : int; + max_buckets : int; +} +(** This record is [7 + 1] words and should be aligned on such a boundary on the + second generation heap. It is probably not worth it to pad it further. *) + +type ('k, 'v) t = ('k, 'v) state Atomic.t + +(* *) + +let lo_buckets = 1 lsl 3 + +and hi_buckets = + (* floor_pow_2 *) + let mask = ceil_pow_2_minus_1 Sys.max_array_length in + mask lxor (mask lsr 1) + +let min_buckets_default = 1 lsl 4 +and max_buckets_default = Int.min hi_buckets (1 lsl 30 (* Limit of [hash] *)) + +let create (type k) ?hashed_type ?min_buckets ?max_buckets () = + let min_buckets = + match min_buckets with + | None -> min_buckets_default + | Some n -> + let n = Int.max lo_buckets n |> Int.min hi_buckets in + ceil_pow_2_minus_1 (n - 1) + 1 + in + let max_buckets = + match max_buckets with + | None -> Int.max min_buckets max_buckets_default + | Some n -> + let n = Int.max min_buckets n |> Int.min hi_buckets in + ceil_pow_2_minus_1 (n - 1) + 1 + in + let equal, hash = + match hashed_type with + | None -> + (( = ), Stdlib.Hashtbl.seeded_hash (Int64.to_int (Random.bits64 ()))) + | Some ((module Hashed_type) : k hashed_type) -> + (Hashed_type.equal, Hashed_type.hash) + in + { + hash; + buckets = Atomic_array.make min_buckets (B Nil); + equal; + non_linearizable_size = + Array.init + (ceil_pow_2_minus_1 + (Multicore_magic.instantaneous_domain_index () lor 1) + (* Calling [...index ()] helps to ensure [at_exit] processing does + not raise. This also potentially adjusts the counter width for + the number of domains. *)) + (fun _ -> Atomic.make_contended 0); + pending = Nothing; + min_buckets; + max_buckets; + } + |> Atomic.make_contended + +(* *) + +let hashed_type_of (type k) (t : (k, _) t) : k hashed_type = + let r = Atomic.get t in + (module struct + type t = k + + let hash = r.hash + and equal = r.equal + end) + +let min_buckets_of t = (Atomic.get t).min_buckets +let max_buckets_of t = (Atomic.get t).max_buckets + +(* *) + +let rec take_at backoff bs i = + match Atomic_array.unsafe_fenceless_get bs i with + | B ((Nil | Cons _) as spine) -> + if + Atomic_array.unsafe_compare_and_set bs i (B spine) + (B (Resize { spine })) + then spine + else take_at (Backoff.once backoff) bs i + | B (Resize spine_r) -> spine_r.spine + +let rec copy_all r target i t step = + let i = (i + step) land (Atomic_array.length target - 1) in + let spine = take_at Backoff.default r.buckets i in + let (B before) = Atomic_array.unsafe_fenceless_get target i in + (* The [before] value is physically different for each resize and so checking + that the resize has not finished is sufficient to ensure that the + [compare_and_set] below does not disrupt the next resize. *) + Atomic.get t == r + && begin + begin + match before with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target i (B before) (B spine) + |> ignore + | Nil | Cons _ -> () + end; + i = 0 || copy_all r target i t step + end + +(* *) + +let[@tail_mod_cons] rec filter t msk chk = function + | Nil -> Nil + | Cons r -> + if t r.key land msk = chk then + Cons { r with rest = filter t msk chk r.rest } + else filter t msk chk r.rest + +let rec split_all r target i t step = + let i = (i + step) land (Atomic_array.length r.buckets - 1) in + let spine = take_at Backoff.default r.buckets i in + let high = Atomic_array.length r.buckets in + let after_lo = filter r.hash high 0 spine in + let after_hi = filter r.hash high high spine in + let (B before_lo) = Atomic_array.unsafe_fenceless_get target i in + let (B before_hi) = Atomic_array.unsafe_fenceless_get target (i + high) in + (* The [before_lo] and [before_hi] values are physically different for each + resize and so checking that the resize has not finished is sufficient to + ensure that the [compare_and_set] below does not disrupt the next + resize. *) + Atomic.get t == r + && begin + begin + match before_lo with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target i (B before_lo) + (B after_lo) + |> ignore + | Nil | Cons _ -> () + end; + begin + match before_hi with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target (i + high) (B before_hi) + (B after_hi) + |> ignore + | Nil | Cons _ -> () + end; + i = 0 || split_all r target i t step + end + +(* *) + +let[@tail_mod_cons] rec merge rest = function + | Nil -> rest + | Cons r -> Cons { r with rest = merge rest r.rest } + +let rec merge_all r target i t step = + let i = (i + step) land (Atomic_array.length target - 1) in + let spine_lo = take_at Backoff.default r.buckets i in + let spine_hi = + take_at Backoff.default r.buckets (i + Atomic_array.length target) + in + let ((Nil | Cons _) as after) = merge spine_lo spine_hi in + let (B before) = Atomic_array.unsafe_fenceless_get target i in + (* The [before] value is physically different for each resize and so checking + that the resize has not finished is sufficient to ensure that the + [compare_and_set] below does not disrupt the next resize. *) + Atomic.get t == r + && begin + begin + match before with + | Resize _ -> + Atomic_array.unsafe_compare_and_set target i (B before) (B after) + |> ignore + | Nil | Cons _ -> () + end; + i = 0 || merge_all r target i t step + end + +(* *) + +let[@inline never] rec finish t r = + match r.pending with + | Nothing -> r + | Resize { buckets; non_linearizable_size } -> + let high_source = Atomic_array.length r.buckets in + let high_target = Atomic_array.length buckets in + (* We step by random amount to better allow cores to work in parallel. + The number of buckets is always a power of two, so any odd number is + relatively prime or coprime. *) + let step = Int64.to_int (Random.bits64 ()) lor 1 in + if + if high_source < high_target then begin + (* We are growing the table. *) + split_all r buckets 0 t step + end + else if high_target < high_source then begin + (* We are shrinking the table. *) + merge_all r buckets 0 t step + end + else begin + (* We are snaphotting the table. *) + copy_all r buckets 0 t step + end + then + let new_r = + { r with buckets; non_linearizable_size; pending = Nothing } + in + if Atomic.compare_and_set t r new_r then new_r + else finish t (Atomic.get t) + else finish t (Atomic.get t) + +(* *) + +let rec estimated_size cs n sum = + let n = n - 1 in + if 0 <= n then estimated_size cs n (sum + Atomic.get (Array.unsafe_get cs n)) + else sum + +(** This only gives an "estimate" of the size, which can be off by one or more + and even be negative, so this must be used with care. *) +let estimated_size r = + let cs = r.non_linearizable_size in + let n = Array.length cs - 1 in + estimated_size cs n (Atomic.get (Array.unsafe_get cs n)) + +(** This must be called with [r.pending == Nothing]. *) +let[@inline never] try_resize t r new_capacity ~clear = + (* We must make sure that on every resize we use a physically different + [Resize _] value to indicate unprocessed target buckets. The use of + [Sys.opaque_identity] below ensures that a new value is allocated. *) + let resize_avoid_aba = + if clear then B Nil else B (Resize { spine = Sys.opaque_identity Nil }) + in + let buckets = Atomic_array.make new_capacity resize_avoid_aba in + let non_linearizable_size = + if clear then + Array.init (Array.length r.non_linearizable_size) @@ fun _ -> + Atomic.make_contended 0 + else r.non_linearizable_size + in + let new_r = { r with pending = Resize { buckets; non_linearizable_size } } in + Atomic.compare_and_set t r new_r + && begin + finish t new_r |> ignore; + true + end + +let rec adjust_estimated_size t r mask delta result = + let i = Multicore_magic.instantaneous_domain_index () in + let n = Array.length r.non_linearizable_size in + if i < n then begin + Atomic.fetch_and_add (Array.unsafe_get r.non_linearizable_size i) delta + |> ignore; + (* Reading the size is potentially expensive, so we only check it + occasionally. The bigger the table the less frequently we should need to + resize. *) + if + r.pending == Nothing + && Int64.to_int (Random.bits64 ()) land mask = 0 + && Atomic.get t == r + then begin + let estimated_size = estimated_size r in + let capacity = Atomic_array.length r.buckets in + if capacity < estimated_size && capacity < r.max_buckets then + try_resize t r (capacity + capacity) ~clear:false |> ignore + else if + r.min_buckets < capacity + && estimated_size + estimated_size + estimated_size < capacity + then try_resize t r (capacity lsr 1) ~clear:false |> ignore + end; + result + end + else + let new_cs = + (* We use [n + n + 1] as it keeps the length of the array as a power of 2 + minus 1 and so the size of the array/block including header word will + be a power of 2. *) + Array.init (n + n + 1) @@ fun i -> + if i < n then Array.unsafe_get r.non_linearizable_size i + else Atomic.make_contended 0 + in + let new_r = { r with non_linearizable_size = new_cs } in + let r = if Atomic.compare_and_set t r new_r then new_r else Atomic.get t in + adjust_estimated_size t r mask delta result + +(* *) + +(** [get] only returns with a state where [pending = Nothing]. *) +let[@inline] get t = + let r = Atomic.get t in + if r.pending == Nothing then r else finish t r + +(* *) + +let rec assoc_node t key = function + | Nil -> (Nil : (_, _, [< `Nil | `Cons ]) tdt) + | Cons r as cons -> if t r.key key then cons else assoc_node t key r.rest + +let find_node t key = + (* Reads can proceed in parallel with writes. *) + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + match Atomic_array.unsafe_fenceless_get r.buckets i with + | B Nil -> Nil + | B (Cons cons_r as cons) -> + if r.equal cons_r.key key then cons + else assoc_node r.equal key cons_r.rest + | B (Resize resize_r) -> + (* A resize is in progress. The spine of the resize still holds what was + in the bucket before resize reached that bucket. *) + assoc_node r.equal key resize_r.spine + +(* *) + +let find_exn t key = + match find_node t key with + | Nil -> raise_notrace Not_found + | Cons r -> r.value + +let mem t key = find_node t key != Nil + +(* *) + +let rec try_add t key value backoff = + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + match Atomic_array.unsafe_fenceless_get r.buckets i with + | B Nil -> + let after = Cons { key; value; rest = Nil } in + if Atomic_array.unsafe_compare_and_set r.buckets i (B Nil) (B after) then + adjust_estimated_size t r mask 1 true + else try_add t key value (Backoff.once backoff) + | B (Cons _ as before) -> + if assoc_node r.equal key before != Nil then false + else + let after = Cons { key; value; rest = before } in + if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) + then adjust_estimated_size t r mask 1 true + else try_add t key value (Backoff.once backoff) + | B (Resize _) -> + let _ = finish t (Atomic.get t) in + try_add t key value Backoff.default + +let[@inline] try_add t key value = try_add t key value Backoff.default + +(* *) + +let[@tail_mod_cons] rec dissoc t key = function + | Nil -> raise_notrace Not_found + | Cons r -> + if t key r.key then r.rest else Cons { r with rest = dissoc t key r.rest } + +let rec remove_node t key backoff = + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + match Atomic_array.unsafe_fenceless_get r.buckets i with + | B Nil -> Nil + | B (Cons cons_r as before) -> begin + if r.equal cons_r.key key then + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B cons_r.rest) + then adjust_estimated_size t r mask (-1) before + else remove_node t key (Backoff.once backoff) + else + match dissoc r.equal key cons_r.rest with + | (Nil | Cons _) as rest -> + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B (Cons { cons_r with rest })) + then + assoc_node r.equal key cons_r.rest + |> adjust_estimated_size t r mask (-1) + else remove_node t key (Backoff.once backoff) + | exception Not_found -> Nil + end + | B (Resize _) -> + let _ = finish t (Atomic.get t) in + remove_node t key Backoff.default + +let try_remove t key = remove_node t key Backoff.default != Nil + +let remove_exn t key = + match remove_node t key Backoff.default with + | Nil -> raise_notrace Not_found + | Cons r -> r.value + +(* *) + +let rec snapshot t ~clear backoff = + let r = get t in + if try_resize t r (Atomic_array.length r.buckets) ~clear then begin + (* At this point the resize has been completed and a new array is used for + buckets and [r.buckets] now has an immutable copy of what was in the hash + table. *) + let snapshot = r.buckets in + let rec loop i kvs () = + match kvs with + | Nil -> + if i = Atomic_array.length snapshot then Seq.Nil + else + loop (i + 1) + (match Atomic_array.unsafe_fenceless_get snapshot i with + | B (Resize spine_r) -> spine_r.spine + | B (Nil | Cons _) -> + (* After resize only [Resize] values should be left in the old + buckets. *) + assert false) + () + | Cons r -> Seq.Cons ((r.key, r.value), loop i r.rest) + in + loop 0 Nil + end + else snapshot t ~clear (Backoff.once backoff) + +let to_seq t = snapshot t ~clear:false Backoff.default +let remove_all t = snapshot t ~clear:true Backoff.default + +(* *) + +let rec try_find_random_non_empty_bucket buckets seed i = + match Atomic_array.unsafe_fenceless_get buckets i with + | B Nil | B (Resize { spine = Nil }) -> + let mask = Atomic_array.length buckets - 1 in + let i = (i + 1) land mask in + if i <> seed land mask then + try_find_random_non_empty_bucket buckets seed i + else Nil + | B (Cons cons_r) | B (Resize { spine = Cons cons_r }) -> Cons cons_r + +let try_find_random_non_empty_bucket t = + let buckets = (Atomic.get t).buckets in + let seed = Int64.to_int (Random.bits64 ()) in + try_find_random_non_empty_bucket buckets seed + (seed land (Atomic_array.length buckets - 1)) + +let rec length spine n = + match spine with Nil -> n | Cons r -> length r.rest (n + 1) + +let length spine = length spine 0 + +let rec nth spine i = + match spine with + | Nil -> impossible () + | Cons r -> if i <= 0 then r.key else nth r.rest (i - 1) + +let find_random_exn t = + match try_find_random_non_empty_bucket t with + | (Cons cons_r as spine : (_, _, [< `Nil | `Cons ]) tdt) -> + (* We found a non-empty bucket - the fast way. *) + if cons_r.rest == Nil then cons_r.key + else + let n = length spine in + nth spine (Random.int n) + | Nil -> + (* We couldn't find a non-empty bucket - the slow way. *) + let bindings = to_seq t |> Array.of_seq in + let n = Array.length bindings in + if n <> 0 then fst (Array.unsafe_get bindings (Random.int n)) + else raise_notrace Not_found diff --git a/src_lockfree/htbl/htbl_unsafe.mli b/src_lockfree/htbl/htbl_unsafe.mli new file mode 100644 index 00000000..ba768a89 --- /dev/null +++ b/src_lockfree/htbl/htbl_unsafe.mli @@ -0,0 +1 @@ +include Htbl_intf.HTBL diff --git a/src_lockfree/saturn_lockfree.ml b/src_lockfree/saturn_lockfree.ml index 904aaec1..3c1fd09c 100644 --- a/src_lockfree/saturn_lockfree.ml +++ b/src_lockfree/saturn_lockfree.ml @@ -36,3 +36,5 @@ module Single_consumer_queue = Mpsc_queue module Relaxed_queue = Mpmc_relaxed_queue module Size = Size module Skiplist = Skiplist +module Htbl = Htbl +module Htbl_unsafe = Htbl_unsafe diff --git a/src_lockfree/saturn_lockfree.mli b/src_lockfree/saturn_lockfree.mli index 145f7d98..214a92e9 100644 --- a/src_lockfree/saturn_lockfree.mli +++ b/src_lockfree/saturn_lockfree.mli @@ -40,3 +40,5 @@ module Single_consumer_queue = Mpsc_queue module Relaxed_queue = Mpmc_relaxed_queue module Skiplist = Skiplist module Size = Size +module Htbl = Htbl +module Htbl_unsafe = Htbl_unsafe diff --git a/test/htbl/dune b/test/htbl/dune new file mode 100644 index 00000000..2f2adf17 --- /dev/null +++ b/test/htbl/dune @@ -0,0 +1,48 @@ +(rule + (action + (copy + ../../src_lockfree/htbl/htbl.ml + htbl.ml)) + (package saturn_lockfree)) + +(rule + (action + (copy + ../../src_lockfree/htbl/htbl_unsafe.ml + htbl_unsafe.ml)) + (package saturn_lockfree)) + +(rule + (action + (copy + ../../src_lockfree/htbl/htbl_intf.ml + htbl_intf.ml)) + (package saturn_lockfree)) + +; (test +; (package saturn_lockfree) +; (name htbl_dscheck) +; (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) +; (build_if +; (and +; (>= %{ocaml_version} 5) +; (not +; (and +; (= %{arch_sixtyfour} false) +; (= %{architecture} arm))))) +; (modules +; htbl +; htbl_unsafe +; htbl_intf +; htbl_dscheck) +; (flags +; (:standard -open Multicore_magic_dscheck))) + + +(test + (package saturn_lockfree) + (name stm_htbl) + (modules stm_htbl) + (libraries htbls saturn_lockfree qcheck-core qcheck-stm.stm stm_run) + (enabled_if + (= %{arch_sixtyfour} true))) diff --git a/test/htbl/htbls/dune b/test/htbl/htbls/dune new file mode 100644 index 00000000..1dc61bc1 --- /dev/null +++ b/test/htbl/htbls/dune @@ -0,0 +1,10 @@ +(rule + (action + (copy + ../../../src_lockfree/htbl/htbl_intf.ml + htbl_intf.ml)) + (package saturn_lockfree)) + +(library + (name htbls) + (libraries saturn_lockfree)) diff --git a/test/htbl/htbls/htbls.ml b/test/htbl/htbls/htbls.ml new file mode 100644 index 00000000..1cb59e9e --- /dev/null +++ b/test/htbl/htbls/htbls.ml @@ -0,0 +1,17 @@ +module type Htbl_tests = sig + include Htbl_intf.HTBL + + val name : string +end + +module Htbl : Htbl_tests = struct + include Saturn_lockfree.Htbl + + let name = "htbl_safe" +end + +module Htbl_unsafe : Htbl_tests = struct + include Saturn_lockfree.Htbl_unsafe + + let name = "htbl_unsafe" +end diff --git a/test/htbl/stm_htbl.ml b/test/htbl/stm_htbl.ml new file mode 100644 index 00000000..19e7fefd --- /dev/null +++ b/test/htbl/stm_htbl.ml @@ -0,0 +1,96 @@ +open QCheck +open STM +module Htbl = Saturn_lockfree.Htbl + +let () = + (* Basics *) + Random.self_init (); + let t = Htbl.create () in + assert (Htbl.try_add t "Basics" 101); + assert (Htbl.try_add t "Answer" 42); + assert (101 = Htbl.remove_exn t "Basics"); + assert (not (Htbl.try_remove t "Basics")); + assert (Htbl.remove_all t |> List.of_seq = [ ("Answer", 42) ]); + assert (Htbl.to_seq t |> List.of_seq = []); + [ "One"; "Two"; "Three" ] + |> List.iteri (fun v k -> assert (Htbl.try_add t k v)); + assert ( + Htbl.to_seq t |> List.of_seq + |> List.sort (fun l r -> String.compare (fst l) (fst r)) + = [ ("One", 0); ("Three", 2); ("Two", 1) ]) + +module Int = struct + include Int + + let hash = Fun.id +end + +module Spec = struct + type cmd = + | Try_add of int + | Mem of int + | Try_remove of int + | To_keys + | Remove_all + + let show_cmd c = + match c with + | Try_add x -> "Try_add " ^ string_of_int x + | Mem x -> "Mem " ^ string_of_int x + | Try_remove x -> "Try_remove " ^ string_of_int x + | To_keys -> "To_keys" + | Remove_all -> "Remove_all" + + module State = Set.Make (Int) + + type state = State.t + type sut = (int, unit) Htbl.t + + let arb_cmd _s = + [ + Gen.int_bound 10 |> Gen.map (fun x -> Try_add x); + Gen.int_bound 10 |> Gen.map (fun x -> Mem x); + Gen.int_bound 10 |> Gen.map (fun x -> Try_remove x); + Gen.return To_keys; + Gen.return Remove_all; + ] + |> Gen.oneof |> make ~print:show_cmd + + let init_state = State.empty + let init_sut () = Htbl.create ~hashed_type:(module Int) () + let cleanup _ = () + + let next_state c s = + match c with + | Try_add x -> State.add x s + | Mem _ -> s + | Try_remove x -> State.remove x s + | 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 ()) + | Mem x -> + Res + ( bool, + match Htbl.find_exn d x with + | _ -> true + | exception Not_found -> false ) + | Try_remove x -> Res (bool, Htbl.try_remove d x) + | To_keys -> Res (seq int, Htbl.to_seq d |> Seq.map fst) + | Remove_all -> Res (seq int, Htbl.remove_all d |> Seq.map fst) + + let postcond c (s : state) res = + match (c, res) with + | Try_add x, Res ((Bool, _), res) -> res <> State.mem x s + | Mem x, Res ((Bool, _), res) -> res = State.mem x s + | Try_remove x, Res ((Bool, _), res) -> res = State.mem x s + | To_keys, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s + | Remove_all, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s + | _, _ -> false +end + +let () = Stm_run.run ~name:"Htbl" (module Spec) |> exit From 8ca0e635273e0379d160cef563bbcf6d1bf9378d Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 25 Sep 2024 12:07:51 +0200 Subject: [PATCH 02/16] Doc : picos -> saturn. --- src_lockfree/htbl/htbl_intf.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src_lockfree/htbl/htbl_intf.ml b/src_lockfree/htbl/htbl_intf.ml index af31dbfc..3a9548bf 100644 --- a/src_lockfree/htbl/htbl_intf.ml +++ b/src_lockfree/htbl/htbl_intf.ml @@ -101,24 +101,24 @@ module type HTBL = sig An example top-level session: {[ - # let t : (int, string) Picos_aux_htbl.t = - Picos_aux_htbl.create + # let t : (int, string) Saturn.Htbl.t = + Saturn.Htbl.create ~hashed_type:(module Int) () - val t : (int, string) Picos_aux_htbl.t = + val t : (int, string) Saturn.Htbl.t = - # Picos_aux_htbl.try_add t 42 "The answer" + # Saturn.Htbl.try_add t 42 "The answer" - : bool = true - # Picos_aux_htbl.try_add t 101 "Basics" + # Saturn.Htbl.try_add t 101 "Basics" - : bool = true - # Picos_aux_htbl.find_exn t 42 + # Saturn.Htbl.find_exn t 42 - : string = "The answer" - # Picos_aux_htbl.try_add t 101 "The basics" + # Saturn.Htbl.try_add t 101 "The basics" - : bool = false - # Picos_aux_htbl.remove_all t |> List.of_seq + # Saturn.Htbl.remove_all t |> List.of_seq - : (int * string) list = [(101, "Basics"); (42, "The answer")] ]} *) end From a0ee60dfb6bb31c5570bd8c5ed9fc9254790268a Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 25 Sep 2024 12:24:18 +0200 Subject: [PATCH 03/16] Stm tests launch for both htbl version. --- test/htbl/stm_htbl.ml | 167 ++++++++++++++++++++++-------------------- 1 file changed, 88 insertions(+), 79 deletions(-) diff --git a/test/htbl/stm_htbl.ml b/test/htbl/stm_htbl.ml index 19e7fefd..2f3fa85d 100644 --- a/test/htbl/stm_htbl.ml +++ b/test/htbl/stm_htbl.ml @@ -1,96 +1,105 @@ open QCheck open STM -module Htbl = Saturn_lockfree.Htbl -let () = - (* Basics *) - Random.self_init (); - let t = Htbl.create () in - assert (Htbl.try_add t "Basics" 101); - assert (Htbl.try_add t "Answer" 42); - assert (101 = Htbl.remove_exn t "Basics"); - assert (not (Htbl.try_remove t "Basics")); - assert (Htbl.remove_all t |> List.of_seq = [ ("Answer", 42) ]); - assert (Htbl.to_seq t |> List.of_seq = []); - [ "One"; "Two"; "Three" ] - |> List.iteri (fun v k -> assert (Htbl.try_add t k v)); - assert ( - Htbl.to_seq t |> List.of_seq - |> List.sort (fun l r -> String.compare (fst l) (fst r)) - = [ ("One", 0); ("Three", 2); ("Two", 1) ]) +module STM_htbl (Htbl : Htbls.Htbl_tests) = struct + let () = + (* Basics *) + Random.self_init (); + let t = Htbl.create () in + assert (Htbl.try_add t "Basics" 101); + assert (Htbl.try_add t "Answer" 42); + assert (101 = Htbl.remove_exn t "Basics"); + assert (not (Htbl.try_remove t "Basics")); + assert (Htbl.remove_all t |> List.of_seq = [ ("Answer", 42) ]); + assert (Htbl.to_seq t |> List.of_seq = []); + [ "One"; "Two"; "Three" ] + |> List.iteri (fun v k -> assert (Htbl.try_add t k v)); + assert ( + Htbl.to_seq t |> List.of_seq + |> List.sort (fun l r -> String.compare (fst l) (fst r)) + = [ ("One", 0); ("Three", 2); ("Two", 1) ]) -module Int = struct - include Int + module Int = struct + include Int - let hash = Fun.id -end + let hash = Fun.id + end -module Spec = struct - type cmd = - | Try_add of int - | Mem of int - | Try_remove of int - | To_keys - | Remove_all + module Spec = struct + type cmd = + | Try_add of int + | Mem of int + | Try_remove of int + | To_keys + | Remove_all - let show_cmd c = - match c with - | Try_add x -> "Try_add " ^ string_of_int x - | Mem x -> "Mem " ^ string_of_int x - | Try_remove x -> "Try_remove " ^ string_of_int x - | To_keys -> "To_keys" - | Remove_all -> "Remove_all" + let show_cmd c = + match c with + | Try_add x -> "Try_add " ^ string_of_int x + | Mem x -> "Mem " ^ string_of_int x + | Try_remove x -> "Try_remove " ^ string_of_int x + | To_keys -> "To_keys" + | Remove_all -> "Remove_all" - module State = Set.Make (Int) + module State = Set.Make (Int) - type state = State.t - type sut = (int, unit) Htbl.t + type state = State.t + type sut = (int, unit) Htbl.t - let arb_cmd _s = - [ - Gen.int_bound 10 |> Gen.map (fun x -> Try_add x); - Gen.int_bound 10 |> Gen.map (fun x -> Mem x); - Gen.int_bound 10 |> Gen.map (fun x -> Try_remove x); - Gen.return To_keys; - Gen.return Remove_all; - ] - |> Gen.oneof |> make ~print:show_cmd + let arb_cmd _s = + [ + Gen.int_bound 10 |> Gen.map (fun x -> Try_add x); + Gen.int_bound 10 |> Gen.map (fun x -> Mem x); + Gen.int_bound 10 |> Gen.map (fun x -> Try_remove x); + Gen.return To_keys; + Gen.return Remove_all; + ] + |> Gen.oneof |> make ~print:show_cmd - let init_state = State.empty - let init_sut () = Htbl.create ~hashed_type:(module Int) () - let cleanup _ = () + let init_state = State.empty + let init_sut () = Htbl.create ~hashed_type:(module Int) () + let cleanup _ = () - let next_state c s = - match c with - | Try_add x -> State.add x s - | Mem _ -> s - | Try_remove x -> State.remove x s - | To_keys -> s - | Remove_all -> State.empty + let next_state c s = + match c with + | Try_add x -> State.add x s + | Mem _ -> s + | Try_remove x -> State.remove x s + | To_keys -> s + | Remove_all -> State.empty - let precond _ _ = true + let precond _ _ = true - let run c d = - match c with - | Try_add x -> Res (bool, Htbl.try_add d x ()) - | Mem x -> - Res - ( bool, - match Htbl.find_exn d x with - | _ -> true - | exception Not_found -> false ) - | Try_remove x -> Res (bool, Htbl.try_remove d x) - | To_keys -> Res (seq int, Htbl.to_seq d |> Seq.map fst) - | Remove_all -> Res (seq int, Htbl.remove_all d |> Seq.map fst) + let run c d = + match c with + | Try_add x -> Res (bool, Htbl.try_add d x ()) + | Mem x -> + Res + ( bool, + match Htbl.find_exn d x with + | _ -> true + | exception Not_found -> false ) + | Try_remove x -> Res (bool, Htbl.try_remove d x) + | To_keys -> Res (seq int, Htbl.to_seq d |> Seq.map fst) + | Remove_all -> Res (seq int, Htbl.remove_all d |> Seq.map fst) - let postcond c (s : state) res = - match (c, res) with - | Try_add x, Res ((Bool, _), res) -> res <> State.mem x s - | Mem x, Res ((Bool, _), res) -> res = State.mem x s - | Try_remove x, Res ((Bool, _), res) -> res = State.mem x s - | To_keys, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s - | Remove_all, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s - | _, _ -> false + let postcond c (s : state) res = + match (c, res) with + | Try_add x, Res ((Bool, _), res) -> res <> State.mem x s + | Mem x, Res ((Bool, _), res) -> res = State.mem x s + | Try_remove x, Res ((Bool, _), res) -> res = State.mem x s + | To_keys, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s + | Remove_all, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s + | _, _ -> false + end + + let run () = Stm_run.run ~name:"Htbl" (module Spec) |> exit end -let () = Stm_run.run ~name:"Htbl" (module Spec) |> exit +let () = + let module Safe = STM_htbl (Htbls.Htbl) in + let exit_code = Safe.run () in + if exit_code <> 0 then exit exit_code + else + let module Unsafe = STM_htbl (Htbls.Htbl_unsafe) in + Unsafe.run () |> exit From ed62e3a3eb72a7b04731c293f946d32becbe0180 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 25 Sep 2024 12:07:31 +0200 Subject: [PATCH 04/16] Add dscheck tests. --- test/htbl/dscheck_htbl.ml | 204 ++++++++++++++++++++++++++++++++++++++ test/htbl/dune | 37 ++++--- 2 files changed, 222 insertions(+), 19 deletions(-) create mode 100644 test/htbl/dscheck_htbl.ml diff --git a/test/htbl/dscheck_htbl.ml b/test/htbl/dscheck_htbl.ml new file mode 100644 index 00000000..e5c5e0fd --- /dev/null +++ b/test/htbl/dscheck_htbl.ml @@ -0,0 +1,204 @@ +module Atomic = Dscheck.TracedAtomic + +module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct + open Htbl + + let try_add htbl k = try_add htbl k k + let create ?min_buckets () = create ?min_buckets ~hashed_type:(module Int) () + + let _two_mem () = + Atomic.trace ~record_traces:true (fun () -> + Random.init 0; + + let htbl = create () in + let added = List.init 10 (fun i -> try_add htbl i) in + let found1, found2, found3, found4 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + found1 := mem htbl 1; + found2 := mem htbl 20); + Atomic.spawn (fun () -> + found3 := mem htbl 1; + found4 := mem htbl 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + List.for_all (fun x -> x) added + && !found1 && (not !found2) && !found3 && !found4))); + + Dscheck.Trace_tracker.print_traces stdout + + let _two_add () = + (* Trying to trigger resize *) + let random_offset = Random.int 1000 in + for i = 0 to 4 do + Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> + Random.init (random_offset + i); + let htbl = create ~min_buckets:8 () in + for i = 0 to 6 do + try_add htbl i |> ignore + done; + let added1, added2, added3, added4 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + added1 := try_add htbl 1; + added2 := try_add htbl 21); + Atomic.spawn (fun () -> + added4 := try_add htbl 22; + added3 := try_add htbl 1); + + Atomic.final (fun () -> + Atomic.check (fun () -> + (not !added1) && !added2 && (not !added3) && !added4 + && mem htbl 1 && mem htbl 21 && mem htbl 22))); + Dscheck.Trace_tracker.print_traces stdout + done + + let _two_remove () = + let random_offset = Random.int 1000 in + (* for i = 0 to 4 do *) + Atomic.trace (fun () -> + Random.init (random_offset + 0); + let htbl = create ~min_buckets:8 () in + for i = 0 to 19 do + try_add htbl i |> ignore + done; + let removed = List.init 10 (fun i -> try_remove htbl i) in + let removed1, removed2, removed3, removed4 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + removed1 := try_remove htbl 11; + removed2 := try_remove htbl 9); + Atomic.spawn (fun () -> + removed3 := try_remove htbl 11; + removed4 := try_remove htbl 10); + + Atomic.final (fun () -> + Atomic.check (fun () -> + List.for_all (fun x -> x) removed + && (not !removed2) + && ((!removed1 && not !removed3) + || ((not !removed1) && !removed3)) + && !removed4 + && List.init 12 (fun i -> not (mem htbl i)) + |> List.for_all (fun x -> x)))) + (* done *) + + let _two_add_remove_same () = + let seed = Random.int 1000 in + + Atomic.trace (fun () -> + Random.init seed; + let htbl = create ~min_buckets:32 () in + let added1, added2, removed1, removed2 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + added1 := try_add htbl 1; + removed1 := try_remove htbl 1); + Atomic.spawn (fun () -> + added2 := try_add htbl 1; + removed2 := try_remove htbl 1); + + Atomic.final (fun () -> + Atomic.check (fun () -> + (!added1 || !added2) && (!removed1 || !removed2) + && not (mem htbl 1)))) + + let _two_add_remove_alt () = + let seed = Random.int 1000 in + + Atomic.trace (fun () -> + Random.init seed; + let htbl = create ~min_buckets:32 () in + let added1, added2, removed1, removed2 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + added1 := try_add htbl 1; + removed1 := try_remove htbl 1); + Atomic.spawn (fun () -> + added2 := try_add htbl 2; + removed2 := try_remove htbl 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + !added1 && !added2 && !removed1 && !removed2 + && (not (mem htbl 1)) + && not (mem htbl 2)))) + + let _two_add_remove_crossed () = + let seed = Random.int 1000 in + + Atomic.trace (fun () -> + Random.init seed; + let htbl = create ~min_buckets:32 () in + let added1, added2, removed1, removed2 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + added1 := try_add htbl 1; + removed2 := try_remove htbl 2); + Atomic.spawn (fun () -> + added2 := try_add htbl 2; + removed1 := try_remove htbl 1); + + Atomic.final (fun () -> + Atomic.check (fun () -> + let mem1 = mem htbl 1 in + let mem2 = mem htbl 2 in + !added1 && !added2 && !removed1 <> mem1 && !removed2 <> mem2))) + + let _two_add_remove_all () = + let seed = Random.int 1000 in + + Atomic.trace (fun () -> + Random.init seed; + let htbl : (int, int) Htbl.t = create ~min_buckets:32 () in + for i = 0 to 9 do + try_add htbl i |> ignore + done; + let added, removed = (ref false, ref []) in + + Atomic.spawn (fun () -> removed := remove_all htbl |> List.of_seq); + Atomic.spawn (fun () -> added := try_add htbl 10); + + Atomic.final (fun () -> + Atomic.check (fun () -> + List.sort compare !removed = List.init 10 (fun i -> (i, i)) + && not (mem htbl 10) + || List.sort compare !removed = List.init 9 (fun i -> (i, i)) + && mem htbl 10))) + + let tests name = + let open Alcotest in + [ + ( "basic_" ^ name, + [ + test_case "2-mem" `Slow _two_mem; + (* test_case "2-add" `Slow _two_add; *) + test_case "2-remove" `Slow _two_remove; + test_case "2-add-remove-same" `Slow _two_add_remove_same; + test_case "2-add-remove-alt" `Slow _two_add_remove_alt; + test_case "2-add-remove-crossed" `Slow _two_add_remove_crossed; + test_case "2-add-remove_all" `Slow _two_add_remove_crossed; + ] ); + ] +end + +let () = + let module Safe = Dscheck_htbl (Htbl) in + let safe_test = Safe.tests "safe" in + let module Unsafe = Dscheck_htbl (Htbl_unsafe) in + let unsafe_test = Unsafe.tests "unsafe" in + let open Alcotest in + run "DSCheck Hshtbl" (safe_test @ unsafe_test) diff --git a/test/htbl/dune b/test/htbl/dune index 2f2adf17..93278afa 100644 --- a/test/htbl/dune +++ b/test/htbl/dune @@ -19,25 +19,24 @@ htbl_intf.ml)) (package saturn_lockfree)) -; (test -; (package saturn_lockfree) -; (name htbl_dscheck) -; (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) -; (build_if -; (and -; (>= %{ocaml_version} 5) -; (not -; (and -; (= %{arch_sixtyfour} false) -; (= %{architecture} arm))))) -; (modules -; htbl -; htbl_unsafe -; htbl_intf -; htbl_dscheck) -; (flags -; (:standard -open Multicore_magic_dscheck))) - + (test + (package saturn_lockfree) + (name dscheck_htbl) + (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) + (build_if + (and + (>= %{ocaml_version} 5) + (not + (and + (= %{arch_sixtyfour} false) + (= %{architecture} arm))))) + (modules + htbl + htbl_unsafe + htbl_intf + dscheck_htbl) + (flags + (:standard -open Multicore_magic_dscheck))) (test (package saturn_lockfree) From 0b1ec15920dad642ec70762cb4b104c0e7db8ba0 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 26 Sep 2024 09:44:53 +0200 Subject: [PATCH 05/16] format --- test/htbl/dune | 44 +++++++++++++++++--------------------------- test/htbl/htbls/dune | 4 +--- 2 files changed, 18 insertions(+), 30 deletions(-) diff --git a/test/htbl/dune b/test/htbl/dune index 93278afa..994a4700 100644 --- a/test/htbl/dune +++ b/test/htbl/dune @@ -1,42 +1,32 @@ (rule (action - (copy - ../../src_lockfree/htbl/htbl.ml - htbl.ml)) + (copy ../../src_lockfree/htbl/htbl.ml htbl.ml)) (package saturn_lockfree)) (rule (action - (copy - ../../src_lockfree/htbl/htbl_unsafe.ml - htbl_unsafe.ml)) + (copy ../../src_lockfree/htbl/htbl_unsafe.ml htbl_unsafe.ml)) (package saturn_lockfree)) (rule (action - (copy - ../../src_lockfree/htbl/htbl_intf.ml - htbl_intf.ml)) + (copy ../../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) (package saturn_lockfree)) - (test - (package saturn_lockfree) - (name dscheck_htbl) - (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) - (build_if - (and - (>= %{ocaml_version} 5) - (not - (and - (= %{arch_sixtyfour} false) - (= %{architecture} arm))))) - (modules - htbl - htbl_unsafe - htbl_intf - dscheck_htbl) - (flags - (:standard -open Multicore_magic_dscheck))) +(test + (package saturn_lockfree) + (name dscheck_htbl) + (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) + (build_if + (and + (>= %{ocaml_version} 5) + (not + (and + (= %{arch_sixtyfour} false) + (= %{architecture} arm))))) + (modules htbl htbl_unsafe htbl_intf dscheck_htbl) + (flags + (:standard -open Multicore_magic_dscheck))) (test (package saturn_lockfree) diff --git a/test/htbl/htbls/dune b/test/htbl/htbls/dune index 1dc61bc1..3e1df282 100644 --- a/test/htbl/htbls/dune +++ b/test/htbl/htbls/dune @@ -1,8 +1,6 @@ (rule (action - (copy - ../../../src_lockfree/htbl/htbl_intf.ml - htbl_intf.ml)) + (copy ../../../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) (package saturn_lockfree)) (library From 7b3dc6f5cbe6d6337cc20ac1abd18226bbbb72d6 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 26 Sep 2024 15:42:19 +0200 Subject: [PATCH 06/16] Dscheck tests that trigger resize. --- src_lockfree/htbl/htbl.ml | 28 +--------- src_lockfree/htbl/htbl_unsafe.ml | 39 +++++-------- src_lockfree/htbl/htbl_utils.ml | 23 ++++++++ test/htbl/dscheck_htbl.ml | 95 ++++++++++++++++++++++++++------ test/htbl/dune | 2 +- test/htbl/htbl_utils.ml | 25 +++++++++ 6 files changed, 142 insertions(+), 70 deletions(-) create mode 100644 src_lockfree/htbl/htbl_utils.ml create mode 100644 test/htbl/htbl_utils.ml diff --git a/src_lockfree/htbl/htbl.ml b/src_lockfree/htbl/htbl.ml index f7aea678..5804ded2 100644 --- a/src_lockfree/htbl/htbl.ml +++ b/src_lockfree/htbl/htbl.ml @@ -11,20 +11,7 @@ LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) - -let[@inline never] impossible () = failwith "impossible" - -let ceil_pow_2_minus_1 n = - let n = Nativeint.of_int n in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 1) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 2) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 4) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 8) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 16) in - Nativeint.to_int - (if Sys.int_size > 32 then - Nativeint.logor n (Nativeint.shift_right_logical n 32) - else n) +open Htbl_utils module Atomic_array = struct type 'a t = 'a Atomic.t array @@ -84,18 +71,6 @@ type ('k, 'v) state = { type ('k, 'v) t = ('k, 'v) state Atomic.t -(* *) - -let lo_buckets = 1 lsl 3 - -and hi_buckets = - (* floor_pow_2 *) - let mask = ceil_pow_2_minus_1 Sys.max_array_length in - mask lxor (mask lsr 1) - -let min_buckets_default = 1 lsl 4 -and max_buckets_default = Int.min hi_buckets (1 lsl 30 (* Limit of [hash] *)) - let create (type k) ?hashed_type ?min_buckets ?max_buckets () = let min_buckets = match min_buckets with @@ -307,6 +282,7 @@ let[@inline never] try_resize t r new_capacity ~clear = let resize_avoid_aba = if clear then B Nil else B (Resize { spine = Sys.opaque_identity Nil }) in + Format.printf "new_capacity %d\n" new_capacity; let buckets = Atomic_array.make new_capacity resize_avoid_aba in let non_linearizable_size = if clear then diff --git a/src_lockfree/htbl/htbl_unsafe.ml b/src_lockfree/htbl/htbl_unsafe.ml index 0ed91d60..ad69e04a 100644 --- a/src_lockfree/htbl/htbl_unsafe.ml +++ b/src_lockfree/htbl/htbl_unsafe.ml @@ -1,17 +1,18 @@ -let[@inline never] impossible () = failwith "impossible" - -let ceil_pow_2_minus_1 n = - let n = Nativeint.of_int n in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 1) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 2) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 4) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 8) in - let n = Nativeint.logor n (Nativeint.shift_right_logical n 16) in - Nativeint.to_int - (if Sys.int_size > 32 then - Nativeint.logor n (Nativeint.shift_right_logical n 32) - else n) +(* Copyright (c) 2023 Vesa Karvonen + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. + + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH + REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY + AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, + INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM + LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR + OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR + PERFORMANCE OF THIS SOFTWARE. *) + +open Htbl_utils module Atomic = Multicore_magic.Transparent_atomic module Atomic_array = Multicore_magic.Atomic_array @@ -59,18 +60,6 @@ type ('k, 'v) state = { type ('k, 'v) t = ('k, 'v) state Atomic.t -(* *) - -let lo_buckets = 1 lsl 3 - -and hi_buckets = - (* floor_pow_2 *) - let mask = ceil_pow_2_minus_1 Sys.max_array_length in - mask lxor (mask lsr 1) - -let min_buckets_default = 1 lsl 4 -and max_buckets_default = Int.min hi_buckets (1 lsl 30 (* Limit of [hash] *)) - let create (type k) ?hashed_type ?min_buckets ?max_buckets () = let min_buckets = match min_buckets with diff --git a/src_lockfree/htbl/htbl_utils.ml b/src_lockfree/htbl/htbl_utils.ml new file mode 100644 index 00000000..9186f1cf --- /dev/null +++ b/src_lockfree/htbl/htbl_utils.ml @@ -0,0 +1,23 @@ +let[@inline never] impossible () = failwith "impossible" + +let ceil_pow_2_minus_1 n = + let n = Nativeint.of_int n in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 1) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 2) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 4) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 8) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 16) in + Nativeint.to_int + (if Sys.int_size > 32 then + Nativeint.logor n (Nativeint.shift_right_logical n 32) + else n) + +let lo_buckets = 1 lsl 3 + +and hi_buckets = + (* floor_pow_2 *) + let mask = ceil_pow_2_minus_1 Sys.max_array_length in + mask lxor (mask lsr 1) + +let min_buckets_default = 1 lsl 4 +and max_buckets_default = Int.min hi_buckets (1 lsl 30 (* Limit of [hash] *)) diff --git a/test/htbl/dscheck_htbl.ml b/test/htbl/dscheck_htbl.ml index e5c5e0fd..1ed76cc7 100644 --- a/test/htbl/dscheck_htbl.ml +++ b/test/htbl/dscheck_htbl.ml @@ -31,30 +31,86 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct Dscheck.Trace_tracker.print_traces stdout let _two_add () = + Atomic.trace (fun () -> + Random.init 0; + let htbl = create ~min_buckets:8 () in + try_add htbl 1 |> ignore; + let added1, added2, added3, added4 = + (ref false, ref false, ref false, ref false) + in + + Atomic.spawn (fun () -> + added1 := try_add htbl 1; + added2 := try_add htbl 21); + Atomic.spawn (fun () -> + added4 := try_add htbl 22; + added3 := try_add htbl 1); + + Atomic.final (fun () -> + Atomic.check (fun () -> + (not !added1) && !added2 && (not !added3) && !added4 + && mem htbl 1 && mem htbl 21 && mem htbl 22))) + + let _two_add_resize () = (* Trying to trigger resize *) let random_offset = Random.int 1000 in - for i = 0 to 4 do + for i = 0 to 5 do Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> Random.init (random_offset + i); - let htbl = create ~min_buckets:8 () in - for i = 0 to 6 do - try_add htbl i |> ignore - done; - let added1, added2, added3, added4 = - (ref false, ref false, ref false, ref false) - in - - Atomic.spawn (fun () -> - added1 := try_add htbl 1; - added2 := try_add htbl 21); - Atomic.spawn (fun () -> - added4 := try_add htbl 22; - added3 := try_add htbl 1); + let htbl = create ~min_buckets:2 () in + try_add htbl 1 |> ignore; + try_add htbl 2 |> ignore; + + let added1, added2 = (ref false, ref false) in + + Atomic.spawn (fun () -> added1 := try_add htbl 21); + Atomic.spawn (fun () -> added2 := try_add htbl 22); + + Atomic.final (fun () -> + Atomic.check (fun () -> + !added1 && !added2 && mem htbl 21 && mem htbl 22))); + Dscheck.Trace_tracker.print_traces stdout + done + + let _two_add_resize2 () = + (* Trying to trigger resize *) + let random_offset = Random.int 1000 in + for i = 0 to 5 do + Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> + Random.init (random_offset + i); + let htbl = create ~min_buckets:2 () in + try_add htbl 1 |> ignore; + try_add htbl 2 |> ignore; + + let added1, added2 = (ref false, ref false) in + + Atomic.spawn (fun () -> added1 := try_add htbl 1); + Atomic.spawn (fun () -> added2 := try_add htbl 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + (not !added1) && (not !added2) && mem htbl 1 && mem htbl 2))); + Dscheck.Trace_tracker.print_traces stdout + done + + let _two_add_resize3 () = + (* Trying to trigger resize *) + let random_offset = Random.int 1000 in + for i = 0 to 5 do + Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> + Random.init (random_offset + i); + let htbl = create ~min_buckets:2 () in + try_add htbl 1 |> ignore; + try_add htbl 2 |> ignore; + + let added1, added2 = (ref false, ref false) in + + Atomic.spawn (fun () -> added1 := try_add htbl 1); + Atomic.spawn (fun () -> added2 := try_add htbl 22); Atomic.final (fun () -> Atomic.check (fun () -> - (not !added1) && !added2 && (not !added3) && !added4 - && mem htbl 1 && mem htbl 21 && mem htbl 22))); + (not !added1) && !added2 && mem htbl 1 && mem htbl 22))); Dscheck.Trace_tracker.print_traces stdout done @@ -185,7 +241,10 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct ( "basic_" ^ name, [ test_case "2-mem" `Slow _two_mem; - (* test_case "2-add" `Slow _two_add; *) + test_case "2-add" `Slow _two_add; + test_case "2-add-resize" `Slow _two_add_resize; + test_case "2-add-resize2" `Slow _two_add_resize2; + test_case "2-add-resize3" `Slow _two_add_resize3; test_case "2-remove" `Slow _two_remove; test_case "2-add-remove-same" `Slow _two_add_remove_same; test_case "2-add-remove-alt" `Slow _two_add_remove_alt; diff --git a/test/htbl/dune b/test/htbl/dune index 994a4700..3155fe35 100644 --- a/test/htbl/dune +++ b/test/htbl/dune @@ -24,7 +24,7 @@ (and (= %{arch_sixtyfour} false) (= %{architecture} arm))))) - (modules htbl htbl_unsafe htbl_intf dscheck_htbl) + (modules htbl htbl_unsafe htbl_intf htbl_utils dscheck_htbl) (flags (:standard -open Multicore_magic_dscheck))) diff --git a/test/htbl/htbl_utils.ml b/test/htbl/htbl_utils.ml new file mode 100644 index 00000000..b6b5e7a0 --- /dev/null +++ b/test/htbl/htbl_utils.ml @@ -0,0 +1,25 @@ +(* This file enables to define a lower low_buckets value for dscheck testing *) + +let[@inline never] impossible () = failwith "impossible" + +let ceil_pow_2_minus_1 n = + let n = Nativeint.of_int n in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 1) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 2) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 4) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 8) in + let n = Nativeint.logor n (Nativeint.shift_right_logical n 16) in + Nativeint.to_int + (if Sys.int_size > 32 then + Nativeint.logor n (Nativeint.shift_right_logical n 32) + else n) + +let lo_buckets = 1 lsl 1 + +and hi_buckets = + (* floor_pow_2 *) + let mask = ceil_pow_2_minus_1 Sys.max_array_length in + mask lxor (mask lsr 1) + +let min_buckets_default = 1 lsl 4 +and max_buckets_default = Int.min hi_buckets (1 lsl 30 (* Limit of [hash] *)) From 3d8d0e28fc645fea028336f72786fa0635a695db Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Fri, 27 Sep 2024 16:41:23 +0200 Subject: [PATCH 07/16] Random.bits64 requires ocaml >= 4.14 --- dune-project | 4 ++-- saturn.opam | 2 +- saturn_lockfree.opam | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dune-project b/dune-project index 02e3c7b7..253348b6 100644 --- a/dune-project +++ b/dune-project @@ -12,7 +12,7 @@ (name saturn) (synopsis "Collection of parallelism-safe data structures for Multicore OCaml") (depends - (ocaml (>= 4.13)) + (ocaml (>= 4.14)) (domain_shims (and (>= 0.1.0) :with-test)) (saturn_lockfree (= :version)) (multicore-magic (and (>= 2.3.0) :with-test)) @@ -32,7 +32,7 @@ (name saturn_lockfree) (synopsis "Collection of lock-free data structures for Multicore OCaml") (depends - (ocaml (>= 4.13)) + (ocaml (>= 4.14)) (domain_shims (and (>= 0.1.0) :with-test)) (backoff (>= 0.1.0)) (multicore-magic (>= 2.3.0)) diff --git a/saturn.opam b/saturn.opam index 376fa2cc..dcece74c 100644 --- a/saturn.opam +++ b/saturn.opam @@ -10,7 +10,7 @@ doc: "https://ocaml-multicore.github.io/saturn/" bug-reports: "https://github.com/ocaml-multicore/saturn/issues" depends: [ "dune" {>= "3.14"} - "ocaml" {>= "4.13"} + "ocaml" {>= "4.14"} "domain_shims" {>= "0.1.0" & with-test} "saturn_lockfree" {= version} "multicore-magic" {>= "2.3.0" & with-test} diff --git a/saturn_lockfree.opam b/saturn_lockfree.opam index 09bd35e1..d18f9116 100644 --- a/saturn_lockfree.opam +++ b/saturn_lockfree.opam @@ -9,7 +9,7 @@ doc: "https://ocaml-multicore.github.io/saturn/" bug-reports: "https://github.com/ocaml-multicore/saturn/issues" depends: [ "dune" {>= "3.14"} - "ocaml" {>= "4.13"} + "ocaml" {>= "4.14"} "domain_shims" {>= "0.1.0" & with-test} "backoff" {>= "0.1.0"} "multicore-magic" {>= "2.3.0"} From 798d87527f79059fe3a87ae7f1cfd63c96adc18f Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 2 Oct 2024 18:03:41 +0200 Subject: [PATCH 08/16] Add benchmarks. --- bench/bench_htbl.ml | 76 +++++++++++++++++++++++++++++++++++++++++++++ bench/dune | 5 +++ bench/main.ml | 1 + 3 files changed, 82 insertions(+) create mode 100644 bench/bench_htbl.ml diff --git a/bench/bench_htbl.ml b/bench/bench_htbl.ml new file mode 100644 index 00000000..e0da6ed7 --- /dev/null +++ b/bench/bench_htbl.ml @@ -0,0 +1,76 @@ +open Multicore_bench + +let run_one ~budgetf ~n_domains ?(n_ops = 20 * Util.iter_factor) + ?(n_keys = 10000) ~percent_mem ?(percent_add = (100 - percent_mem + 1) / 2) + ?(prepopulate = true) (module Htbl : Htbl_intf.HTBL) = + let percent_rem = 100 - (percent_mem + percent_add) in + + let limit_mem = percent_mem in + let limit_add = percent_mem + percent_add in + + assert (0 <= limit_mem && limit_mem <= 100); + assert (limit_mem <= limit_add && limit_add <= 100); + + let t = Htbl.create ~hashed_type:(module Int) () in + if prepopulate then + for _ = 1 to n_keys do + let value = Random.bits () in + let key = value mod n_keys in + Htbl.try_add t key value |> ignore + done; + + let n_ops = (100 + percent_mem) * n_ops / 100 in + let n_ops = n_ops * n_domains in + + let n_ops_todo = Atomic.make 0 |> Multicore_magic.copy_as_padded in + + let init _ = + Atomic.set n_ops_todo n_ops; + Random.State.make_self_init () + in + let work _ state = + let rec work () = + let n = Util.alloc n_ops_todo in + if n <> 0 then + let rec loop n = + if 0 < n then + let value = Random.State.bits state in + let op = (value asr 20) mod 100 in + let key = value mod n_keys in + if op < limit_mem then begin + Htbl.mem t key |> ignore; + loop (n - 1) + end + else if op < limit_add then begin + Htbl.try_add t key value |> ignore; + loop (n - 1) + end + else begin + Htbl.try_remove t key |> ignore; + loop (n - 1) + end + else work () + in + loop n + in + work () + in + + let config = + Printf.sprintf "%d workers, %d%% mem %d%% add %d%% rem" n_domains + percent_mem percent_add percent_rem + in + Times.record ~budgetf ~n_domains ~init ~work () + |> Times.to_thruput_metrics ~n:n_ops ~singular:"operation" ~config + +let run_suite ~budgetf = + let run (module Htbl : Htbl_intf.HTBL) = + Util.cross [ 10; 50; 90 ] [ 1; 2; 4 ] + |> List.concat_map @@ fun (percent_mem, n_domains) -> + run_one ~budgetf ~n_domains ~percent_mem (module Htbl) + in + List.fold_right2 + (fun safe unsafe acc -> safe :: unsafe :: acc) + (run (module Saturn_lockfree.Htbl)) + (run (module Saturn_lockfree.Htbl_unsafe)) + [] diff --git a/bench/dune b/bench/dune index e9d3db44..e1c46552 100644 --- a/bench/dune +++ b/bench/dune @@ -7,6 +7,11 @@ let () = Jbuild_plugin.V1.send @@ {| +(rule + (action + (copy ../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) + (package saturn_lockfree)) + (test (package saturn) (name main) diff --git a/bench/main.ml b/bench/main.ml index accc3fff..be50b92b 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -5,6 +5,7 @@ let benchmarks = ("Saturn_lockfree Single_prod_single_cons_queue", Bench_spsc_queue.run_suite); ("Saturn_lockfree Size", Bench_size.run_suite); ("Saturn_lockfree Skiplist", Bench_skiplist.run_suite); + ("Saturn_lockfree Htbl", Bench_htbl.run_suite); ("Saturn_lockfree Stack", Bench_stack.run_suite); ("Saturn_lockfree Work_stealing_deque", Bench_ws_deque.run_suite); ] From 5f0788dcd8d752971f9fc4360cee854006723618 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 3 Oct 2024 14:38:38 +0200 Subject: [PATCH 09/16] Compute htbl length with the Size module. --- src_lockfree/htbl/htbl.ml | 389 ++++++++++++++++++++----------- src_lockfree/htbl/htbl_intf.ml | 3 + src_lockfree/htbl/htbl_unsafe.ml | 388 +++++++++++++++++++----------- test/htbl/dune | 7 +- test/htbl/stm_htbl.ml | 6 + 5 files changed, 531 insertions(+), 262 deletions(-) diff --git a/src_lockfree/htbl/htbl.ml b/src_lockfree/htbl/htbl.ml index 5804ded2..698b1f7a 100644 --- a/src_lockfree/htbl/htbl.ml +++ b/src_lockfree/htbl/htbl.ml @@ -37,37 +37,47 @@ type ('k, 'v, _) tdt = rest : ('k, 'v, [ `Nil | `Cons ]) tdt; } -> ('k, 'v, [> `Cons ]) tdt + | Nil_with_size : { + mutable size_modifier : Size.once; + } + -> ('k, 'v, [> `Nil_with_size ]) tdt + | Cons_with_size : { + mutable size_modifier : Size.once; + key : 'k; + value : 'v; + rest : ('k, 'v, [ `Nil | `Cons ]) tdt; + } + -> ('k, 'v, [> `Cons_with_size ]) tdt | Resize : { - spine : ('k, 'v, [ `Nil | `Cons ]) tdt; + spine : ('k, 'v, [ `Nil_with_size | `Cons_with_size ]) tdt; } -> ('k, 'v, [> `Resize ]) tdt (** During resizing and snapshotting target buckets will be initialized - with a physically unique [Resize] value and the source buckets will - then be gradually updated to [Resize] values and the target buckets - updated with data from the source buckets. *) + with a physically unique [Resize] value and the source buckets will + then be gradually updated to [Resize] values and the target buckets + updated with data from the source buckets. *) type ('k, 'v) bucket = - | B : ('k, 'v, [< `Nil | `Cons | `Resize ]) tdt -> ('k, 'v) bucket + | B : + ('k, 'v, [< `Nil_with_size | `Cons_with_size | `Resize ]) tdt + -> ('k, 'v) bucket [@@unboxed] type ('k, 'v) pending = | Nothing - | Resize of { - buckets : ('k, 'v) bucket Atomic_array.t; - non_linearizable_size : int Atomic.t array; - } + | Resize of { buckets : ('k, 'v) bucket Atomic_array.t; size : Size.t } type ('k, 'v) state = { hash : 'k -> int; buckets : ('k, 'v) bucket Atomic_array.t; equal : 'k -> 'k -> bool; - non_linearizable_size : int Atomic.t array; + size : Size.t; pending : ('k, 'v) pending; min_buckets : int; max_buckets : int; } (** This record is [7 + 1] words and should be aligned on such a boundary on the - second generation heap. It is probably not worth it to pad it further. *) + second generation heap. It is probably not worth it to pad it further. *) type ('k, 'v) t = ('k, 'v) state Atomic.t @@ -95,16 +105,11 @@ let create (type k) ?hashed_type ?min_buckets ?max_buckets () = in { hash; - buckets = Atomic_array.make min_buckets (B Nil); + buckets = + Atomic_array.make min_buckets + (B (Nil_with_size { size_modifier = Size.used_once })); equal; - non_linearizable_size = - Array.init - (ceil_pow_2_minus_1 - (Multicore_magic.instantaneous_domain_index () lor 1) - (* Calling [...index ()] helps to ensure [at_exit] processing does - not raise. This also potentially adjusts the counter width for - the number of domains. *)) - (fun _ -> Atomic.make_contended 0); + size = Size.create (); pending = Nothing; min_buckets; max_buckets; @@ -127,19 +132,25 @@ let max_buckets_of t = (Atomic.get t).max_buckets (* *) -let rec take_at backoff bs i = +let rec take_at backoff size bs i = match Atomic_array.unsafe_fenceless_get bs i with - | B ((Nil | Cons _) as spine) -> + | B + ((Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) + as spine) -> begin + if size_modifier != Size.used_once then + Size.update_once size size_modifier; + if Atomic_array.unsafe_compare_and_set bs i (B spine) (B (Resize { spine })) then spine - else take_at (Backoff.once backoff) bs i + else take_at (Backoff.once backoff) size bs i + end | B (Resize spine_r) -> spine_r.spine let rec copy_all r target i t step = let i = (i + step) land (Atomic_array.length target - 1) in - let spine = take_at Backoff.default r.buckets i in + let spine = take_at Backoff.default r.size r.buckets i in let (B before) = Atomic_array.unsafe_fenceless_get target i in (* The [before] value is physically different for each resize and so checking that the resize has not finished is sufficient to ensure that the @@ -151,23 +162,46 @@ let rec copy_all r target i t step = | Resize _ -> Atomic_array.unsafe_compare_and_set target i (B before) (B spine) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; i = 0 || copy_all r target i t step end (* *) -let[@tail_mod_cons] rec filter t msk chk = function +let[@tail_mod_cons] rec filter_ t msk chk = function | Nil -> Nil | Cons r -> if t r.key land msk = chk then - Cons { r with rest = filter t msk chk r.rest } - else filter t msk chk r.rest + Cons { r with rest = filter_ t msk chk r.rest } + else filter_ t msk chk r.rest + +let[@tail_mod_cons] rec filter_fst t mask chk = function + | Nil -> Nil_with_size { size_modifier = Size.used_once } + | Cons r -> + if t r.key land mask = chk then + Cons_with_size + { + key = r.key; + value = r.value; + size_modifier = Size.used_once; + rest = filter_ t mask chk r.rest; + } + else filter_fst t mask chk r.rest + +let filter t mask chk : + ('a, 'b, [ `Cons_with_size | `Nil_with_size ]) tdt -> + ('a, 'b, [> `Cons_with_size | `Nil_with_size ]) tdt = function + | Nil_with_size s -> Nil_with_size s + | Cons_with_size r -> begin + if t r.key land mask = chk then + Cons_with_size { r with rest = filter_ t mask chk r.rest } + else filter_fst t mask chk r.rest + end let rec split_all r target i t step = let i = (i + step) land (Atomic_array.length r.buckets - 1) in - let spine = take_at Backoff.default r.buckets i in + let spine = take_at Backoff.default r.size r.buckets i in let high = Atomic_array.length r.buckets in let after_lo = filter r.hash high 0 spine in let after_hi = filter r.hash high high spine in @@ -185,7 +219,7 @@ let rec split_all r target i t step = Atomic_array.unsafe_compare_and_set target i (B before_lo) (B after_lo) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; begin match before_hi with @@ -193,7 +227,7 @@ let rec split_all r target i t step = Atomic_array.unsafe_compare_and_set target (i + high) (B before_hi) (B after_hi) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; i = 0 || split_all r target i t step end @@ -204,13 +238,41 @@ let[@tail_mod_cons] rec merge rest = function | Nil -> rest | Cons r -> Cons { r with rest = merge rest r.rest } +let merge size (rest : ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt) : + ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt -> + ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt = function + | Nil_with_size r -> + (* Each size_modifier that is going to be removed need to be applied *) + if r.size_modifier != Size.used_once then + Size.update_once size r.size_modifier; + rest + | Cons_with_size r -> begin + match rest with + | Nil_with_size r' -> + if r'.size_modifier != Size.used_once then + Size.update_once size r'.size_modifier; + Cons_with_size r + | Cons_with_size r' -> begin + if r'.size_modifier != Size.used_once then + Size.update_once size r'.size_modifier; + Cons_with_size + { + r with + rest = + merge + (Cons { key = r'.key; value = r'.value; rest = r'.rest }) + r.rest; + } + end + end + let rec merge_all r target i t step = let i = (i + step) land (Atomic_array.length target - 1) in - let spine_lo = take_at Backoff.default r.buckets i in + let spine_lo = take_at Backoff.default r.size r.buckets i in let spine_hi = - take_at Backoff.default r.buckets (i + Atomic_array.length target) + take_at Backoff.default r.size r.buckets (i + Atomic_array.length target) in - let ((Nil | Cons _) as after) = merge spine_lo spine_hi in + let after = merge r.size spine_lo spine_hi in let (B before) = Atomic_array.unsafe_fenceless_get target i in (* The [before] value is physically different for each resize and so checking that the resize has not finished is sufficient to ensure that the @@ -222,7 +284,7 @@ let rec merge_all r target i t step = | Resize _ -> Atomic_array.unsafe_compare_and_set target i (B before) (B after) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; i = 0 || merge_all r target i t step end @@ -232,7 +294,7 @@ let rec merge_all r target i t step = let[@inline never] rec finish t r = match r.pending with | Nothing -> r - | Resize { buckets; non_linearizable_size } -> + | Resize { buckets; size } -> let high_source = Atomic_array.length r.buckets in let high_target = Atomic_array.length buckets in (* We step by random amount to better allow cores to work in parallel. @@ -249,91 +311,64 @@ let[@inline never] rec finish t r = merge_all r buckets 0 t step end else begin - (* We are snaphotting the table. *) + (* We are snapshotting the table. *) copy_all r buckets 0 t step end then - let new_r = - { r with buckets; non_linearizable_size; pending = Nothing } - in + let new_r = { r with buckets; size; pending = Nothing } in if Atomic.compare_and_set t r new_r then new_r else finish t (Atomic.get t) else finish t (Atomic.get t) (* *) -let rec estimated_size cs n sum = - let n = n - 1 in - if 0 <= n then estimated_size cs n (sum + Atomic.get (Array.unsafe_get cs n)) - else sum - -(** This only gives an "estimate" of the size, which can be off by one or more - and even be negative, so this must be used with care. *) -let estimated_size r = - let cs = r.non_linearizable_size in - let n = Array.length cs - 1 in - estimated_size cs n (Atomic.get (Array.unsafe_get cs n)) - (** This must be called with [r.pending == Nothing]. *) let[@inline never] try_resize t r new_capacity ~clear = (* We must make sure that on every resize we use a physically different [Resize _] value to indicate unprocessed target buckets. The use of [Sys.opaque_identity] below ensures that a new value is allocated. *) let resize_avoid_aba = - if clear then B Nil else B (Resize { spine = Sys.opaque_identity Nil }) + if clear then B (Nil_with_size { size_modifier = Size.used_once }) + else + B + (Resize + { + spine = + Sys.opaque_identity + (Nil_with_size { size_modifier = Size.used_once }); + }) in - Format.printf "new_capacity %d\n" new_capacity; let buckets = Atomic_array.make new_capacity resize_avoid_aba in - let non_linearizable_size = - if clear then - Array.init (Array.length r.non_linearizable_size) @@ fun _ -> - Atomic.make_contended 0 - else r.non_linearizable_size + let new_r = + { + r with + pending = + Resize { buckets; size = (if clear then Size.create () else r.size) }; + } in - let new_r = { r with pending = Resize { buckets; non_linearizable_size } } in Atomic.compare_and_set t r new_r && begin finish t new_r |> ignore; true end -let rec adjust_estimated_size t r mask delta result = - let i = Multicore_magic.instantaneous_domain_index () in - let n = Array.length r.non_linearizable_size in - if i < n then begin - Atomic.fetch_and_add (Array.unsafe_get r.non_linearizable_size i) delta - |> ignore; +let adjust_size t r mask result = + if + r.pending == Nothing + && Int64.to_int (Random.bits64 ()) land mask = 0 + && Atomic.get t == r + then begin (* Reading the size is potentially expensive, so we only check it occasionally. The bigger the table the less frequently we should need to resize. *) - if - r.pending == Nothing - && Int64.to_int (Random.bits64 ()) land mask = 0 - && Atomic.get t == r - then begin - let estimated_size = estimated_size r in - let capacity = Atomic_array.length r.buckets in - if capacity < estimated_size && capacity < r.max_buckets then - try_resize t r (capacity + capacity) ~clear:false |> ignore - else if - r.min_buckets < capacity - && estimated_size + estimated_size + estimated_size < capacity - then try_resize t r (capacity lsr 1) ~clear:false |> ignore - end; - result - end - else - let new_cs = - (* We use [n + n + 1] as it keeps the length of the array as a power of 2 - minus 1 and so the size of the array/block including header word will - be a power of 2. *) - Array.init (n + n + 1) @@ fun i -> - if i < n then Array.unsafe_get r.non_linearizable_size i - else Atomic.make_contended 0 - in - let new_r = { r with non_linearizable_size = new_cs } in - let r = if Atomic.compare_and_set t r new_r then new_r else Atomic.get t in - adjust_estimated_size t r mask delta result + let size = Size.get r.size in + let capacity = Atomic_array.length r.buckets in + if capacity < size && capacity < r.max_buckets then + try_resize t r (capacity + capacity) ~clear:false |> ignore + else if r.min_buckets < capacity && size + size + size < capacity then + try_resize t r (capacity lsr 1) ~clear:false |> ignore + end; + result (* *) @@ -354,16 +389,24 @@ let find_node t key = let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - match Atomic_array.unsafe_fenceless_get r.buckets i with - | B Nil -> Nil - | B (Cons cons_r as cons) -> - if r.equal cons_r.key key then cons - else assoc_node r.equal key cons_r.rest - | B (Resize resize_r) -> - (* A resize is in progress. The spine of the resize still holds what was - in the bucket before resize reached that bucket. *) - assoc_node r.equal key resize_r.spine + let rec loop = function + | B (Nil_with_size nil_r) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once r.size nil_r.size_modifier; + Nil + | B (Cons_with_size cons_r) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + if r.equal cons_r.key key then + Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } + else assoc_node r.equal key cons_r.rest + | B (Resize resize_r) -> + (* A resize is in progress. The spine of the resize still holds what was + in the bucket before resize reached that bucket. *) + loop (B resize_r.spine) + in + loop @@ Atomic_array.unsafe_fenceless_get r.buckets i (* *) let find_exn t key = @@ -381,17 +424,47 @@ let rec try_add t key value backoff = let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in match Atomic_array.unsafe_fenceless_get r.buckets i with - | B Nil -> - let after = Cons { key; value; rest = Nil } in - if Atomic_array.unsafe_compare_and_set r.buckets i (B Nil) (B after) then - adjust_estimated_size t r mask 1 true + | B (Nil_with_size nil_r as before) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once r.size nil_r.size_modifier; + let (Cons_with_size cons_r as after : ('a, 'b, [ `Cons_with_size ]) tdt) = + Cons_with_size + { + size_modifier = Size.new_once r.size Size.incr; + key; + value; + rest = Nil; + } + in + if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + adjust_size t r mask true) else try_add t key value (Backoff.once backoff) - | B (Cons _ as before) -> - if assoc_node r.equal key before != Nil then false + | B (Cons_with_size cons_r as before) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + if r.equal cons_r.key key then false + else if assoc_node r.equal key cons_r.rest != Nil then false else - let after = Cons { key; value; rest = before } in + let (Cons_with_size cons_r as after) : ('a, 'b, [ `Cons_with_size ]) tdt + = + Cons_with_size + { + size_modifier = Size.(new_once r.size incr); + key; + value; + rest = + Cons + { key = cons_r.key; value = cons_r.value; rest = cons_r.rest }; + } + in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then adjust_estimated_size t r mask 1 true + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + adjust_size t r mask true) else try_add t key value (Backoff.once backoff) | B (Resize _) -> let _ = finish t (Atomic.get t) in @@ -412,23 +485,63 @@ let rec remove_node t key backoff = let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in match Atomic_array.unsafe_fenceless_get r.buckets i with - | B Nil -> Nil - | B (Cons cons_r as before) -> begin + | B (Nil_with_size nil_r) -> + if nil_r.size_modifier != Size.used_once then ( + Size.update_once r.size nil_r.size_modifier; + nil_r.size_modifier <- Size.used_once); + Nil + | B (Cons_with_size cons_r as before) -> begin + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + + let size_modifier = Size.new_once r.size Size.decr in if r.equal cons_r.key key then - if - Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B cons_r.rest) - then adjust_estimated_size t r mask (-1) before - else remove_node t key (Backoff.once backoff) + let found_node = + Cons { key = cons_r.key; value = cons_r.value; rest = Nil } + in + match cons_r.rest with + | Nil -> + let (Nil_with_size nil_r as after) : + ('a, 'b, [ `Nil_with_size ]) tdt = + Nil_with_size { size_modifier } + in + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B after) + then ( + Size.update_once r.size nil_r.size_modifier; + nil_r.size_modifier <- Size.used_once; + adjust_size t r mask found_node) + else remove_node t key (Backoff.once backoff) + | Cons next -> + let (Cons_with_size cons_r as after) : + ('a, 'b, [ `Cons_with_size ]) tdt = + Cons_with_size + { + size_modifier; + key = next.key; + value = next.value; + rest = next.rest; + } + in + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B after) + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + adjust_size t r mask found_node) + else remove_node t key (Backoff.once backoff) else match dissoc r.equal key cons_r.rest with | (Nil | Cons _) as rest -> if Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B (Cons { cons_r with rest })) - then - assoc_node r.equal key cons_r.rest - |> adjust_estimated_size t r mask (-1) + (B (Cons_with_size { cons_r with rest; size_modifier })) + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + assoc_node r.equal key cons_r.rest |> adjust_size t r mask) else remove_node t key (Backoff.once backoff) | exception Not_found -> Nil end @@ -459,8 +572,15 @@ let rec snapshot t ~clear backoff = else loop (i + 1) (match Atomic_array.unsafe_fenceless_get snapshot i with - | B (Resize spine_r) -> spine_r.spine - | B (Nil | Cons _) -> + | B (Resize { spine = Nil_with_size _ }) -> Nil + | B (Resize { spine = Cons_with_size cons_r }) -> + Cons + { + key = cons_r.key; + value = cons_r.value; + rest = cons_r.rest; + } + | B (Nil_with_size _ | Cons_with_size _) -> (* After resize only [Resize] values should be left in the old buckets. *) assert false) @@ -476,21 +596,26 @@ let remove_all t = snapshot t ~clear:true Backoff.default (* *) -let rec try_find_random_non_empty_bucket buckets seed i = +let rec try_find_random_non_empty_bucket size buckets seed i = match Atomic_array.unsafe_fenceless_get buckets i with - | B Nil | B (Resize { spine = Nil }) -> + | B (Nil_with_size nil_r) | B (Resize { spine = Nil_with_size nil_r }) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once size nil_r.size_modifier; let mask = Atomic_array.length buckets - 1 in let i = (i + 1) land mask in if i <> seed land mask then - try_find_random_non_empty_bucket buckets seed i + try_find_random_non_empty_bucket size buckets seed i else Nil - | B (Cons cons_r) | B (Resize { spine = Cons cons_r }) -> Cons cons_r + | B (Cons_with_size cons_r) | B (Resize { spine = Cons_with_size cons_r }) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once size cons_r.size_modifier; + Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } let try_find_random_non_empty_bucket t = - let buckets = (Atomic.get t).buckets in + let r = Atomic.get t in let seed = Int64.to_int (Random.bits64 ()) in - try_find_random_non_empty_bucket buckets seed - (seed land (Atomic_array.length buckets - 1)) + try_find_random_non_empty_bucket r.size r.buckets seed + (seed land (Atomic_array.length r.buckets - 1)) let rec length spine n = match spine with Nil -> n | Cons r -> length r.rest (n + 1) @@ -516,3 +641,5 @@ let find_random_exn t = let n = Array.length bindings in if n <> 0 then fst (Array.unsafe_get bindings (Random.int n)) else raise_notrace Not_found + +let length t = (Atomic.get t).size |> Size.get diff --git a/src_lockfree/htbl/htbl_intf.ml b/src_lockfree/htbl/htbl_intf.ml index 3a9548bf..9381c50f 100644 --- a/src_lockfree/htbl/htbl_intf.ml +++ b/src_lockfree/htbl/htbl_intf.ml @@ -48,6 +48,9 @@ module type HTBL = sig ℹī¸ The returned value may not be the same as given to {!create}. *) + val length : ('k, 'v) t -> int + (** [length htbl] returns the number of bindings in the hash table [htbl]. *) + (** {2 Looking up bindings} *) val find_exn : ('k, 'v) t -> 'k -> 'v diff --git a/src_lockfree/htbl/htbl_unsafe.ml b/src_lockfree/htbl/htbl_unsafe.ml index ad69e04a..495b54f3 100644 --- a/src_lockfree/htbl/htbl_unsafe.ml +++ b/src_lockfree/htbl/htbl_unsafe.ml @@ -26,37 +26,47 @@ type ('k, 'v, _) tdt = rest : ('k, 'v, [ `Nil | `Cons ]) tdt; } -> ('k, 'v, [> `Cons ]) tdt + | Nil_with_size : { + mutable size_modifier : Size.once; + } + -> ('k, 'v, [> `Nil_with_size ]) tdt + | Cons_with_size : { + mutable size_modifier : Size.once; + key : 'k; + value : 'v; + rest : ('k, 'v, [ `Nil | `Cons ]) tdt; + } + -> ('k, 'v, [> `Cons_with_size ]) tdt | Resize : { - spine : ('k, 'v, [ `Nil | `Cons ]) tdt; + spine : ('k, 'v, [ `Nil_with_size | `Cons_with_size ]) tdt; } -> ('k, 'v, [> `Resize ]) tdt (** During resizing and snapshotting target buckets will be initialized - with a physically unique [Resize] value and the source buckets will - then be gradually updated to [Resize] values and the target buckets - updated with data from the source buckets. *) + with a physically unique [Resize] value and the source buckets will + then be gradually updated to [Resize] values and the target buckets + updated with data from the source buckets. *) type ('k, 'v) bucket = - | B : ('k, 'v, [< `Nil | `Cons | `Resize ]) tdt -> ('k, 'v) bucket + | B : + ('k, 'v, [< `Nil_with_size | `Cons_with_size | `Resize ]) tdt + -> ('k, 'v) bucket [@@unboxed] type ('k, 'v) pending = | Nothing - | Resize of { - buckets : ('k, 'v) bucket Atomic_array.t; - non_linearizable_size : int Atomic.t array; - } + | Resize of { buckets : ('k, 'v) bucket Atomic_array.t; size : Size.t } type ('k, 'v) state = { hash : 'k -> int; buckets : ('k, 'v) bucket Atomic_array.t; equal : 'k -> 'k -> bool; - non_linearizable_size : int Atomic.t array; + size : Size.t; pending : ('k, 'v) pending; min_buckets : int; max_buckets : int; } (** This record is [7 + 1] words and should be aligned on such a boundary on the - second generation heap. It is probably not worth it to pad it further. *) + second generation heap. It is probably not worth it to pad it further. *) type ('k, 'v) t = ('k, 'v) state Atomic.t @@ -84,16 +94,11 @@ let create (type k) ?hashed_type ?min_buckets ?max_buckets () = in { hash; - buckets = Atomic_array.make min_buckets (B Nil); + buckets = + Atomic_array.make min_buckets + (B (Nil_with_size { size_modifier = Size.used_once })); equal; - non_linearizable_size = - Array.init - (ceil_pow_2_minus_1 - (Multicore_magic.instantaneous_domain_index () lor 1) - (* Calling [...index ()] helps to ensure [at_exit] processing does - not raise. This also potentially adjusts the counter width for - the number of domains. *)) - (fun _ -> Atomic.make_contended 0); + size = Size.create (); pending = Nothing; min_buckets; max_buckets; @@ -116,19 +121,25 @@ let max_buckets_of t = (Atomic.get t).max_buckets (* *) -let rec take_at backoff bs i = +let rec take_at backoff size bs i = match Atomic_array.unsafe_fenceless_get bs i with - | B ((Nil | Cons _) as spine) -> + | B + ((Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) + as spine) -> begin + if size_modifier != Size.used_once then + Size.update_once size size_modifier; + if Atomic_array.unsafe_compare_and_set bs i (B spine) (B (Resize { spine })) then spine - else take_at (Backoff.once backoff) bs i + else take_at (Backoff.once backoff) size bs i + end | B (Resize spine_r) -> spine_r.spine let rec copy_all r target i t step = let i = (i + step) land (Atomic_array.length target - 1) in - let spine = take_at Backoff.default r.buckets i in + let spine = take_at Backoff.default r.size r.buckets i in let (B before) = Atomic_array.unsafe_fenceless_get target i in (* The [before] value is physically different for each resize and so checking that the resize has not finished is sufficient to ensure that the @@ -140,23 +151,46 @@ let rec copy_all r target i t step = | Resize _ -> Atomic_array.unsafe_compare_and_set target i (B before) (B spine) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; i = 0 || copy_all r target i t step end (* *) -let[@tail_mod_cons] rec filter t msk chk = function +let[@tail_mod_cons] rec filter_ t msk chk = function | Nil -> Nil | Cons r -> if t r.key land msk = chk then - Cons { r with rest = filter t msk chk r.rest } - else filter t msk chk r.rest + Cons { r with rest = filter_ t msk chk r.rest } + else filter_ t msk chk r.rest + +let[@tail_mod_cons] rec filter_fst t mask chk = function + | Nil -> Nil_with_size { size_modifier = Size.used_once } + | Cons r -> + if t r.key land mask = chk then + Cons_with_size + { + key = r.key; + value = r.value; + size_modifier = Size.used_once; + rest = filter_ t mask chk r.rest; + } + else filter_fst t mask chk r.rest + +let filter t mask chk : + ('a, 'b, [ `Cons_with_size | `Nil_with_size ]) tdt -> + ('a, 'b, [> `Cons_with_size | `Nil_with_size ]) tdt = function + | Nil_with_size s -> Nil_with_size s + | Cons_with_size r -> begin + if t r.key land mask = chk then + Cons_with_size { r with rest = filter_ t mask chk r.rest } + else filter_fst t mask chk r.rest + end let rec split_all r target i t step = let i = (i + step) land (Atomic_array.length r.buckets - 1) in - let spine = take_at Backoff.default r.buckets i in + let spine = take_at Backoff.default r.size r.buckets i in let high = Atomic_array.length r.buckets in let after_lo = filter r.hash high 0 spine in let after_hi = filter r.hash high high spine in @@ -174,7 +208,7 @@ let rec split_all r target i t step = Atomic_array.unsafe_compare_and_set target i (B before_lo) (B after_lo) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; begin match before_hi with @@ -182,7 +216,7 @@ let rec split_all r target i t step = Atomic_array.unsafe_compare_and_set target (i + high) (B before_hi) (B after_hi) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; i = 0 || split_all r target i t step end @@ -193,13 +227,41 @@ let[@tail_mod_cons] rec merge rest = function | Nil -> rest | Cons r -> Cons { r with rest = merge rest r.rest } +let merge size (rest : ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt) : + ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt -> + ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt = function + | Nil_with_size r -> + (* Each size_modifier that is going to be removed need to be applied *) + if r.size_modifier != Size.used_once then + Size.update_once size r.size_modifier; + rest + | Cons_with_size r -> begin + match rest with + | Nil_with_size r' -> + if r'.size_modifier != Size.used_once then + Size.update_once size r'.size_modifier; + Cons_with_size r + | Cons_with_size r' -> begin + if r'.size_modifier != Size.used_once then + Size.update_once size r'.size_modifier; + Cons_with_size + { + r with + rest = + merge + (Cons { key = r'.key; value = r'.value; rest = r'.rest }) + r.rest; + } + end + end + let rec merge_all r target i t step = let i = (i + step) land (Atomic_array.length target - 1) in - let spine_lo = take_at Backoff.default r.buckets i in + let spine_lo = take_at Backoff.default r.size r.buckets i in let spine_hi = - take_at Backoff.default r.buckets (i + Atomic_array.length target) + take_at Backoff.default r.size r.buckets (i + Atomic_array.length target) in - let ((Nil | Cons _) as after) = merge spine_lo spine_hi in + let after = merge r.size spine_lo spine_hi in let (B before) = Atomic_array.unsafe_fenceless_get target i in (* The [before] value is physically different for each resize and so checking that the resize has not finished is sufficient to ensure that the @@ -211,7 +273,7 @@ let rec merge_all r target i t step = | Resize _ -> Atomic_array.unsafe_compare_and_set target i (B before) (B after) |> ignore - | Nil | Cons _ -> () + | Nil_with_size _ | Cons_with_size _ -> () end; i = 0 || merge_all r target i t step end @@ -221,7 +283,7 @@ let rec merge_all r target i t step = let[@inline never] rec finish t r = match r.pending with | Nothing -> r - | Resize { buckets; non_linearizable_size } -> + | Resize { buckets; size } -> let high_source = Atomic_array.length r.buckets in let high_target = Atomic_array.length buckets in (* We step by random amount to better allow cores to work in parallel. @@ -238,90 +300,64 @@ let[@inline never] rec finish t r = merge_all r buckets 0 t step end else begin - (* We are snaphotting the table. *) + (* We are snapshotting the table. *) copy_all r buckets 0 t step end then - let new_r = - { r with buckets; non_linearizable_size; pending = Nothing } - in + let new_r = { r with buckets; size; pending = Nothing } in if Atomic.compare_and_set t r new_r then new_r else finish t (Atomic.get t) else finish t (Atomic.get t) (* *) -let rec estimated_size cs n sum = - let n = n - 1 in - if 0 <= n then estimated_size cs n (sum + Atomic.get (Array.unsafe_get cs n)) - else sum - -(** This only gives an "estimate" of the size, which can be off by one or more - and even be negative, so this must be used with care. *) -let estimated_size r = - let cs = r.non_linearizable_size in - let n = Array.length cs - 1 in - estimated_size cs n (Atomic.get (Array.unsafe_get cs n)) - (** This must be called with [r.pending == Nothing]. *) let[@inline never] try_resize t r new_capacity ~clear = (* We must make sure that on every resize we use a physically different [Resize _] value to indicate unprocessed target buckets. The use of [Sys.opaque_identity] below ensures that a new value is allocated. *) let resize_avoid_aba = - if clear then B Nil else B (Resize { spine = Sys.opaque_identity Nil }) + if clear then B (Nil_with_size { size_modifier = Size.used_once }) + else + B + (Resize + { + spine = + Sys.opaque_identity + (Nil_with_size { size_modifier = Size.used_once }); + }) in let buckets = Atomic_array.make new_capacity resize_avoid_aba in - let non_linearizable_size = - if clear then - Array.init (Array.length r.non_linearizable_size) @@ fun _ -> - Atomic.make_contended 0 - else r.non_linearizable_size + let new_r = + { + r with + pending = + Resize { buckets; size = (if clear then Size.create () else r.size) }; + } in - let new_r = { r with pending = Resize { buckets; non_linearizable_size } } in Atomic.compare_and_set t r new_r && begin finish t new_r |> ignore; true end -let rec adjust_estimated_size t r mask delta result = - let i = Multicore_magic.instantaneous_domain_index () in - let n = Array.length r.non_linearizable_size in - if i < n then begin - Atomic.fetch_and_add (Array.unsafe_get r.non_linearizable_size i) delta - |> ignore; +let adjust_size t r mask result = + if + r.pending == Nothing + && Int64.to_int (Random.bits64 ()) land mask = 0 + && Atomic.get t == r + then begin (* Reading the size is potentially expensive, so we only check it occasionally. The bigger the table the less frequently we should need to resize. *) - if - r.pending == Nothing - && Int64.to_int (Random.bits64 ()) land mask = 0 - && Atomic.get t == r - then begin - let estimated_size = estimated_size r in - let capacity = Atomic_array.length r.buckets in - if capacity < estimated_size && capacity < r.max_buckets then - try_resize t r (capacity + capacity) ~clear:false |> ignore - else if - r.min_buckets < capacity - && estimated_size + estimated_size + estimated_size < capacity - then try_resize t r (capacity lsr 1) ~clear:false |> ignore - end; - result - end - else - let new_cs = - (* We use [n + n + 1] as it keeps the length of the array as a power of 2 - minus 1 and so the size of the array/block including header word will - be a power of 2. *) - Array.init (n + n + 1) @@ fun i -> - if i < n then Array.unsafe_get r.non_linearizable_size i - else Atomic.make_contended 0 - in - let new_r = { r with non_linearizable_size = new_cs } in - let r = if Atomic.compare_and_set t r new_r then new_r else Atomic.get t in - adjust_estimated_size t r mask delta result + let size = Size.get r.size in + let capacity = Atomic_array.length r.buckets in + if capacity < size && capacity < r.max_buckets then + try_resize t r (capacity + capacity) ~clear:false |> ignore + else if r.min_buckets < capacity && size + size + size < capacity then + try_resize t r (capacity lsr 1) ~clear:false |> ignore + end; + result (* *) @@ -342,16 +378,24 @@ let find_node t key = let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - match Atomic_array.unsafe_fenceless_get r.buckets i with - | B Nil -> Nil - | B (Cons cons_r as cons) -> - if r.equal cons_r.key key then cons - else assoc_node r.equal key cons_r.rest - | B (Resize resize_r) -> - (* A resize is in progress. The spine of the resize still holds what was - in the bucket before resize reached that bucket. *) - assoc_node r.equal key resize_r.spine + let rec loop = function + | B (Nil_with_size nil_r) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once r.size nil_r.size_modifier; + Nil + | B (Cons_with_size cons_r) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + if r.equal cons_r.key key then + Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } + else assoc_node r.equal key cons_r.rest + | B (Resize resize_r) -> + (* A resize is in progress. The spine of the resize still holds what was + in the bucket before resize reached that bucket. *) + loop (B resize_r.spine) + in + loop @@ Atomic_array.unsafe_fenceless_get r.buckets i (* *) let find_exn t key = @@ -369,17 +413,47 @@ let rec try_add t key value backoff = let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in match Atomic_array.unsafe_fenceless_get r.buckets i with - | B Nil -> - let after = Cons { key; value; rest = Nil } in - if Atomic_array.unsafe_compare_and_set r.buckets i (B Nil) (B after) then - adjust_estimated_size t r mask 1 true + | B (Nil_with_size nil_r as before) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once r.size nil_r.size_modifier; + let (Cons_with_size cons_r as after : ('a, 'b, [ `Cons_with_size ]) tdt) = + Cons_with_size + { + size_modifier = Size.new_once r.size Size.incr; + key; + value; + rest = Nil; + } + in + if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + adjust_size t r mask true) else try_add t key value (Backoff.once backoff) - | B (Cons _ as before) -> - if assoc_node r.equal key before != Nil then false + | B (Cons_with_size cons_r as before) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + if r.equal cons_r.key key then false + else if assoc_node r.equal key cons_r.rest != Nil then false else - let after = Cons { key; value; rest = before } in + let (Cons_with_size cons_r as after) : ('a, 'b, [ `Cons_with_size ]) tdt + = + Cons_with_size + { + size_modifier = Size.(new_once r.size incr); + key; + value; + rest = + Cons + { key = cons_r.key; value = cons_r.value; rest = cons_r.rest }; + } + in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then adjust_estimated_size t r mask 1 true + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + adjust_size t r mask true) else try_add t key value (Backoff.once backoff) | B (Resize _) -> let _ = finish t (Atomic.get t) in @@ -400,23 +474,63 @@ let rec remove_node t key backoff = let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in match Atomic_array.unsafe_fenceless_get r.buckets i with - | B Nil -> Nil - | B (Cons cons_r as before) -> begin + | B (Nil_with_size nil_r) -> + if nil_r.size_modifier != Size.used_once then ( + Size.update_once r.size nil_r.size_modifier; + nil_r.size_modifier <- Size.used_once); + Nil + | B (Cons_with_size cons_r as before) -> begin + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + + let size_modifier = Size.new_once r.size Size.decr in if r.equal cons_r.key key then - if - Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B cons_r.rest) - then adjust_estimated_size t r mask (-1) before - else remove_node t key (Backoff.once backoff) + let found_node = + Cons { key = cons_r.key; value = cons_r.value; rest = Nil } + in + match cons_r.rest with + | Nil -> + let (Nil_with_size nil_r as after) : + ('a, 'b, [ `Nil_with_size ]) tdt = + Nil_with_size { size_modifier } + in + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B after) + then ( + Size.update_once r.size nil_r.size_modifier; + nil_r.size_modifier <- Size.used_once; + adjust_size t r mask found_node) + else remove_node t key (Backoff.once backoff) + | Cons next -> + let (Cons_with_size cons_r as after) : + ('a, 'b, [ `Cons_with_size ]) tdt = + Cons_with_size + { + size_modifier; + key = next.key; + value = next.value; + rest = next.rest; + } + in + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) + (B after) + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + adjust_size t r mask found_node) + else remove_node t key (Backoff.once backoff) else match dissoc r.equal key cons_r.rest with | (Nil | Cons _) as rest -> if Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B (Cons { cons_r with rest })) - then - assoc_node r.equal key cons_r.rest - |> adjust_estimated_size t r mask (-1) + (B (Cons_with_size { cons_r with rest; size_modifier })) + then ( + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once; + assoc_node r.equal key cons_r.rest |> adjust_size t r mask) else remove_node t key (Backoff.once backoff) | exception Not_found -> Nil end @@ -447,8 +561,15 @@ let rec snapshot t ~clear backoff = else loop (i + 1) (match Atomic_array.unsafe_fenceless_get snapshot i with - | B (Resize spine_r) -> spine_r.spine - | B (Nil | Cons _) -> + | B (Resize { spine = Nil_with_size _ }) -> Nil + | B (Resize { spine = Cons_with_size cons_r }) -> + Cons + { + key = cons_r.key; + value = cons_r.value; + rest = cons_r.rest; + } + | B (Nil_with_size _ | Cons_with_size _) -> (* After resize only [Resize] values should be left in the old buckets. *) assert false) @@ -464,21 +585,26 @@ let remove_all t = snapshot t ~clear:true Backoff.default (* *) -let rec try_find_random_non_empty_bucket buckets seed i = +let rec try_find_random_non_empty_bucket size buckets seed i = match Atomic_array.unsafe_fenceless_get buckets i with - | B Nil | B (Resize { spine = Nil }) -> + | B (Nil_with_size nil_r) | B (Resize { spine = Nil_with_size nil_r }) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once size nil_r.size_modifier; let mask = Atomic_array.length buckets - 1 in let i = (i + 1) land mask in if i <> seed land mask then - try_find_random_non_empty_bucket buckets seed i + try_find_random_non_empty_bucket size buckets seed i else Nil - | B (Cons cons_r) | B (Resize { spine = Cons cons_r }) -> Cons cons_r + | B (Cons_with_size cons_r) | B (Resize { spine = Cons_with_size cons_r }) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once size cons_r.size_modifier; + Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } let try_find_random_non_empty_bucket t = - let buckets = (Atomic.get t).buckets in + let r = Atomic.get t in let seed = Int64.to_int (Random.bits64 ()) in - try_find_random_non_empty_bucket buckets seed - (seed land (Atomic_array.length buckets - 1)) + try_find_random_non_empty_bucket r.size r.buckets seed + (seed land (Atomic_array.length r.buckets - 1)) let rec length spine n = match spine with Nil -> n | Cons r -> length r.rest (n + 1) @@ -504,3 +630,5 @@ let find_random_exn t = let n = Array.length bindings in if n <> 0 then fst (Array.unsafe_get bindings (Random.int n)) else raise_notrace Not_found + +let length t = (Atomic.get t).size |> Size.get diff --git a/test/htbl/dune b/test/htbl/dune index 3155fe35..8a5a689b 100644 --- a/test/htbl/dune +++ b/test/htbl/dune @@ -13,6 +13,11 @@ (copy ../../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) (package saturn_lockfree)) +(rule + (action + (copy ../../src_lockfree/size.ml size.ml)) + (package saturn_lockfree)) + (test (package saturn_lockfree) (name dscheck_htbl) @@ -24,7 +29,7 @@ (and (= %{arch_sixtyfour} false) (= %{architecture} arm))))) - (modules htbl htbl_unsafe htbl_intf htbl_utils dscheck_htbl) + (modules htbl htbl_unsafe htbl_intf htbl_utils dscheck_htbl size) (flags (:standard -open Multicore_magic_dscheck))) diff --git a/test/htbl/stm_htbl.ml b/test/htbl/stm_htbl.ml index 2f3fa85d..58198015 100644 --- a/test/htbl/stm_htbl.ml +++ b/test/htbl/stm_htbl.ml @@ -32,6 +32,7 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct | Try_remove of int | To_keys | Remove_all + | Length let show_cmd c = match c with @@ -40,6 +41,7 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct | Try_remove x -> "Try_remove " ^ string_of_int x | To_keys -> "To_keys" | Remove_all -> "Remove_all" + | Length -> "Length" module State = Set.Make (Int) @@ -53,6 +55,7 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct Gen.int_bound 10 |> Gen.map (fun x -> Try_remove x); Gen.return To_keys; Gen.return Remove_all; + Gen.return Length; ] |> Gen.oneof |> make ~print:show_cmd @@ -67,6 +70,7 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct | Try_remove x -> State.remove x s | To_keys -> s | Remove_all -> State.empty + | Length -> s let precond _ _ = true @@ -82,6 +86,7 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct | Try_remove x -> Res (bool, Htbl.try_remove d x) | To_keys -> Res (seq int, Htbl.to_seq d |> Seq.map fst) | Remove_all -> Res (seq int, Htbl.remove_all d |> Seq.map fst) + | Length -> Res (int, Htbl.length d) let postcond c (s : state) res = match (c, res) with @@ -90,6 +95,7 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct | Try_remove x, Res ((Bool, _), res) -> res = State.mem x s | To_keys, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s | Remove_all, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s + | Length, Res ((Int, _), res) -> res = State.cardinal s | _, _ -> false end From c7b0ad8736de7858758ec370c2ea181ae9665bb2 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 9 Oct 2024 11:46:47 +0200 Subject: [PATCH 10/16] Apply reviews. --- bench/bench_htbl.ml | 93 +-- dune-project | 2 +- saturn.opam | 2 +- src_lockfree/htbl/dune | 20 + .../htbl/{htbl_unsafe.ml => htbl.body.ml} | 102 ++- src_lockfree/htbl/htbl.head_safe.ml | 27 + src_lockfree/htbl/htbl.head_unsafe.ml | 16 + src_lockfree/htbl/htbl.ml | 645 ------------------ test/htbl/dscheck_htbl.ml | 106 ++- test/htbl/stm_htbl.ml | 9 +- 10 files changed, 210 insertions(+), 812 deletions(-) create mode 100644 src_lockfree/htbl/dune rename src_lockfree/htbl/{htbl_unsafe.ml => htbl.body.ml} (88%) create mode 100644 src_lockfree/htbl/htbl.head_safe.ml create mode 100644 src_lockfree/htbl/htbl.head_unsafe.ml delete mode 100644 src_lockfree/htbl/htbl.ml diff --git a/bench/bench_htbl.ml b/bench/bench_htbl.ml index e0da6ed7..5fe3e244 100644 --- a/bench/bench_htbl.ml +++ b/bench/bench_htbl.ml @@ -1,76 +1,79 @@ open Multicore_bench +module Key = struct + type t = int + + let equal = Int.equal + let hash = Fun.id +end + let run_one ~budgetf ~n_domains ?(n_ops = 20 * Util.iter_factor) ?(n_keys = 10000) ~percent_mem ?(percent_add = (100 - percent_mem + 1) / 2) - ?(prepopulate = true) (module Htbl : Htbl_intf.HTBL) = - let percent_rem = 100 - (percent_mem + percent_add) in - + ?(prepopulate = true) ~unsafe (module Htbl : Htbl_intf.HTBL) = let limit_mem = percent_mem in let limit_add = percent_mem + percent_add in assert (0 <= limit_mem && limit_mem <= 100); assert (limit_mem <= limit_add && limit_add <= 100); - let t = Htbl.create ~hashed_type:(module Int) () in - if prepopulate then - for _ = 1 to n_keys do - let value = Random.bits () in - let key = value mod n_keys in - Htbl.try_add t key value |> ignore - done; + let t = Htbl.create ~hashed_type:(module Key) () in let n_ops = (100 + percent_mem) * n_ops / 100 in let n_ops = n_ops * n_domains in - let n_ops_todo = Atomic.make 0 |> Multicore_magic.copy_as_padded in + let n_ops_todo = Countdown.create ~n_domains () in - let init _ = - Atomic.set n_ops_todo n_ops; - Random.State.make_self_init () + let before () = + let _ : _ Seq.t = Htbl.remove_all t in + Countdown.non_atomic_set n_ops_todo n_ops in - let work _ state = + let init i = + let state = Random.State.make_self_init () in + if prepopulate then begin + let n = ((i + 1) * n_keys / n_domains) - (i * n_keys / n_domains) in + for _ = 1 to n do + let value = Random.State.bits state in + let key = value mod n_keys in + Htbl.try_add t key value |> ignore + done + end; + state + in + let work domain_index state = let rec work () = - let n = Util.alloc n_ops_todo in - if n <> 0 then - let rec loop n = - if 0 < n then - let value = Random.State.bits state in - let op = (value asr 20) mod 100 in - let key = value mod n_keys in - if op < limit_mem then begin - Htbl.mem t key |> ignore; - loop (n - 1) - end - else if op < limit_add then begin - Htbl.try_add t key value |> ignore; - loop (n - 1) - end - else begin - Htbl.try_remove t key |> ignore; - loop (n - 1) - end - else work () - in - loop n + 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 + match Htbl.find_exn t key with _ -> () | exception Not_found -> () + else if op < limit_add then Htbl.try_add t key value |> ignore + else Htbl.try_remove t key |> ignore + done; + work () + end in work () in - let config = - Printf.sprintf "%d workers, %d%% mem %d%% add %d%% rem" n_domains - percent_mem percent_add percent_rem + Printf.sprintf "%d worker%s, %d%% reads %s" n_domains + (if n_domains = 1 then "" else "s") + percent_mem + (if unsafe then " (unsafe)" else "") in - Times.record ~budgetf ~n_domains ~init ~work () + Times.record ~budgetf ~n_domains ~before ~init ~work () |> Times.to_thruput_metrics ~n:n_ops ~singular:"operation" ~config let run_suite ~budgetf = - let run (module Htbl : Htbl_intf.HTBL) = + let run ~unsafe (module Htbl : Htbl_intf.HTBL) = Util.cross [ 10; 50; 90 ] [ 1; 2; 4 ] |> List.concat_map @@ fun (percent_mem, n_domains) -> - run_one ~budgetf ~n_domains ~percent_mem (module Htbl) + run_one ~budgetf ~n_domains ~percent_mem ~unsafe (module Htbl) in List.fold_right2 (fun safe unsafe acc -> safe :: unsafe :: acc) - (run (module Saturn_lockfree.Htbl)) - (run (module Saturn_lockfree.Htbl_unsafe)) + (run ~unsafe:false (module Saturn_lockfree.Htbl)) + (run ~unsafe:true (module Saturn_lockfree.Htbl_unsafe)) [] diff --git a/dune-project b/dune-project index 253348b6..8ba31ea4 100644 --- a/dune-project +++ b/dune-project @@ -16,7 +16,7 @@ (domain_shims (and (>= 0.1.0) :with-test)) (saturn_lockfree (= :version)) (multicore-magic (and (>= 2.3.0) :with-test)) - (multicore-bench (and (>= 0.1.2) :with-test)) + (multicore-bench (and (>= 0.1.7) :with-test)) (multicore-magic-dscheck (and (>= 2.3.0) :with-test)) (backoff (and (>= 0.1.0) :with-test)) (alcotest (and (>= 1.7.0) :with-test)) diff --git a/saturn.opam b/saturn.opam index dcece74c..22bb9aae 100644 --- a/saturn.opam +++ b/saturn.opam @@ -14,7 +14,7 @@ depends: [ "domain_shims" {>= "0.1.0" & with-test} "saturn_lockfree" {= version} "multicore-magic" {>= "2.3.0" & with-test} - "multicore-bench" {>= "0.1.2" & with-test} + "multicore-bench" {>= "0.1.7" & with-test} "multicore-magic-dscheck" {>= "2.3.0" & with-test} "backoff" {>= "0.1.0" & with-test} "alcotest" {>= "1.7.0" & with-test} diff --git a/src_lockfree/htbl/dune b/src_lockfree/htbl/dune new file mode 100644 index 00000000..66f64cdb --- /dev/null +++ b/src_lockfree/htbl/dune @@ -0,0 +1,20 @@ +(rule + (action + (with-stdout-to + htbl.ml + (progn + (echo "# 1 \"htbl.head_safe.ml\"\n") + (cat htbl.head_safe.ml) + (echo "# 1 \"htbl.body.ml\"\n") + (cat htbl.body.ml))))) + +(rule + (action + (with-stdout-to + htbl_unsafe.ml + (progn + (echo "# 1 \"htbl.head_unsafe.ml\"\n") + (cat htbl.head_safe.ml) + (echo "# 1 \"htbl.body.ml\"\n") + (cat htbl.body.ml))))) + diff --git a/src_lockfree/htbl/htbl_unsafe.ml b/src_lockfree/htbl/htbl.body.ml similarity index 88% rename from src_lockfree/htbl/htbl_unsafe.ml rename to src_lockfree/htbl/htbl.body.ml index 495b54f3..0136fbf3 100644 --- a/src_lockfree/htbl/htbl_unsafe.ml +++ b/src_lockfree/htbl/htbl.body.ml @@ -1,20 +1,4 @@ -(* Copyright (c) 2023 Vesa Karvonen - - Permission to use, copy, modify, and/or distribute this software for any - purpose with or without fee is hereby granted, provided that the above - copyright notice and this permission notice appear in all copies. - - THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH - REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY - AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM - LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR - OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - PERFORMANCE OF THIS SOFTWARE. *) - open Htbl_utils -module Atomic = Multicore_magic.Transparent_atomic -module Atomic_array = Multicore_magic.Atomic_array type 'k hashed_type = (module Stdlib.Hashtbl.HashedType with type t = 'k) @@ -42,9 +26,9 @@ type ('k, 'v, _) tdt = } -> ('k, 'v, [> `Resize ]) tdt (** During resizing and snapshotting target buckets will be initialized - with a physically unique [Resize] value and the source buckets will - then be gradually updated to [Resize] values and the target buckets - updated with data from the source buckets. *) + with a physically unique [Resize] value and the source buckets will + then be gradually updated to [Resize] values and the target buckets + updated with data from the source buckets. *) type ('k, 'v) bucket = | B : @@ -66,7 +50,7 @@ type ('k, 'v) state = { max_buckets : int; } (** This record is [7 + 1] words and should be aligned on such a boundary on the - second generation heap. It is probably not worth it to pad it further. *) + second generation heap. It is probably not worth it to pad it further. *) type ('k, 'v) t = ('k, 'v) state Atomic.t @@ -128,7 +112,6 @@ let rec take_at backoff size bs i = as spine) -> begin if size_modifier != Size.used_once then Size.update_once size size_modifier; - if Atomic_array.unsafe_compare_and_set bs i (B spine) (B (Resize { spine })) @@ -236,14 +219,19 @@ let merge size (rest : ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt) : Size.update_once size r.size_modifier; rest | Cons_with_size r -> begin + begin + match rest with + | Nil_with_size r' -> + if r'.size_modifier != Size.used_once then + Size.update_once size r'.size_modifier + | Cons_with_size r' -> begin + if r'.size_modifier != Size.used_once then + Size.update_once size r'.size_modifier + end + end; match rest with - | Nil_with_size r' -> - if r'.size_modifier != Size.used_once then - Size.update_once size r'.size_modifier; - Cons_with_size r + | Nil_with_size _ -> Cons_with_size r | Cons_with_size r' -> begin - if r'.size_modifier != Size.used_once then - Size.update_once size r'.size_modifier; Cons_with_size { r with @@ -372,30 +360,29 @@ let rec assoc_node t key = function | Nil -> (Nil : (_, _, [< `Nil | `Cons ]) tdt) | Cons r as cons -> if t r.key key then cons else assoc_node t key r.rest +let rec assoc r key = function + | B (Nil_with_size nil_r) -> + if nil_r.size_modifier != Size.used_once then + Size.update_once r.size nil_r.size_modifier; + Nil + | B (Cons_with_size cons_r) -> + if cons_r.size_modifier != Size.used_once then + Size.update_once r.size cons_r.size_modifier; + if r.equal cons_r.key key then + Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } + else assoc_node r.equal key cons_r.rest + | B (Resize resize_r) -> + (* A resize is in progress. The spine of the resize still holds what was + in the bucket before resize reached that bucket. *) + assoc r key (B resize_r.spine) + let find_node t key = (* Reads can proceed in parallel with writes. *) let r = Atomic.get t in let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - let rec loop = function - | B (Nil_with_size nil_r) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once r.size nil_r.size_modifier; - Nil - | B (Cons_with_size cons_r) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; - if r.equal cons_r.key key then - Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } - else assoc_node r.equal key cons_r.rest - | B (Resize resize_r) -> - (* A resize is in progress. The spine of the resize still holds what was - in the bucket before resize reached that bucket. *) - loop (B resize_r.spine) - in - - loop @@ Atomic_array.unsafe_fenceless_get r.buckets i + assoc r key @@ Atomic_array.unsafe_fenceless_get r.buckets i (* *) let find_exn t key = @@ -450,10 +437,11 @@ let rec try_add t key value backoff = } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then ( + then begin Size.update_once r.size cons_r.size_modifier; cons_r.size_modifier <- Size.used_once; - adjust_size t r mask true) + adjust_size t r mask true + end else try_add t key value (Backoff.once backoff) | B (Resize _) -> let _ = finish t (Atomic.get t) in @@ -475,9 +463,10 @@ let rec remove_node t key backoff = let i = h land mask in match Atomic_array.unsafe_fenceless_get r.buckets i with | B (Nil_with_size nil_r) -> - if nil_r.size_modifier != Size.used_once then ( + if nil_r.size_modifier != Size.used_once then begin Size.update_once r.size nil_r.size_modifier; - nil_r.size_modifier <- Size.used_once); + nil_r.size_modifier <- Size.used_once + end; Nil | B (Cons_with_size cons_r as before) -> begin if cons_r.size_modifier != Size.used_once then @@ -497,10 +486,11 @@ let rec remove_node t key backoff = if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then ( + then begin Size.update_once r.size nil_r.size_modifier; nil_r.size_modifier <- Size.used_once; - adjust_size t r mask found_node) + adjust_size t r mask found_node + end else remove_node t key (Backoff.once backoff) | Cons next -> let (Cons_with_size cons_r as after) : @@ -516,10 +506,11 @@ let rec remove_node t key backoff = if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then ( + then begin Size.update_once r.size cons_r.size_modifier; cons_r.size_modifier <- Size.used_once; - adjust_size t r mask found_node) + adjust_size t r mask found_node + end else remove_node t key (Backoff.once backoff) else match dissoc r.equal key cons_r.rest with @@ -527,10 +518,11 @@ let rec remove_node t key backoff = if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B (Cons_with_size { cons_r with rest; size_modifier })) - then ( + then begin Size.update_once r.size cons_r.size_modifier; cons_r.size_modifier <- Size.used_once; - assoc_node r.equal key cons_r.rest |> adjust_size t r mask) + assoc_node r.equal key cons_r.rest |> adjust_size t r mask + end else remove_node t key (Backoff.once backoff) | exception Not_found -> Nil end diff --git a/src_lockfree/htbl/htbl.head_safe.ml b/src_lockfree/htbl/htbl.head_safe.ml new file mode 100644 index 00000000..aafe7bfe --- /dev/null +++ b/src_lockfree/htbl/htbl.head_safe.ml @@ -0,0 +1,27 @@ +(* Copyright (c) 2023 Vesa Karvonen + + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. + + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH + REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY + AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, + INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM + LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR + OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR + PERFORMANCE OF THIS SOFTWARE. *) + +module Atomic_array = struct + type 'a t = 'a Atomic.t array + + let[@inline] at (xs : 'a t) i : 'a Atomic.t = Array.get xs i + let[@inline] make n v = Array.init n @@ fun _ -> Atomic.make v + + external length : 'a array -> int = "%array_length" + + let unsafe_fenceless_get xs i = Atomic.get xs.(i) + + let[@inline] unsafe_compare_and_set xs i b a = + Atomic.compare_and_set (at xs i) b a +end diff --git a/src_lockfree/htbl/htbl.head_unsafe.ml b/src_lockfree/htbl/htbl.head_unsafe.ml new file mode 100644 index 00000000..afa557a4 --- /dev/null +++ b/src_lockfree/htbl/htbl.head_unsafe.ml @@ -0,0 +1,16 @@ +(* Copyright (c) 2023 Vesa Karvonen + + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. + + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH + REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY + AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, + INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM + LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR + OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR + PERFORMANCE OF THIS SOFTWARE. *) + +module Atomic = Multicore_magic.Transparent_atomic +module Atomic_array = Multicore_magic.Atomic_array diff --git a/src_lockfree/htbl/htbl.ml b/src_lockfree/htbl/htbl.ml deleted file mode 100644 index 698b1f7a..00000000 --- a/src_lockfree/htbl/htbl.ml +++ /dev/null @@ -1,645 +0,0 @@ -(* Copyright (c) 2023 Vesa Karvonen - - Permission to use, copy, modify, and/or distribute this software for any - purpose with or without fee is hereby granted, provided that the above - copyright notice and this permission notice appear in all copies. - - THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH - REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY - AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM - LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR - OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - PERFORMANCE OF THIS SOFTWARE. *) -open Htbl_utils - -module Atomic_array = struct - type 'a t = 'a Atomic.t array - - let[@inline] at (xs : 'a t) i : 'a Atomic.t = Array.get xs i - let[@inline] make n v = Array.init n @@ fun _ -> Atomic.make v - - external length : 'a array -> int = "%array_length" - - let unsafe_fenceless_get xs i = Atomic.get xs.(i) - - let[@inline] unsafe_compare_and_set xs i b a = - Atomic.compare_and_set (at xs i) b a -end - -type 'k hashed_type = (module Stdlib.Hashtbl.HashedType with type t = 'k) - -type ('k, 'v, _) tdt = - | Nil : ('k, 'v, [> `Nil ]) tdt - | Cons : { - key : 'k; - value : 'v; - rest : ('k, 'v, [ `Nil | `Cons ]) tdt; - } - -> ('k, 'v, [> `Cons ]) tdt - | Nil_with_size : { - mutable size_modifier : Size.once; - } - -> ('k, 'v, [> `Nil_with_size ]) tdt - | Cons_with_size : { - mutable size_modifier : Size.once; - key : 'k; - value : 'v; - rest : ('k, 'v, [ `Nil | `Cons ]) tdt; - } - -> ('k, 'v, [> `Cons_with_size ]) tdt - | Resize : { - spine : ('k, 'v, [ `Nil_with_size | `Cons_with_size ]) tdt; - } - -> ('k, 'v, [> `Resize ]) tdt - (** During resizing and snapshotting target buckets will be initialized - with a physically unique [Resize] value and the source buckets will - then be gradually updated to [Resize] values and the target buckets - updated with data from the source buckets. *) - -type ('k, 'v) bucket = - | B : - ('k, 'v, [< `Nil_with_size | `Cons_with_size | `Resize ]) tdt - -> ('k, 'v) bucket -[@@unboxed] - -type ('k, 'v) pending = - | Nothing - | Resize of { buckets : ('k, 'v) bucket Atomic_array.t; size : Size.t } - -type ('k, 'v) state = { - hash : 'k -> int; - buckets : ('k, 'v) bucket Atomic_array.t; - equal : 'k -> 'k -> bool; - size : Size.t; - pending : ('k, 'v) pending; - min_buckets : int; - max_buckets : int; -} -(** This record is [7 + 1] words and should be aligned on such a boundary on the - second generation heap. It is probably not worth it to pad it further. *) - -type ('k, 'v) t = ('k, 'v) state Atomic.t - -let create (type k) ?hashed_type ?min_buckets ?max_buckets () = - let min_buckets = - match min_buckets with - | None -> min_buckets_default - | Some n -> - let n = Int.max lo_buckets n |> Int.min hi_buckets in - ceil_pow_2_minus_1 (n - 1) + 1 - in - let max_buckets = - match max_buckets with - | None -> Int.max min_buckets max_buckets_default - | Some n -> - let n = Int.max min_buckets n |> Int.min hi_buckets in - ceil_pow_2_minus_1 (n - 1) + 1 - in - let equal, hash = - match hashed_type with - | None -> - (( = ), Stdlib.Hashtbl.seeded_hash (Int64.to_int (Random.bits64 ()))) - | Some ((module Hashed_type) : k hashed_type) -> - (Hashed_type.equal, Hashed_type.hash) - in - { - hash; - buckets = - Atomic_array.make min_buckets - (B (Nil_with_size { size_modifier = Size.used_once })); - equal; - size = Size.create (); - pending = Nothing; - min_buckets; - max_buckets; - } - |> Atomic.make_contended - -(* *) - -let hashed_type_of (type k) (t : (k, _) t) : k hashed_type = - let r = Atomic.get t in - (module struct - type t = k - - let hash = r.hash - and equal = r.equal - end) - -let min_buckets_of t = (Atomic.get t).min_buckets -let max_buckets_of t = (Atomic.get t).max_buckets - -(* *) - -let rec take_at backoff size bs i = - match Atomic_array.unsafe_fenceless_get bs i with - | B - ((Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) - as spine) -> begin - if size_modifier != Size.used_once then - Size.update_once size size_modifier; - - if - Atomic_array.unsafe_compare_and_set bs i (B spine) - (B (Resize { spine })) - then spine - else take_at (Backoff.once backoff) size bs i - end - | B (Resize spine_r) -> spine_r.spine - -let rec copy_all r target i t step = - let i = (i + step) land (Atomic_array.length target - 1) in - let spine = take_at Backoff.default r.size r.buckets i in - let (B before) = Atomic_array.unsafe_fenceless_get target i in - (* The [before] value is physically different for each resize and so checking - that the resize has not finished is sufficient to ensure that the - [compare_and_set] below does not disrupt the next resize. *) - Atomic.get t == r - && begin - begin - match before with - | Resize _ -> - Atomic_array.unsafe_compare_and_set target i (B before) (B spine) - |> ignore - | Nil_with_size _ | Cons_with_size _ -> () - end; - i = 0 || copy_all r target i t step - end - -(* *) - -let[@tail_mod_cons] rec filter_ t msk chk = function - | Nil -> Nil - | Cons r -> - if t r.key land msk = chk then - Cons { r with rest = filter_ t msk chk r.rest } - else filter_ t msk chk r.rest - -let[@tail_mod_cons] rec filter_fst t mask chk = function - | Nil -> Nil_with_size { size_modifier = Size.used_once } - | Cons r -> - if t r.key land mask = chk then - Cons_with_size - { - key = r.key; - value = r.value; - size_modifier = Size.used_once; - rest = filter_ t mask chk r.rest; - } - else filter_fst t mask chk r.rest - -let filter t mask chk : - ('a, 'b, [ `Cons_with_size | `Nil_with_size ]) tdt -> - ('a, 'b, [> `Cons_with_size | `Nil_with_size ]) tdt = function - | Nil_with_size s -> Nil_with_size s - | Cons_with_size r -> begin - if t r.key land mask = chk then - Cons_with_size { r with rest = filter_ t mask chk r.rest } - else filter_fst t mask chk r.rest - end - -let rec split_all r target i t step = - let i = (i + step) land (Atomic_array.length r.buckets - 1) in - let spine = take_at Backoff.default r.size r.buckets i in - let high = Atomic_array.length r.buckets in - let after_lo = filter r.hash high 0 spine in - let after_hi = filter r.hash high high spine in - let (B before_lo) = Atomic_array.unsafe_fenceless_get target i in - let (B before_hi) = Atomic_array.unsafe_fenceless_get target (i + high) in - (* The [before_lo] and [before_hi] values are physically different for each - resize and so checking that the resize has not finished is sufficient to - ensure that the [compare_and_set] below does not disrupt the next - resize. *) - Atomic.get t == r - && begin - begin - match before_lo with - | Resize _ -> - Atomic_array.unsafe_compare_and_set target i (B before_lo) - (B after_lo) - |> ignore - | Nil_with_size _ | Cons_with_size _ -> () - end; - begin - match before_hi with - | Resize _ -> - Atomic_array.unsafe_compare_and_set target (i + high) (B before_hi) - (B after_hi) - |> ignore - | Nil_with_size _ | Cons_with_size _ -> () - end; - i = 0 || split_all r target i t step - end - -(* *) - -let[@tail_mod_cons] rec merge rest = function - | Nil -> rest - | Cons r -> Cons { r with rest = merge rest r.rest } - -let merge size (rest : ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt) : - ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt -> - ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt = function - | Nil_with_size r -> - (* Each size_modifier that is going to be removed need to be applied *) - if r.size_modifier != Size.used_once then - Size.update_once size r.size_modifier; - rest - | Cons_with_size r -> begin - match rest with - | Nil_with_size r' -> - if r'.size_modifier != Size.used_once then - Size.update_once size r'.size_modifier; - Cons_with_size r - | Cons_with_size r' -> begin - if r'.size_modifier != Size.used_once then - Size.update_once size r'.size_modifier; - Cons_with_size - { - r with - rest = - merge - (Cons { key = r'.key; value = r'.value; rest = r'.rest }) - r.rest; - } - end - end - -let rec merge_all r target i t step = - let i = (i + step) land (Atomic_array.length target - 1) in - let spine_lo = take_at Backoff.default r.size r.buckets i in - let spine_hi = - take_at Backoff.default r.size r.buckets (i + Atomic_array.length target) - in - let after = merge r.size spine_lo spine_hi in - let (B before) = Atomic_array.unsafe_fenceless_get target i in - (* The [before] value is physically different for each resize and so checking - that the resize has not finished is sufficient to ensure that the - [compare_and_set] below does not disrupt the next resize. *) - Atomic.get t == r - && begin - begin - match before with - | Resize _ -> - Atomic_array.unsafe_compare_and_set target i (B before) (B after) - |> ignore - | Nil_with_size _ | Cons_with_size _ -> () - end; - i = 0 || merge_all r target i t step - end - -(* *) - -let[@inline never] rec finish t r = - match r.pending with - | Nothing -> r - | Resize { buckets; size } -> - let high_source = Atomic_array.length r.buckets in - let high_target = Atomic_array.length buckets in - (* We step by random amount to better allow cores to work in parallel. - The number of buckets is always a power of two, so any odd number is - relatively prime or coprime. *) - let step = Int64.to_int (Random.bits64 ()) lor 1 in - if - if high_source < high_target then begin - (* We are growing the table. *) - split_all r buckets 0 t step - end - else if high_target < high_source then begin - (* We are shrinking the table. *) - merge_all r buckets 0 t step - end - else begin - (* We are snapshotting the table. *) - copy_all r buckets 0 t step - end - then - let new_r = { r with buckets; size; pending = Nothing } in - if Atomic.compare_and_set t r new_r then new_r - else finish t (Atomic.get t) - else finish t (Atomic.get t) - -(* *) - -(** This must be called with [r.pending == Nothing]. *) -let[@inline never] try_resize t r new_capacity ~clear = - (* We must make sure that on every resize we use a physically different - [Resize _] value to indicate unprocessed target buckets. The use of - [Sys.opaque_identity] below ensures that a new value is allocated. *) - let resize_avoid_aba = - if clear then B (Nil_with_size { size_modifier = Size.used_once }) - else - B - (Resize - { - spine = - Sys.opaque_identity - (Nil_with_size { size_modifier = Size.used_once }); - }) - in - let buckets = Atomic_array.make new_capacity resize_avoid_aba in - let new_r = - { - r with - pending = - Resize { buckets; size = (if clear then Size.create () else r.size) }; - } - in - Atomic.compare_and_set t r new_r - && begin - finish t new_r |> ignore; - true - end - -let adjust_size t r mask result = - if - r.pending == Nothing - && Int64.to_int (Random.bits64 ()) land mask = 0 - && Atomic.get t == r - then begin - (* Reading the size is potentially expensive, so we only check it - occasionally. The bigger the table the less frequently we should need to - resize. *) - let size = Size.get r.size in - let capacity = Atomic_array.length r.buckets in - if capacity < size && capacity < r.max_buckets then - try_resize t r (capacity + capacity) ~clear:false |> ignore - else if r.min_buckets < capacity && size + size + size < capacity then - try_resize t r (capacity lsr 1) ~clear:false |> ignore - end; - result - -(* *) - -(** [get] only returns with a state where [pending = Nothing]. *) -let[@inline] get t = - let r = Atomic.get t in - if r.pending == Nothing then r else finish t r - -(* *) - -let rec assoc_node t key = function - | Nil -> (Nil : (_, _, [< `Nil | `Cons ]) tdt) - | Cons r as cons -> if t r.key key then cons else assoc_node t key r.rest - -let find_node t key = - (* Reads can proceed in parallel with writes. *) - let r = Atomic.get t in - let h = r.hash key in - let mask = Atomic_array.length r.buckets - 1 in - let i = h land mask in - let rec loop = function - | B (Nil_with_size nil_r) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once r.size nil_r.size_modifier; - Nil - | B (Cons_with_size cons_r) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; - if r.equal cons_r.key key then - Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } - else assoc_node r.equal key cons_r.rest - | B (Resize resize_r) -> - (* A resize is in progress. The spine of the resize still holds what was - in the bucket before resize reached that bucket. *) - loop (B resize_r.spine) - in - - loop @@ Atomic_array.unsafe_fenceless_get r.buckets i -(* *) - -let find_exn t key = - match find_node t key with - | Nil -> raise_notrace Not_found - | Cons r -> r.value - -let mem t key = find_node t key != Nil - -(* *) - -let rec try_add t key value backoff = - let r = Atomic.get t in - let h = r.hash key in - let mask = Atomic_array.length r.buckets - 1 in - let i = h land mask in - match Atomic_array.unsafe_fenceless_get r.buckets i with - | B (Nil_with_size nil_r as before) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once r.size nil_r.size_modifier; - let (Cons_with_size cons_r as after : ('a, 'b, [ `Cons_with_size ]) tdt) = - Cons_with_size - { - size_modifier = Size.new_once r.size Size.incr; - key; - value; - rest = Nil; - } - in - if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then ( - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - adjust_size t r mask true) - else try_add t key value (Backoff.once backoff) - | B (Cons_with_size cons_r as before) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; - if r.equal cons_r.key key then false - else if assoc_node r.equal key cons_r.rest != Nil then false - else - let (Cons_with_size cons_r as after) : ('a, 'b, [ `Cons_with_size ]) tdt - = - Cons_with_size - { - size_modifier = Size.(new_once r.size incr); - key; - value; - rest = - Cons - { key = cons_r.key; value = cons_r.value; rest = cons_r.rest }; - } - in - if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then ( - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - adjust_size t r mask true) - else try_add t key value (Backoff.once backoff) - | B (Resize _) -> - let _ = finish t (Atomic.get t) in - try_add t key value Backoff.default - -let[@inline] try_add t key value = try_add t key value Backoff.default - -(* *) - -let[@tail_mod_cons] rec dissoc t key = function - | Nil -> raise_notrace Not_found - | Cons r -> - if t key r.key then r.rest else Cons { r with rest = dissoc t key r.rest } - -let rec remove_node t key backoff = - let r = Atomic.get t in - let h = r.hash key in - let mask = Atomic_array.length r.buckets - 1 in - let i = h land mask in - match Atomic_array.unsafe_fenceless_get r.buckets i with - | B (Nil_with_size nil_r) -> - if nil_r.size_modifier != Size.used_once then ( - Size.update_once r.size nil_r.size_modifier; - nil_r.size_modifier <- Size.used_once); - Nil - | B (Cons_with_size cons_r as before) -> begin - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; - - let size_modifier = Size.new_once r.size Size.decr in - if r.equal cons_r.key key then - let found_node = - Cons { key = cons_r.key; value = cons_r.value; rest = Nil } - in - match cons_r.rest with - | Nil -> - let (Nil_with_size nil_r as after) : - ('a, 'b, [ `Nil_with_size ]) tdt = - Nil_with_size { size_modifier } - in - if - Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B after) - then ( - Size.update_once r.size nil_r.size_modifier; - nil_r.size_modifier <- Size.used_once; - adjust_size t r mask found_node) - else remove_node t key (Backoff.once backoff) - | Cons next -> - let (Cons_with_size cons_r as after) : - ('a, 'b, [ `Cons_with_size ]) tdt = - Cons_with_size - { - size_modifier; - key = next.key; - value = next.value; - rest = next.rest; - } - in - if - Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B after) - then ( - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - adjust_size t r mask found_node) - else remove_node t key (Backoff.once backoff) - else - match dissoc r.equal key cons_r.rest with - | (Nil | Cons _) as rest -> - if - Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B (Cons_with_size { cons_r with rest; size_modifier })) - then ( - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - assoc_node r.equal key cons_r.rest |> adjust_size t r mask) - else remove_node t key (Backoff.once backoff) - | exception Not_found -> Nil - end - | B (Resize _) -> - let _ = finish t (Atomic.get t) in - remove_node t key Backoff.default - -let try_remove t key = remove_node t key Backoff.default != Nil - -let remove_exn t key = - match remove_node t key Backoff.default with - | Nil -> raise_notrace Not_found - | Cons r -> r.value - -(* *) - -let rec snapshot t ~clear backoff = - let r = get t in - if try_resize t r (Atomic_array.length r.buckets) ~clear then begin - (* At this point the resize has been completed and a new array is used for - buckets and [r.buckets] now has an immutable copy of what was in the hash - table. *) - let snapshot = r.buckets in - let rec loop i kvs () = - match kvs with - | Nil -> - if i = Atomic_array.length snapshot then Seq.Nil - else - loop (i + 1) - (match Atomic_array.unsafe_fenceless_get snapshot i with - | B (Resize { spine = Nil_with_size _ }) -> Nil - | B (Resize { spine = Cons_with_size cons_r }) -> - Cons - { - key = cons_r.key; - value = cons_r.value; - rest = cons_r.rest; - } - | B (Nil_with_size _ | Cons_with_size _) -> - (* After resize only [Resize] values should be left in the old - buckets. *) - assert false) - () - | Cons r -> Seq.Cons ((r.key, r.value), loop i r.rest) - in - loop 0 Nil - end - else snapshot t ~clear (Backoff.once backoff) - -let to_seq t = snapshot t ~clear:false Backoff.default -let remove_all t = snapshot t ~clear:true Backoff.default - -(* *) - -let rec try_find_random_non_empty_bucket size buckets seed i = - match Atomic_array.unsafe_fenceless_get buckets i with - | B (Nil_with_size nil_r) | B (Resize { spine = Nil_with_size nil_r }) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once size nil_r.size_modifier; - let mask = Atomic_array.length buckets - 1 in - let i = (i + 1) land mask in - if i <> seed land mask then - try_find_random_non_empty_bucket size buckets seed i - else Nil - | B (Cons_with_size cons_r) | B (Resize { spine = Cons_with_size cons_r }) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once size cons_r.size_modifier; - Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } - -let try_find_random_non_empty_bucket t = - let r = Atomic.get t in - let seed = Int64.to_int (Random.bits64 ()) in - try_find_random_non_empty_bucket r.size r.buckets seed - (seed land (Atomic_array.length r.buckets - 1)) - -let rec length spine n = - match spine with Nil -> n | Cons r -> length r.rest (n + 1) - -let length spine = length spine 0 - -let rec nth spine i = - match spine with - | Nil -> impossible () - | Cons r -> if i <= 0 then r.key else nth r.rest (i - 1) - -let find_random_exn t = - match try_find_random_non_empty_bucket t with - | (Cons cons_r as spine : (_, _, [< `Nil | `Cons ]) tdt) -> - (* We found a non-empty bucket - the fast way. *) - if cons_r.rest == Nil then cons_r.key - else - let n = length spine in - nth spine (Random.int n) - | Nil -> - (* We couldn't find a non-empty bucket - the slow way. *) - let bindings = to_seq t |> Array.of_seq in - let n = Array.length bindings in - if n <> 0 then fst (Array.unsafe_get bindings (Random.int n)) - else raise_notrace Not_found - -let length t = (Atomic.get t).size |> Size.get diff --git a/test/htbl/dscheck_htbl.ml b/test/htbl/dscheck_htbl.ml index 1ed76cc7..1088c245 100644 --- a/test/htbl/dscheck_htbl.ml +++ b/test/htbl/dscheck_htbl.ml @@ -4,6 +4,14 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct open Htbl let try_add htbl k = try_add htbl k k + + module Int = struct + type t = int + + let equal = Int.equal + let hash = Hashtbl.hash + end + let create ?min_buckets () = create ?min_buckets ~hashed_type:(module Int) () let _two_mem () = @@ -52,71 +60,42 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct && mem htbl 1 && mem htbl 21 && mem htbl 22))) let _two_add_resize () = - (* Trying to trigger resize *) - let random_offset = Random.int 1000 in - for i = 0 to 5 do - Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> - Random.init (random_offset + i); - let htbl = create ~min_buckets:2 () in - try_add htbl 1 |> ignore; - try_add htbl 2 |> ignore; + (* Should trigger a resize *) + Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> + Random.init 0; + let htbl = create ~min_buckets:2 () in + try_add htbl 1 |> ignore; + try_add htbl 2 |> ignore; - let added1, added2 = (ref false, ref false) in + let added1, added2 = (ref false, ref false) in - Atomic.spawn (fun () -> added1 := try_add htbl 21); - Atomic.spawn (fun () -> added2 := try_add htbl 22); + Atomic.spawn (fun () -> added1 := try_add htbl 21); + Atomic.spawn (fun () -> added2 := try_add htbl 22); - Atomic.final (fun () -> - Atomic.check (fun () -> - !added1 && !added2 && mem htbl 21 && mem htbl 22))); - Dscheck.Trace_tracker.print_traces stdout - done + Atomic.final (fun () -> + Atomic.check (fun () -> + !added1 && !added2 && mem htbl 21 && mem htbl 22))); + Dscheck.Trace_tracker.print_traces stdout let _two_add_resize2 () = - (* Trying to trigger resize *) - let random_offset = Random.int 1000 in - for i = 0 to 5 do - Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> - Random.init (random_offset + i); - let htbl = create ~min_buckets:2 () in - try_add htbl 1 |> ignore; - try_add htbl 2 |> ignore; - - let added1, added2 = (ref false, ref false) in - - Atomic.spawn (fun () -> added1 := try_add htbl 1); - Atomic.spawn (fun () -> added2 := try_add htbl 2); - - Atomic.final (fun () -> - Atomic.check (fun () -> - (not !added1) && (not !added2) && mem htbl 1 && mem htbl 2))); - Dscheck.Trace_tracker.print_traces stdout - done - - let _two_add_resize3 () = - (* Trying to trigger resize *) - let random_offset = Random.int 1000 in - for i = 0 to 5 do - Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> - Random.init (random_offset + i); - let htbl = create ~min_buckets:2 () in - try_add htbl 1 |> ignore; - try_add htbl 2 |> ignore; + Atomic.trace ~interleavings:stdout ~record_traces:true (fun () -> + Random.init 6; + let htbl = create ~min_buckets:2 () in + try_add htbl 1 |> ignore; + try_add htbl 2 |> ignore; - let added1, added2 = (ref false, ref false) in + let added1, added2 = (ref false, ref false) in - Atomic.spawn (fun () -> added1 := try_add htbl 1); - Atomic.spawn (fun () -> added2 := try_add htbl 22); + Atomic.spawn (fun () -> added1 := try_add htbl 1); + Atomic.spawn (fun () -> added2 := try_add htbl 22); - Atomic.final (fun () -> - Atomic.check (fun () -> - (not !added1) && !added2 && mem htbl 1 && mem htbl 22))); - Dscheck.Trace_tracker.print_traces stdout - done + Atomic.final (fun () -> + Atomic.check (fun () -> + (not !added1) && !added2 && mem htbl 1 && mem htbl 22))); + Dscheck.Trace_tracker.print_traces stdout let _two_remove () = let random_offset = Random.int 1000 in - (* for i = 0 to 4 do *) Atomic.trace (fun () -> Random.init (random_offset + 0); let htbl = create ~min_buckets:8 () in @@ -144,7 +123,6 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct && !removed4 && List.init 12 (fun i -> not (mem htbl i)) |> List.for_all (fun x -> x)))) - (* done *) let _two_add_remove_same () = let seed = Random.int 1000 in @@ -244,7 +222,6 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct test_case "2-add" `Slow _two_add; test_case "2-add-resize" `Slow _two_add_resize; test_case "2-add-resize2" `Slow _two_add_resize2; - test_case "2-add-resize3" `Slow _two_add_resize3; test_case "2-remove" `Slow _two_remove; test_case "2-add-remove-same" `Slow _two_add_remove_same; test_case "2-add-remove-alt" `Slow _two_add_remove_alt; @@ -255,9 +232,14 @@ module Dscheck_htbl (Htbl : Htbl_intf.HTBL) = struct end let () = - let module Safe = Dscheck_htbl (Htbl) in - let safe_test = Safe.tests "safe" in - let module Unsafe = Dscheck_htbl (Htbl_unsafe) in - let unsafe_test = Unsafe.tests "unsafe" in - let open Alcotest in - run "DSCheck Hshtbl" (safe_test @ unsafe_test) + (* Both safe and unsafe version have the same body code. We randomly pick one for testing. *) + Random.self_init (); + let safe = Random.bool () in + if safe then + let module Safe = Dscheck_htbl (Htbl) in + let open Alcotest in + run "DSCheck Hshtbl" (Safe.tests "safe") + else + let module Unsafe = Dscheck_htbl (Htbl_unsafe) in + let open Alcotest in + run "DSCheck Hshtbl" (Unsafe.tests "unsafe") diff --git a/test/htbl/stm_htbl.ml b/test/htbl/stm_htbl.ml index 58198015..d425e2ba 100644 --- a/test/htbl/stm_htbl.ml +++ b/test/htbl/stm_htbl.ml @@ -103,9 +103,12 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct end let () = - let module Safe = STM_htbl (Htbls.Htbl) in - let exit_code = Safe.run () in - if exit_code <> 0 then exit exit_code + (* Both safe and unsafe version have the same body code. We randomly pick one for testing. *) + Random.self_init (); + let safe = Random.bool () in + if safe then + let module Safe = STM_htbl (Htbls.Htbl) in + Safe.run () |> exit else let module Unsafe = STM_htbl (Htbls.Htbl_unsafe) in Unsafe.run () |> exit From 4547c06f976dee536063436697c6280da6f2ed33 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 24 Oct 2024 18:32:11 +0200 Subject: [PATCH 11/16] Add Nil at the root level of the bucket to remove the useless allocation of Nil_with_size {size_modifier = Size.used_once} values. --- src_lockfree/htbl/htbl.body.ml | 159 +++++++++++++++++++-------------- 1 file changed, 91 insertions(+), 68 deletions(-) diff --git a/src_lockfree/htbl/htbl.body.ml b/src_lockfree/htbl/htbl.body.ml index 0136fbf3..3e7eb617 100644 --- a/src_lockfree/htbl/htbl.body.ml +++ b/src_lockfree/htbl/htbl.body.ml @@ -22,7 +22,7 @@ type ('k, 'v, _) tdt = } -> ('k, 'v, [> `Cons_with_size ]) tdt | Resize : { - spine : ('k, 'v, [ `Nil_with_size | `Cons_with_size ]) tdt; + spine : ('k, 'v, [ `Nil_with_size | `Cons_with_size | `Nil ]) tdt; } -> ('k, 'v, [> `Resize ]) tdt (** During resizing and snapshotting target buckets will be initialized @@ -32,7 +32,7 @@ type ('k, 'v, _) tdt = type ('k, 'v) bucket = | B : - ('k, 'v, [< `Nil_with_size | `Cons_with_size | `Resize ]) tdt + ('k, 'v, [< `Nil_with_size | `Cons_with_size | `Resize | `Nil ]) tdt -> ('k, 'v) bucket [@@unboxed] @@ -78,9 +78,7 @@ let create (type k) ?hashed_type ?min_buckets ?max_buckets () = in { hash; - buckets = - Atomic_array.make min_buckets - (B (Nil_with_size { size_modifier = Size.used_once })); + buckets = Atomic_array.make min_buckets (B Nil); equal; size = Size.create (); pending = Nothing; @@ -106,19 +104,25 @@ let max_buckets_of t = (Atomic.get t).max_buckets (* *) let rec take_at backoff size bs i = - match Atomic_array.unsafe_fenceless_get bs i with - | B - ((Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) - as spine) -> begin - if size_modifier != Size.used_once then - Size.update_once size size_modifier; + let (B old_bucket) = Atomic_array.unsafe_fenceless_get bs i in + begin + (* Make sure size_modifier has been updated. *) + match old_bucket with + | Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ } -> + if size_modifier != Size.used_once then + Size.update_once size size_modifier + | _ -> () + end; + + match old_bucket with + | (Nil_with_size _ | Cons_with_size _ | Nil) as spine -> begin if Atomic_array.unsafe_compare_and_set bs i (B spine) (B (Resize { spine })) then spine else take_at (Backoff.once backoff) size bs i end - | B (Resize spine_r) -> spine_r.spine + | Resize spine_r -> spine_r.spine let rec copy_all r target i t step = let i = (i + step) land (Atomic_array.length target - 1) in @@ -134,7 +138,7 @@ let rec copy_all r target i t step = | Resize _ -> Atomic_array.unsafe_compare_and_set target i (B before) (B spine) |> ignore - | Nil_with_size _ | Cons_with_size _ -> () + | Nil_with_size _ | Cons_with_size _ | Nil -> () end; i = 0 || copy_all r target i t step end @@ -149,7 +153,7 @@ let[@tail_mod_cons] rec filter_ t msk chk = function else filter_ t msk chk r.rest let[@tail_mod_cons] rec filter_fst t mask chk = function - | Nil -> Nil_with_size { size_modifier = Size.used_once } + | Nil -> Nil | Cons r -> if t r.key land mask = chk then Cons_with_size @@ -162,14 +166,15 @@ let[@tail_mod_cons] rec filter_fst t mask chk = function else filter_fst t mask chk r.rest let filter t mask chk : - ('a, 'b, [ `Cons_with_size | `Nil_with_size ]) tdt -> - ('a, 'b, [> `Cons_with_size | `Nil_with_size ]) tdt = function + ('a, 'b, [ `Cons_with_size | `Nil_with_size | `Nil ]) tdt -> + ('a, 'b, [> `Cons_with_size | `Nil_with_size | `Nil ]) tdt = function | Nil_with_size s -> Nil_with_size s | Cons_with_size r -> begin if t r.key land mask = chk then Cons_with_size { r with rest = filter_ t mask chk r.rest } else filter_fst t mask chk r.rest end + | Nil -> Nil let rec split_all r target i t step = let i = (i + step) land (Atomic_array.length r.buckets - 1) in @@ -191,7 +196,7 @@ let rec split_all r target i t step = Atomic_array.unsafe_compare_and_set target i (B before_lo) (B after_lo) |> ignore - | Nil_with_size _ | Cons_with_size _ -> () + | Nil_with_size _ | Cons_with_size _ | Nil -> () end; begin match before_hi with @@ -199,7 +204,7 @@ let rec split_all r target i t step = Atomic_array.unsafe_compare_and_set target (i + high) (B before_hi) (B after_hi) |> ignore - | Nil_with_size _ | Cons_with_size _ -> () + | Nil_with_size _ | Cons_with_size _ | Nil -> () end; i = 0 || split_all r target i t step end @@ -210,27 +215,28 @@ let[@tail_mod_cons] rec merge rest = function | Nil -> rest | Cons r -> Cons { r with rest = merge rest r.rest } -let merge size (rest : ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt) : - ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt -> - ('a, 'b, [ `Nil_with_size | `Cons_with_size ]) tdt = function +let merge size + (rest : ('a, 'b, [ `Nil_with_size | `Cons_with_size | `Nil ]) tdt) : + ('a, 'b, [ `Nil_with_size | `Cons_with_size | `Nil ]) tdt -> + ('a, 'b, [ `Nil_with_size | `Cons_with_size | `Nil ]) tdt = function | Nil_with_size r -> (* Each size_modifier that is going to be removed need to be applied *) if r.size_modifier != Size.used_once then Size.update_once size r.size_modifier; rest + | Nil -> rest | Cons_with_size r -> begin begin match rest with - | Nil_with_size r' -> - if r'.size_modifier != Size.used_once then - Size.update_once size r'.size_modifier - | Cons_with_size r' -> begin - if r'.size_modifier != Size.used_once then - Size.update_once size r'.size_modifier - end + | Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ } + -> + if size_modifier != Size.used_once then + Size.update_once size size_modifier + | Nil -> () end; match rest with | Nil_with_size _ -> Cons_with_size r + | Nil -> Cons_with_size r | Cons_with_size r' -> begin Cons_with_size { @@ -261,7 +267,7 @@ let rec merge_all r target i t step = | Resize _ -> Atomic_array.unsafe_compare_and_set target i (B before) (B after) |> ignore - | Nil_with_size _ | Cons_with_size _ -> () + | Nil_with_size _ | Cons_with_size _ | Nil -> () end; i = 0 || merge_all r target i t step end @@ -305,15 +311,7 @@ let[@inline never] try_resize t r new_capacity ~clear = [Resize _] value to indicate unprocessed target buckets. The use of [Sys.opaque_identity] below ensures that a new value is allocated. *) let resize_avoid_aba = - if clear then B (Nil_with_size { size_modifier = Size.used_once }) - else - B - (Resize - { - spine = - Sys.opaque_identity - (Nil_with_size { size_modifier = Size.used_once }); - }) + if clear then B Nil else B (Resize { spine = Sys.opaque_identity Nil }) in let buckets = Atomic_array.make new_capacity resize_avoid_aba in let new_r = @@ -365,6 +363,7 @@ let rec assoc r key = function if nil_r.size_modifier != Size.used_once then Size.update_once r.size nil_r.size_modifier; Nil + | B Nil -> Nil | B (Cons_with_size cons_r) -> if cons_r.size_modifier != Size.used_once then Size.update_once r.size cons_r.size_modifier; @@ -399,10 +398,18 @@ let rec try_add t key value backoff = let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - match Atomic_array.unsafe_fenceless_get r.buckets i with - | B (Nil_with_size nil_r as before) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once r.size nil_r.size_modifier; + let (B old_bucket) = Atomic_array.unsafe_fenceless_get r.buckets i in + begin + (* Make sure size_modifier has been updated. *) + match old_bucket with + | Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ } -> + if size_modifier != Size.used_once then + Size.update_once r.size size_modifier + | _ -> () + end; + + match old_bucket with + | (Nil_with_size _ | Nil) as before -> let (Cons_with_size cons_r as after : ('a, 'b, [ `Cons_with_size ]) tdt) = Cons_with_size { @@ -418,9 +425,7 @@ let rec try_add t key value backoff = cons_r.size_modifier <- Size.used_once; adjust_size t r mask true) else try_add t key value (Backoff.once backoff) - | B (Cons_with_size cons_r as before) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; + | Cons_with_size cons_r as before -> if r.equal cons_r.key key then false else if assoc_node r.equal key cons_r.rest != Nil then false else @@ -428,7 +433,7 @@ let rec try_add t key value backoff = = Cons_with_size { - size_modifier = Size.(new_once r.size incr); + size_modifier = Size.new_once r.size Size.incr; key; value; rest = @@ -443,7 +448,7 @@ let rec try_add t key value backoff = adjust_size t r mask true end else try_add t key value (Backoff.once backoff) - | B (Resize _) -> + | Resize _ -> let _ = finish t (Atomic.get t) in try_add t key value Backoff.default @@ -461,17 +466,24 @@ let rec remove_node t key backoff = let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - match Atomic_array.unsafe_fenceless_get r.buckets i with - | B (Nil_with_size nil_r) -> - if nil_r.size_modifier != Size.used_once then begin - Size.update_once r.size nil_r.size_modifier; - nil_r.size_modifier <- Size.used_once - end; - Nil - | B (Cons_with_size cons_r as before) -> begin - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; - + let (B old_bucket) = Atomic_array.unsafe_fenceless_get r.buckets i in + begin + (* Make sure size_modifier has been updated. *) + match old_bucket with + | Nil_with_size nil_r -> + if nil_r.size_modifier != Size.used_once then begin + Size.update_once r.size nil_r.size_modifier; + nil_r.size_modifier <- Size.used_once + end + | Cons_with_size cons_r -> + if cons_r.size_modifier != Size.used_once then begin + Size.update_once r.size cons_r.size_modifier + end + | _ -> () + end; + match old_bucket with + | Nil_with_size _ | Nil -> Nil + | Cons_with_size cons_r as before -> begin let size_modifier = Size.new_once r.size Size.decr in if r.equal cons_r.key key then let found_node = @@ -526,7 +538,7 @@ let rec remove_node t key backoff = else remove_node t key (Backoff.once backoff) | exception Not_found -> Nil end - | B (Resize _) -> + | Resize _ -> let _ = finish t (Atomic.get t) in remove_node t key Backoff.default @@ -553,7 +565,7 @@ let rec snapshot t ~clear backoff = else loop (i + 1) (match Atomic_array.unsafe_fenceless_get snapshot i with - | B (Resize { spine = Nil_with_size _ }) -> Nil + | B (Resize { spine = Nil_with_size _ | Nil }) -> Nil | B (Resize { spine = Cons_with_size cons_r }) -> Cons { @@ -561,7 +573,7 @@ let rec snapshot t ~clear backoff = value = cons_r.value; rest = cons_r.rest; } - | B (Nil_with_size _ | Cons_with_size _) -> + | B (Nil_with_size _ | Cons_with_size _ | Nil) -> (* After resize only [Resize] values should be left in the old buckets. *) assert false) @@ -578,18 +590,29 @@ let remove_all t = snapshot t ~clear:true Backoff.default (* *) let rec try_find_random_non_empty_bucket size buckets seed i = - match Atomic_array.unsafe_fenceless_get buckets i with - | B (Nil_with_size nil_r) | B (Resize { spine = Nil_with_size nil_r }) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once size nil_r.size_modifier; + let (B old_bucket) = Atomic_array.unsafe_fenceless_get buckets i in + begin + match old_bucket with + | Nil_with_size { size_modifier } + | Cons_with_size { size_modifier; _ } + | Resize { spine = Nil_with_size { size_modifier } } + | Resize { spine = Cons_with_size { size_modifier; _ } } -> + if size_modifier != Size.used_once then + Size.update_once size size_modifier + | _ -> () + end; + + match old_bucket with + | Nil_with_size _ + | Resize { spine = Nil_with_size _ } + | Nil + | Resize { spine = Nil } -> let mask = Atomic_array.length buckets - 1 in let i = (i + 1) land mask in if i <> seed land mask then try_find_random_non_empty_bucket size buckets seed i else Nil - | B (Cons_with_size cons_r) | B (Resize { spine = Cons_with_size cons_r }) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once size cons_r.size_modifier; + | Cons_with_size cons_r | Resize { spine = Cons_with_size cons_r } -> Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } let try_find_random_non_empty_bucket t = From 7ddcfd80536e76c66619eb4201f1a42f0b70cbae Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 24 Oct 2024 19:10:00 +0200 Subject: [PATCH 12/16] Factorize some code in the function adjust_size --- src_lockfree/htbl/htbl.body.ml | 74 ++++++++++++++-------------------- 1 file changed, 31 insertions(+), 43 deletions(-) diff --git a/src_lockfree/htbl/htbl.body.ml b/src_lockfree/htbl/htbl.body.ml index 3e7eb617..7e6ad7b3 100644 --- a/src_lockfree/htbl/htbl.body.ml +++ b/src_lockfree/htbl/htbl.body.ml @@ -327,7 +327,22 @@ let[@inline never] try_resize t r new_capacity ~clear = true end -let adjust_size t r mask result = +let adjust_size t r node mask result = + begin + match node with + | Nil_with_size nil_r -> + if nil_r.size_modifier != Size.used_once then begin + Size.update_once r.size nil_r.size_modifier; + nil_r.size_modifier <- Size.used_once + end + | Cons_with_size cons_r -> + if cons_r.size_modifier != Size.used_once then begin + Size.update_once r.size cons_r.size_modifier; + cons_r.size_modifier <- Size.used_once + end + | _ -> () + end; + if r.pending == Nothing && Int64.to_int (Random.bits64 ()) land mask = 0 @@ -410,7 +425,7 @@ let rec try_add t key value backoff = match old_bucket with | (Nil_with_size _ | Nil) as before -> - let (Cons_with_size cons_r as after : ('a, 'b, [ `Cons_with_size ]) tdt) = + let after = Cons_with_size { size_modifier = Size.new_once r.size Size.incr; @@ -420,17 +435,13 @@ let rec try_add t key value backoff = } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then ( - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - adjust_size t r mask true) + then adjust_size t r after mask true else try_add t key value (Backoff.once backoff) | Cons_with_size cons_r as before -> if r.equal cons_r.key key then false else if assoc_node r.equal key cons_r.rest != Nil then false else - let (Cons_with_size cons_r as after) : ('a, 'b, [ `Cons_with_size ]) tdt - = + let after = Cons_with_size { size_modifier = Size.new_once r.size Size.incr; @@ -442,11 +453,7 @@ let rec try_add t key value backoff = } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then begin - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - adjust_size t r mask true - end + then adjust_size t r after mask true else try_add t key value (Backoff.once backoff) | Resize _ -> let _ = finish t (Atomic.get t) in @@ -470,14 +477,9 @@ let rec remove_node t key backoff = begin (* Make sure size_modifier has been updated. *) match old_bucket with - | Nil_with_size nil_r -> - if nil_r.size_modifier != Size.used_once then begin - Size.update_once r.size nil_r.size_modifier; - nil_r.size_modifier <- Size.used_once - end - | Cons_with_size cons_r -> - if cons_r.size_modifier != Size.used_once then begin - Size.update_once r.size cons_r.size_modifier + | Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ } -> + if size_modifier != Size.used_once then begin + Size.update_once r.size size_modifier end | _ -> () end; @@ -491,22 +493,14 @@ let rec remove_node t key backoff = in match cons_r.rest with | Nil -> - let (Nil_with_size nil_r as after) : - ('a, 'b, [ `Nil_with_size ]) tdt = - Nil_with_size { size_modifier } - in + let after = Nil_with_size { size_modifier } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then begin - Size.update_once r.size nil_r.size_modifier; - nil_r.size_modifier <- Size.used_once; - adjust_size t r mask found_node - end + then adjust_size t r after mask found_node else remove_node t key (Backoff.once backoff) | Cons next -> - let (Cons_with_size cons_r as after) : - ('a, 'b, [ `Cons_with_size ]) tdt = + let after = Cons_with_size { size_modifier; @@ -518,23 +512,17 @@ let rec remove_node t key backoff = if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then begin - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - adjust_size t r mask found_node - end + then adjust_size t r after mask found_node else remove_node t key (Backoff.once backoff) else match dissoc r.equal key cons_r.rest with | (Nil | Cons _) as rest -> + let after = Cons_with_size { cons_r with rest; size_modifier } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B (Cons_with_size { cons_r with rest; size_modifier })) - then begin - Size.update_once r.size cons_r.size_modifier; - cons_r.size_modifier <- Size.used_once; - assoc_node r.equal key cons_r.rest |> adjust_size t r mask - end + (B after) + then + assoc_node r.equal key cons_r.rest |> adjust_size t r after mask else remove_node t key (Backoff.once backoff) | exception Not_found -> Nil end From bc35f12eb8cb533815a0e5fa2ec563b8d833a958 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Fri, 25 Oct 2024 10:29:41 +0200 Subject: [PATCH 13/16] Update following Picos (PR317)[https://github.com/ocaml-multicore/picos/pull/317] --- src_lockfree/htbl/dune | 1 - src_lockfree/htbl/htbl.body.ml | 375 +++++++++++++++++++++++---------- src_lockfree/htbl/htbl_intf.ml | 110 +++++++--- 3 files changed, 348 insertions(+), 138 deletions(-) diff --git a/src_lockfree/htbl/dune b/src_lockfree/htbl/dune index 66f64cdb..5a3dd09e 100644 --- a/src_lockfree/htbl/dune +++ b/src_lockfree/htbl/dune @@ -17,4 +17,3 @@ (cat htbl.head_safe.ml) (echo "# 1 \"htbl.body.ml\"\n") (cat htbl.body.ml))))) - diff --git a/src_lockfree/htbl/htbl.body.ml b/src_lockfree/htbl/htbl.body.ml index 7e6ad7b3..49f684a6 100644 --- a/src_lockfree/htbl/htbl.body.ml +++ b/src_lockfree/htbl/htbl.body.ml @@ -369,42 +369,71 @@ let[@inline] get t = (* *) -let rec assoc_node t key = function - | Nil -> (Nil : (_, _, [< `Nil | `Cons ]) tdt) - | Cons r as cons -> if t r.key key then cons else assoc_node t key r.rest - -let rec assoc r key = function - | B (Nil_with_size nil_r) -> - if nil_r.size_modifier != Size.used_once then - Size.update_once r.size nil_r.size_modifier; - Nil - | B Nil -> Nil +let rec exists t key = function + | Nil -> false + | Cons r -> + let result = t r.key key in + if result then result else exists t key r.rest + +let rec mem r key bucket = + begin + match bucket with + | B (Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) + -> + if size_modifier != Size.used_once then + Size.update_once r.size size_modifier + | _ -> () + end; + + match bucket with + | B (Nil_with_size _ | Nil) -> false | B (Cons_with_size cons_r) -> - if cons_r.size_modifier != Size.used_once then - Size.update_once r.size cons_r.size_modifier; - if r.equal cons_r.key key then - Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } - else assoc_node r.equal key cons_r.rest + let result = r.equal cons_r.key key in + if result then result else exists r.equal key cons_r.rest | B (Resize resize_r) -> (* A resize is in progress. The spine of the resize still holds what was in the bucket before resize reached that bucket. *) - assoc r key (B resize_r.spine) + mem r key (B resize_r.spine) -let find_node t key = +let mem t key = (* Reads can proceed in parallel with writes. *) let r = Atomic.get t in let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - assoc r key @@ Atomic_array.unsafe_fenceless_get r.buckets i -(* *) + mem r key @@ Atomic_array.unsafe_fenceless_get r.buckets i -let find_exn t key = - match find_node t key with +(* *) +let rec assoc t key = function | Nil -> raise_notrace Not_found - | Cons r -> r.value + | Cons r -> if t r.key key then r.value else assoc t key r.rest -let mem t key = find_node t key != Nil +let rec find_exn r key bucket = + begin + match bucket with + | B (Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) + -> + if size_modifier != Size.used_once then + Size.update_once r.size size_modifier + | _ -> () + end; + + match bucket with + | B (Nil_with_size _ | Nil) -> raise_notrace Not_found + | B (Cons_with_size cons_r) -> + if r.equal cons_r.key key then cons_r.value + else assoc r.equal key cons_r.rest + | B (Resize resize_r) -> + (* A resize is in progress. The spine of the resize still holds what was + in the bucket before resize reached that bucket. *) + find_exn r key (B resize_r.spine) + +let find_exn t key = + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + find_exn r key @@ Atomic_array.unsafe_fenceless_get r.buckets i (* *) @@ -439,7 +468,7 @@ let rec try_add t key value backoff = else try_add t key value (Backoff.once backoff) | Cons_with_size cons_r as before -> if r.equal cons_r.key key then false - else if assoc_node r.equal key cons_r.rest != Nil then false + else if exists r.equal key cons_r.rest then false else let after = Cons_with_size @@ -463,79 +492,205 @@ let[@inline] try_add t key value = try_add t key value Backoff.default (* *) -let[@tail_mod_cons] rec dissoc t key = function - | Nil -> raise_notrace Not_found - | Cons r -> - if t key r.key then r.rest else Cons { r with rest = dissoc t key r.rest } +type ('v, _, _) op = + | Compare : ('v, 'v, bool) op + | Exists : ('v, _, bool) op + | Return : ('v, _, 'v) op -let rec remove_node t key backoff = +let rec try_reassoc : + type v c r. (_, v) t -> _ -> c -> v -> (v, c, r) op -> _ -> r = + fun t key present future op backoff -> let r = Atomic.get t in let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - let (B old_bucket) = Atomic_array.unsafe_fenceless_get r.buckets i in + let not_found (type v c r) (op : (v, c, r) op) : r = + match op with + | Compare -> false + | Exists -> false + | Return -> raise_notrace Not_found + in + + let old_bucket : (_, v) bucket = + Atomic_array.unsafe_fenceless_get r.buckets i + in begin (* Make sure size_modifier has been updated. *) match old_bucket with - | Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ } -> + | B (Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) + -> if size_modifier != Size.used_once then begin Size.update_once r.size size_modifier end | _ -> () end; + match old_bucket with - | Nil_with_size _ | Nil -> Nil - | Cons_with_size cons_r as before -> begin - let size_modifier = Size.new_once r.size Size.decr in + | B (Nil | Nil_with_size _) -> not_found op + | B (Cons_with_size cons_r as before) -> begin if r.equal cons_r.key key then - let found_node = - Cons { key = cons_r.key; value = cons_r.value; rest = Nil } + if + match op with + | Exists | Return -> true + | Compare -> cons_r.value == present + then + let after = Cons_with_size { cons_r with value = future } in + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) + then + match op with + | Compare -> true + | Exists -> true + | Return -> cons_r.value + else try_reassoc t key present future op (Backoff.once backoff) + else not_found op + else + let[@tail_mod_cons] rec reassoc : + type v c r. + _ -> _ -> c -> v -> (v, c, r) op -> (_, v, 't) tdt -> (_, v, 't) tdt + = + fun t key present future op -> function + | Nil -> raise_notrace Not_found + | Cons r -> + if t key r.key then + match op with + | Exists | Return -> Cons { r with value = future } + | Compare -> + if r.value == present then Cons { r with value = future } + else raise_notrace Not_found + else Cons { r with rest = reassoc t key present future op r.rest } in - match cons_r.rest with - | Nil -> - let after = Nil_with_size { size_modifier } in + match reassoc r.equal key present future op cons_r.rest with + | rest -> + let after = Cons_with_size { cons_r with rest } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) - then adjust_size t r after mask found_node - else remove_node t key (Backoff.once backoff) - | Cons next -> - let after = - Cons_with_size - { - size_modifier; - key = next.key; - value = next.value; - rest = next.rest; - } + then + match op with + | Compare -> true + | Exists -> true + | Return -> assoc r.equal key cons_r.rest + else try_reassoc t key present future op (Backoff.once backoff) + | exception Not_found -> not_found op + end + | B (Resize _) -> + let _ = finish t (Atomic.get t) in + try_reassoc t key present future op Backoff.default + +let[@inline] try_set t key future = + try_reassoc t key future future Exists Backoff.default + +let[@inline] try_compare_and_set t key present future = + try_reassoc t key present future Compare Backoff.default + +let[@inline] set_exn t key value = + try_reassoc t key key value Return Backoff.default + +(* *) +let rec try_dissoc : type v c r. (_, v) t -> _ -> c -> (v, c, r) op -> _ -> r = + fun t key present op backoff -> + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + let not_found (type v c r) (op : (v, c, r) op) : r = + match op with + | Compare -> false + | Exists -> false + | Return -> raise_notrace Not_found + in + + let old_bucket : (_, v) bucket = + Atomic_array.unsafe_fenceless_get r.buckets i + in + begin + (* Make sure size_modifier has been updated. *) + match old_bucket with + | B (Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) + -> + if size_modifier != Size.used_once then begin + Size.update_once r.size size_modifier + end + | _ -> () + end; + + match old_bucket with + | B (Nil_with_size _ | Nil) -> not_found op + | B (Cons_with_size cons_r as before) -> begin + let size_modifier = Size.new_once r.size Size.decr in + if r.equal cons_r.key key then + if + match op with + | Exists | Return -> true + | Compare -> cons_r.value == present + then + let after = + match cons_r.rest with + | Nil -> Nil_with_size { size_modifier } + | Cons next -> + Cons_with_size + { + size_modifier; + key = next.key; + value = next.value; + rest = next.rest; + } + in + if + Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) + then + let res : r = + match op with + | Compare -> true + | Exists -> true + | Return -> cons_r.value in - if - Atomic_array.unsafe_compare_and_set r.buckets i (B before) - (B after) - then adjust_size t r after mask found_node - else remove_node t key (Backoff.once backoff) + adjust_size t r after mask res + else try_dissoc t key present op (Backoff.once backoff) + else not_found op else - match dissoc r.equal key cons_r.rest with + let[@tail_mod_cons] rec dissoc : + type v c r. + _ -> _ -> c -> (v, c, r) op -> (_, v, 't) tdt -> (_, v, 't) tdt = + fun t key present op -> function + | Nil -> raise_notrace Not_found + | Cons r -> + if t key r.key then + match op with + | Exists | Return -> r.rest + | Compare -> + if r.value == present then r.rest + else raise_notrace Not_found + else Cons { r with rest = dissoc t key present op r.rest } + in + match dissoc r.equal key present op cons_r.rest with | (Nil | Cons _) as rest -> let after = Cons_with_size { cons_r with rest; size_modifier } in if Atomic_array.unsafe_compare_and_set r.buckets i (B before) (B after) then - assoc_node r.equal key cons_r.rest |> adjust_size t r after mask - else remove_node t key (Backoff.once backoff) - | exception Not_found -> Nil + let res : r = + match op with + | Compare -> true + | Exists -> true + | Return -> assoc r.equal key cons_r.rest + in + adjust_size t r after mask res + else try_dissoc t key present op (Backoff.once backoff) + | exception Not_found -> not_found op end - | Resize _ -> + | B (Resize _) -> let _ = finish t (Atomic.get t) in - remove_node t key Backoff.default + try_dissoc t key present op Backoff.default -let try_remove t key = remove_node t key Backoff.default != Nil +let[@inline] try_remove t key = try_dissoc t key key Exists Backoff.default -let remove_exn t key = - match remove_node t key Backoff.default with - | Nil -> raise_notrace Not_found - | Cons r -> r.value +let[@inline] try_compare_and_remove t key present = + try_dissoc t key present Compare Backoff.default + +let[@inline] remove_exn t key = try_dissoc t key key Return Backoff.default (* *) @@ -577,55 +732,57 @@ let remove_all t = snapshot t ~clear:true Backoff.default (* *) -let rec try_find_random_non_empty_bucket size buckets seed i = - let (B old_bucket) = Atomic_array.unsafe_fenceless_get buckets i in - begin - match old_bucket with - | Nil_with_size { size_modifier } - | Cons_with_size { size_modifier; _ } - | Resize { spine = Nil_with_size { size_modifier } } - | Resize { spine = Cons_with_size { size_modifier; _ } } -> - if size_modifier != Size.used_once then - Size.update_once size size_modifier - | _ -> () - end; - - match old_bucket with - | Nil_with_size _ - | Resize { spine = Nil_with_size _ } - | Nil - | Resize { spine = Nil } -> - let mask = Atomic_array.length buckets - 1 in - let i = (i + 1) land mask in - if i <> seed land mask then - try_find_random_non_empty_bucket size buckets seed i - else Nil - | Cons_with_size cons_r | Resize { spine = Cons_with_size cons_r } -> - Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } - -let try_find_random_non_empty_bucket t = - let r = Atomic.get t in - let seed = Int64.to_int (Random.bits64 ()) in - try_find_random_non_empty_bucket r.size r.buckets seed - (seed land (Atomic_array.length r.buckets - 1)) - -let rec length spine n = - match spine with Nil -> n | Cons r -> length r.rest (n + 1) - -let length spine = length spine 0 - -let rec nth spine i = - match spine with - | Nil -> impossible () - | Cons r -> if i <= 0 then r.key else nth r.rest (i - 1) - let find_random_exn t = + let try_find_random_non_empty_bucket t = + let r = Atomic.get t in + let buckets = r.buckets in + let seed = Int64.to_int (Random.bits64 ()) in + let rec try_find_random_non_empty_bucket buckets seed i = + let (B old_bucket) = Atomic_array.unsafe_fenceless_get buckets i in + begin + match old_bucket with + | Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ } + -> + if size_modifier != Size.used_once then + Size.update_once r.size size_modifier + | Resize + { + spine = + ( Nil_with_size { size_modifier } + | Cons_with_size { size_modifier; _ } ); + } -> + if size_modifier != Size.used_once then + Size.update_once r.size size_modifier + | _ -> () + end; + + match old_bucket with + | Nil_with_size _ | Nil | Resize { spine = Nil_with_size _ | Nil } -> + let mask = Atomic_array.length buckets - 1 in + let i = (i + 1) land mask in + if i <> seed land mask then + try_find_random_non_empty_bucket buckets seed i + else Nil + | Cons_with_size cons_r | Resize { spine = Cons_with_size cons_r } -> + Cons { key = cons_r.key; value = cons_r.value; rest = cons_r.rest } + in + try_find_random_non_empty_bucket buckets seed + (seed land (Atomic_array.length buckets - 1)) + in match try_find_random_non_empty_bucket t with | (Cons cons_r as spine : (_, _, [< `Nil | `Cons ]) tdt) -> (* We found a non-empty bucket - the fast way. *) if cons_r.rest == Nil then cons_r.key else - let n = length spine in + let rec length spine n = + match spine with Nil -> n | Cons r -> length r.rest (n + 1) + in + let n = length cons_r.rest 1 in + let rec nth spine i = + match spine with + | Nil -> impossible () + | Cons r -> if i <= 0 then r.key else nth r.rest (i - 1) + in nth spine (Random.int n) | Nil -> (* We couldn't find a non-empty bucket - the slow way. *) diff --git a/src_lockfree/htbl/htbl_intf.ml b/src_lockfree/htbl/htbl_intf.ml index 9381c50f..8ceaded5 100644 --- a/src_lockfree/htbl/htbl_intf.ml +++ b/src_lockfree/htbl/htbl_intf.ml @@ -1,6 +1,12 @@ module type HTBL = sig (** Lock-free hash table. + The operations provided by this hash table are designed to work as building + blocks of non-blocking algorithms. Specifically, the operation signatures + and semantics are designed to allow building + {{:https://dl.acm.org/doi/10.1145/62546.62593} consensus protocols over + arbitrary numbers of processes}. + 🏎ī¸ Single key reads with this hash table are actually wait-free rather than just lock-free. Internal resizing automatically uses all the threads that are trying to write to the hash table. *) @@ -49,39 +55,53 @@ module type HTBL = sig ℹī¸ The returned value may not be the same as given to {!create}. *) val length : ('k, 'v) t -> int - (** [length htbl] returns the number of bindings in the hash table [htbl]. *) + (** [length htbl] returns the number of bindings in the hash table [htbl]. *) (** {2 Looking up bindings} *) val find_exn : ('k, 'v) t -> 'k -> 'v (** [find_exn htbl key] returns the current binding of [key] in the hash table - [htbl] or raises {!Not_found} if no such binding exists. *) + [htbl] or raises {!Not_found} if no such binding exists. + + @raise Not_found in case no binding of [key] exists in the hash table + [htbl]. *) val mem : ('k, 'v) t -> 'k -> bool (** [mem htbl key] determines whether the hash table [htbl] has a binding for the [key]. *) - val to_seq : ('k, 'v) t -> ('k * 'v) Seq.t - (** [to_seq htbl] takes a snapshot of the bindings in the hash table and returns - them as an association sequence. - - 🐌 This is a linear time operation. *) - - val find_random_exn : ('k, 'v) t -> 'k - (** [find_random_exn htbl] tries to find a random binding from the hash table - and returns the key of the binding or raises {!Not_found} in case the hash - table is empty. - - 🐌 This is an expected constant time operation with worst case linear time - complexity. *) - (** {2 Adding bindings} *) val try_add : ('k, 'v) t -> 'k -> 'v -> bool (** [try_add htbl key value] tries to add a new binding of [key] to [value] to - the hash table [htbl]. Returns [true] on success and [false] in case the + the hash table [htbl]. Returns [true] on success and [false] in case the hash table already contained a binding for [key]. *) + (** {2 Updating bindings} *) + + val try_set : ('k, 'v) t -> 'k -> 'v -> bool + (** [try_set htbl key value] tries to update an existing binding of [key] to + [value] in the hash table [htbl]. Returns [true] on success and [false] in + case the hash table did not contain a binding for [key]. *) + + val try_compare_and_set : ('k, 'v) t -> 'k -> 'v -> 'v -> bool + (** [try_compare_and_set htbl key before after] tries to update an existing + binding of [key] from the [before] value to the [after] value in the hash + table [htbl]. Returns [true] on success and [false] in case the hash table + did not contain a binding of [key] to the [before] value. + + ℹī¸ The values are compared using physical equality, i.e. the [==] + operator. *) + + val set_exn : ('k, 'v) t -> 'k -> 'v -> 'v + (** [set_exn htbl key after] tries to update an existing binding of [key] from + some [before] value to the [after] value in the hash table [htbl]. Returns + the [before] value on success or raises {!Not_found} if no such binding + exists. + + @raise Not_found in case no binding of [key] exists in the hash table + [htbl]. *) + (** {2 Removing bindings} *) val try_remove : ('k, 'v) t -> 'k -> bool @@ -89,39 +109,73 @@ module type HTBL = sig [htbl]. Returns [true] on success and [false] in case the hash table did not contain a binding for [key]. *) + val try_compare_and_remove : ('k, 'v) t -> 'k -> 'v -> bool + (** [try_compare_and_remove htbl key before] tries to remove a binding of [key] + to the [before] value from the hash table [htbl]. Returns [true] on success + and [false] in case the hash table did not contain a binding of [key] to the + [before] value. + + ℹī¸ The values are compared using physical equality, i.e. the [==] + operator. *) + val remove_exn : ('k, 'v) t -> 'k -> 'v - (** [remove_exn htbl key] tries to remove a binding of [key] from the hash table - [htbl] and return it or raise {!Not_found} if no such binding exists. *) + (** [remove_exn htbl key] tries to remove a binding of [key] to some [before] + value from the hash table [htbl]. Returns the [before] value on success or + raises {!Not_found} if no such binding exists. + + @raise Not_found in case no binding of [key] exists in the hash table + [htbl]. *) + + (** {2 Examining contents} *) + + val to_seq : ('k, 'v) t -> ('k * 'v) Seq.t + (** [to_seq htbl] takes a snapshot of the bindings in the hash table [htbl] and + returns them as an association sequence. + + 🐌 This is a linear time operation. *) val remove_all : ('k, 'v) t -> ('k * 'v) Seq.t - (** [remove_all htbl] takes a snapshot of the bindings in the hash table, + (** [remove_all htbl] takes a snapshot of the bindings in the hash table [htbl], removes the bindings from the hash table, and returns the snapshot as an association sequence. 🐌 This is a linear time operation. *) + val find_random_exn : ('k, 'v) t -> 'k + (** [find_random_exn htbl] tries to find a random binding from the hash table + [htbl] and returns the key of the binding or raises {!Not_found} in case the + hash table is empty. + + 🐌 This is an expected constant time operation with worst case linear time + complexity. + + @raise Not_found in case the hash table [htbl] is empty. *) + (** {1 Examples} An example top-level session: {[ - # let t : (int, string) Saturn.Htbl.t = - Saturn.Htbl.create + # module Htbl = Saturn_lockfree.Htbl + module Htbl = Saturn_lockfree.Htbl + + # let t : (int, string) Htbl.t = + Htbl.create ~hashed_type:(module Int) () - val t : (int, string) Saturn.Htbl.t = + val t : (int, string) Htbl.t = - # Saturn.Htbl.try_add t 42 "The answer" + # Htbl.try_add t 42 "The answer" - : bool = true - # Saturn.Htbl.try_add t 101 "Basics" + # Htbl.try_add t 101 "Basics" - : bool = true - # Saturn.Htbl.find_exn t 42 + # Htbl.find_exn t 42 - : string = "The answer" - # Saturn.Htbl.try_add t 101 "The basics" + # Htbl.try_add t 101 "The basics" - : bool = false - # Saturn.Htbl.remove_all t |> List.of_seq + # Htbl.remove_all t |> List.of_seq - : (int * string) list = [(101, "Basics"); (42, "The answer")] ]} *) end From ac9a14da05a33161a32218be9db92a2850338a31 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 29 Oct 2024 11:32:35 +0100 Subject: [PATCH 14/16] mdx tests for documentation. --- bench/dune | 2 +- dune-project | 4 ++ saturn.opam | 1 + saturn_lockfree.opam | 1 + src_lockfree/dune | 1 + src_lockfree/htbl/dune | 9 +++ src_lockfree/htbl/htbl.mli | 12 ++++ .../htbl/{htbl_intf.ml => htbl_intf.mli} | 68 ++++++++----------- src_lockfree/htbl/htbl_unsafe.mli | 12 ++++ test/htbl/dune | 2 +- test/htbl/htbls/dune | 2 +- 11 files changed, 71 insertions(+), 43 deletions(-) rename src_lockfree/htbl/{htbl_intf.ml => htbl_intf.mli} (66%) diff --git a/bench/dune b/bench/dune index e1c46552..66c707c8 100644 --- a/bench/dune +++ b/bench/dune @@ -9,7 +9,7 @@ let () = (rule (action - (copy ../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) + (copy ../src_lockfree/htbl/htbl_intf.mli htbl_intf.ml)) (package saturn_lockfree)) (test diff --git a/dune-project b/dune-project index 8ba31ea4..918bc36e 100644 --- a/dune-project +++ b/dune-project @@ -7,6 +7,8 @@ (authors "KC Sivaramakrishnan") (maintainers "Carine Morel" "KC Sivaramakrishnan" "Sudha Parimala") (documentation "https://ocaml-multicore.github.io/saturn/") +(using mdx 0.4) + (package (name saturn) @@ -15,6 +17,7 @@ (ocaml (>= 4.14)) (domain_shims (and (>= 0.1.0) :with-test)) (saturn_lockfree (= :version)) + (mdx (and (>= 0.4) :with-test)) (multicore-magic (and (>= 2.3.0) :with-test)) (multicore-bench (and (>= 0.1.7) :with-test)) (multicore-magic-dscheck (and (>= 2.3.0) :with-test)) @@ -37,6 +40,7 @@ (backoff (>= 0.1.0)) (multicore-magic (>= 2.3.0)) (multicore-magic-dscheck (and (>= 2.3.0) :with-test)) + (mdx (and (>= 0.4) :with-test)) (alcotest (and (>= 1.7.0) :with-test)) (qcheck (and (>= 0.21.3) :with-test)) (qcheck-core (and (>= 0.21.3) :with-test)) diff --git a/saturn.opam b/saturn.opam index 22bb9aae..83d07f6c 100644 --- a/saturn.opam +++ b/saturn.opam @@ -13,6 +13,7 @@ depends: [ "ocaml" {>= "4.14"} "domain_shims" {>= "0.1.0" & with-test} "saturn_lockfree" {= version} + "mdx" {>= "0.4" & with-test} "multicore-magic" {>= "2.3.0" & with-test} "multicore-bench" {>= "0.1.7" & with-test} "multicore-magic-dscheck" {>= "2.3.0" & with-test} diff --git a/saturn_lockfree.opam b/saturn_lockfree.opam index d18f9116..d15c84d5 100644 --- a/saturn_lockfree.opam +++ b/saturn_lockfree.opam @@ -14,6 +14,7 @@ depends: [ "backoff" {>= "0.1.0"} "multicore-magic" {>= "2.3.0"} "multicore-magic-dscheck" {>= "2.3.0" & with-test} + "mdx" {>= "0.4" & with-test} "alcotest" {>= "1.7.0" & with-test} "qcheck" {>= "0.21.3" & with-test} "qcheck-core" {>= "0.21.3" & with-test} diff --git a/src_lockfree/dune b/src_lockfree/dune index 3d9b0187..13efeb68 100644 --- a/src_lockfree/dune +++ b/src_lockfree/dune @@ -13,6 +13,7 @@ let () = (library (name saturn_lockfree) (public_name saturn_lockfree) + (modules_without_implementation htbl_intf) (libraries backoff multicore-magic |} ^ maybe_threads ^ {| )) diff --git a/src_lockfree/htbl/dune b/src_lockfree/htbl/dune index 5a3dd09e..128fbf69 100644 --- a/src_lockfree/htbl/dune +++ b/src_lockfree/htbl/dune @@ -17,3 +17,12 @@ (cat htbl.head_safe.ml) (echo "# 1 \"htbl.body.ml\"\n") (cat htbl.body.ml))))) + +(mdx + (package saturn_lockfree) + (enabled_if + (and + (<> %{os_type} Win32) + (>= %{ocaml_version} 5.1.0))) + (libraries saturn_lockfree) + (files htbl_intf.mli)) diff --git a/src_lockfree/htbl/htbl.mli b/src_lockfree/htbl/htbl.mli index ba768a89..dc6c2330 100644 --- a/src_lockfree/htbl/htbl.mli +++ b/src_lockfree/htbl/htbl.mli @@ -1 +1,13 @@ +(** Lock-free hash table. + + The operations provided by this hash table are designed to work as building + blocks of non-blocking algorithms. Specifically, the operation signatures + and semantics are designed to allow building + {{:https://dl.acm.org/doi/10.1145/62546.62593} consensus protocols over + arbitrary numbers of processes}. + + 🏎ī¸ Single key reads with this hash table are actually wait-free rather than + just lock-free. Internal resizing automatically uses all the threads that + are trying to write to the hash table. *) + include Htbl_intf.HTBL diff --git a/src_lockfree/htbl/htbl_intf.ml b/src_lockfree/htbl/htbl_intf.mli similarity index 66% rename from src_lockfree/htbl/htbl_intf.ml rename to src_lockfree/htbl/htbl_intf.mli index 8ceaded5..b66aa32d 100644 --- a/src_lockfree/htbl/htbl_intf.ml +++ b/src_lockfree/htbl/htbl_intf.mli @@ -1,16 +1,4 @@ module type HTBL = sig - (** Lock-free hash table. - - The operations provided by this hash table are designed to work as building - blocks of non-blocking algorithms. Specifically, the operation signatures - and semantics are designed to allow building - {{:https://dl.acm.org/doi/10.1145/62546.62593} consensus protocols over - arbitrary numbers of processes}. - - 🏎ī¸ Single key reads with this hash table are actually wait-free rather than - just lock-free. Internal resizing automatically uses all the threads that - are trying to write to the hash table. *) - (** {1 API} *) type (!'k, !'v) t @@ -30,12 +18,12 @@ module type HTBL = sig table. - The optional [hashed_type] argument can and usually should be used to - specify the [equal] and [hash] operations on keys. Slow polymorphic + specify the [equal] and [hash] operations on keys. Slow polymorphic equality [(=)] and slow polymorphic {{!Stdlib.Hashtbl.seeded_hash} [seeded_hash (Bits64.to_int (Random.bits64 ()))]} - is used by default. - - The default [min_buckets] is unspecified and a given [min_buckets] may be + are used by default. + - The default [min_buckets] is unspecified, and a given [min_buckets] may be adjusted by the implementation. - - The default [max_buckets] is unspecified and a given [max_buckets] may be + - The default [max_buckets] is unspecified, and a given [max_buckets] may be adjusted by the implementation. *) val hashed_type_of : ('k, 'v) t -> 'k hashed_type @@ -43,16 +31,16 @@ module type HTBL = sig table [htbl] was created. *) val min_buckets_of : ('k, 'v) t -> int - (** [min_buckets_of htbl] returns the minimum number of buckets of the hash + (** [min_buckets_of htbl] returns the minimum number of buckets in the hash table [htbl]. - ℹī¸ The returned value may not be the same as given to {!create}. *) + ℹī¸ The returned value may not be the same as the one given to {!create}. *) val max_buckets_of : ('k, 'v) t -> int - (** [max_buckets_of htbl] returns the maximum number of buckets of the hash + (** [max_buckets_of htbl] returns the maximum number of buckets in the hash table [htbl]. - ℹī¸ The returned value may not be the same as given to {!create}. *) + ℹī¸ The returned value may not be the same as the one given to {!create}. *) val length : ('k, 'v) t -> int (** [length htbl] returns the number of bindings in the hash table [htbl]. *) @@ -63,7 +51,7 @@ module type HTBL = sig (** [find_exn htbl key] returns the current binding of [key] in the hash table [htbl] or raises {!Not_found} if no such binding exists. - @raise Not_found in case no binding of [key] exists in the hash table + @raise Not_found if no binding of [key] exists in the hash table [htbl]. *) val mem : ('k, 'v) t -> 'k -> bool @@ -74,45 +62,45 @@ module type HTBL = sig val try_add : ('k, 'v) t -> 'k -> 'v -> bool (** [try_add htbl key value] tries to add a new binding of [key] to [value] to - the hash table [htbl]. Returns [true] on success and [false] in case the - hash table already contained a binding for [key]. *) + the hash table [htbl]. Returns [true] on success and [false] if the + hash table already contains a binding for [key]. *) (** {2 Updating bindings} *) val try_set : ('k, 'v) t -> 'k -> 'v -> bool (** [try_set htbl key value] tries to update an existing binding of [key] to - [value] in the hash table [htbl]. Returns [true] on success and [false] in - case the hash table did not contain a binding for [key]. *) + [value] in the hash table [htbl]. Returns [true] on success and [false] if + the hash table does not contain a binding for [key]. *) val try_compare_and_set : ('k, 'v) t -> 'k -> 'v -> 'v -> bool (** [try_compare_and_set htbl key before after] tries to update an existing binding of [key] from the [before] value to the [after] value in the hash - table [htbl]. Returns [true] on success and [false] in case the hash table - did not contain a binding of [key] to the [before] value. + table [htbl]. Returns [true] on success and [false] if the hash table + does not contain a binding of [key] to the [before] value. ℹī¸ The values are compared using physical equality, i.e. the [==] operator. *) val set_exn : ('k, 'v) t -> 'k -> 'v -> 'v (** [set_exn htbl key after] tries to update an existing binding of [key] from - some [before] value to the [after] value in the hash table [htbl]. Returns + some [before] value to the [after] value in the hash table [htbl]. Returns the [before] value on success or raises {!Not_found} if no such binding exists. - @raise Not_found in case no binding of [key] exists in the hash table + @raise Not_found if no binding of [key] exists in the hash table [htbl]. *) (** {2 Removing bindings} *) val try_remove : ('k, 'v) t -> 'k -> bool (** [try_remove htbl key] tries to remove a binding of [key] from the hash table - [htbl]. Returns [true] on success and [false] in case the hash table did - not contain a binding for [key]. *) + [htbl]. Returns [true] on success and [false] if the hash table does not + contain a binding for [key]. *) val try_compare_and_remove : ('k, 'v) t -> 'k -> 'v -> bool (** [try_compare_and_remove htbl key before] tries to remove a binding of [key] - to the [before] value from the hash table [htbl]. Returns [true] on success - and [false] in case the hash table did not contain a binding of [key] to the + to the [before] value from the hash table [htbl]. Returns [true] on success + and [false] if the hash table does not contain a binding of [key] to the [before] value. ℹī¸ The values are compared using physical equality, i.e. the [==] @@ -120,10 +108,10 @@ module type HTBL = sig val remove_exn : ('k, 'v) t -> 'k -> 'v (** [remove_exn htbl key] tries to remove a binding of [key] to some [before] - value from the hash table [htbl]. Returns the [before] value on success or + value from the hash table [htbl]. Returns the [before] value on success or raises {!Not_found} if no such binding exists. - @raise Not_found in case no binding of [key] exists in the hash table + @raise Not_found if no binding of [key] exists in the hash table [htbl]. *) (** {2 Examining contents} *) @@ -132,24 +120,24 @@ module type HTBL = sig (** [to_seq htbl] takes a snapshot of the bindings in the hash table [htbl] and returns them as an association sequence. - 🐌 This is a linear time operation. *) + 🐌 This is a linear-time operation. *) val remove_all : ('k, 'v) t -> ('k * 'v) Seq.t (** [remove_all htbl] takes a snapshot of the bindings in the hash table [htbl], removes the bindings from the hash table, and returns the snapshot as an association sequence. - 🐌 This is a linear time operation. *) + 🐌 This is a linear-time operation. *) val find_random_exn : ('k, 'v) t -> 'k (** [find_random_exn htbl] tries to find a random binding from the hash table - [htbl] and returns the key of the binding or raises {!Not_found} in case the + [htbl] and returns the key of the binding or raises {!Not_found} if the hash table is empty. - 🐌 This is an expected constant time operation with worst case linear time + 🐌 This is an expected constant-time operation with worst-case linear-time complexity. - @raise Not_found in case the hash table [htbl] is empty. *) + @raise Not_found if the hash table [htbl] is empty. *) (** {1 Examples} diff --git a/src_lockfree/htbl/htbl_unsafe.mli b/src_lockfree/htbl/htbl_unsafe.mli index ba768a89..dc6c2330 100644 --- a/src_lockfree/htbl/htbl_unsafe.mli +++ b/src_lockfree/htbl/htbl_unsafe.mli @@ -1 +1,13 @@ +(** Lock-free hash table. + + The operations provided by this hash table are designed to work as building + blocks of non-blocking algorithms. Specifically, the operation signatures + and semantics are designed to allow building + {{:https://dl.acm.org/doi/10.1145/62546.62593} consensus protocols over + arbitrary numbers of processes}. + + 🏎ī¸ Single key reads with this hash table are actually wait-free rather than + just lock-free. Internal resizing automatically uses all the threads that + are trying to write to the hash table. *) + include Htbl_intf.HTBL diff --git a/test/htbl/dune b/test/htbl/dune index 8a5a689b..a000a963 100644 --- a/test/htbl/dune +++ b/test/htbl/dune @@ -10,7 +10,7 @@ (rule (action - (copy ../../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) + (copy ../../src_lockfree/htbl/htbl_intf.mli htbl_intf.ml)) (package saturn_lockfree)) (rule diff --git a/test/htbl/htbls/dune b/test/htbl/htbls/dune index 3e1df282..8ecea0e4 100644 --- a/test/htbl/htbls/dune +++ b/test/htbl/htbls/dune @@ -1,6 +1,6 @@ (rule (action - (copy ../../../src_lockfree/htbl/htbl_intf.ml htbl_intf.ml)) + (copy ../../../src_lockfree/htbl/htbl_intf.mli htbl_intf.ml)) (package saturn_lockfree)) (library From 0dd63141c51679483365b65c01e9fe5d20dfa67e Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 30 Oct 2024 16:19:08 +0100 Subject: [PATCH 15/16] Add find_opt. --- src_lockfree/htbl/htbl.body.ml | 50 +++++++++++++++++++++++++++------ src_lockfree/htbl/htbl_intf.mli | 3 ++ 2 files changed, 44 insertions(+), 9 deletions(-) diff --git a/src_lockfree/htbl/htbl.body.ml b/src_lockfree/htbl/htbl.body.ml index 49f684a6..188265c0 100644 --- a/src_lockfree/htbl/htbl.body.ml +++ b/src_lockfree/htbl/htbl.body.ml @@ -404,11 +404,30 @@ let mem t key = mem r key @@ Atomic_array.unsafe_fenceless_get r.buckets i (* *) -let rec assoc t key = function - | Nil -> raise_notrace Not_found - | Cons r -> if t r.key key then r.value else assoc t key r.rest -let rec find_exn r key bucket = +type ('k, 'v, _) poly = + | Value : ('k, 'v, 'v) poly + | Option : ('k, 'v, 'v option) poly + +let rec find_as : + type k v r. (k, v) state -> k -> (k, v) bucket -> (k, v, r) poly -> r = + fun r key bucket poly -> + let rec assoc : + type k v r. + (k -> k -> bool) -> + k -> + (k, v, [ `Nil | `Cons ]) tdt -> + (k, v, r) poly -> + r = + fun eq key node poly -> + match node with + | Nil -> ( + match poly with Value -> raise_notrace Not_found | Option -> None) + | Cons r -> + if eq r.key key then + match poly with Value -> r.value | Option -> Some r.value + else assoc eq key r.rest poly + in begin match bucket with | B (Nil_with_size { size_modifier } | Cons_with_size { size_modifier; _ }) @@ -419,21 +438,30 @@ let rec find_exn r key bucket = end; match bucket with - | B (Nil_with_size _ | Nil) -> raise_notrace Not_found + | B (Nil_with_size _ | Nil) -> ( + match poly with Value -> raise_notrace Not_found | Option -> None) | B (Cons_with_size cons_r) -> - if r.equal cons_r.key key then cons_r.value - else assoc r.equal key cons_r.rest + if r.equal cons_r.key key then + match poly with Value -> cons_r.value | Option -> Some cons_r.value + else assoc r.equal key cons_r.rest poly | B (Resize resize_r) -> (* A resize is in progress. The spine of the resize still holds what was in the bucket before resize reached that bucket. *) - find_exn r key (B resize_r.spine) + find_as r key (B resize_r.spine) poly let find_exn t key = let r = Atomic.get t in let h = r.hash key in let mask = Atomic_array.length r.buckets - 1 in let i = h land mask in - find_exn r key @@ Atomic_array.unsafe_fenceless_get r.buckets i + find_as r key (Atomic_array.unsafe_fenceless_get r.buckets i) Value + +let find_opt t key = + let r = Atomic.get t in + let h = r.hash key in + let mask = Atomic_array.length r.buckets - 1 in + let i = h land mask in + find_as r key (Atomic_array.unsafe_fenceless_get r.buckets i) Option (* *) @@ -497,6 +525,10 @@ type ('v, _, _) op = | Exists : ('v, _, bool) op | Return : ('v, _, 'v) op +let rec assoc eq key = function + | Nil -> raise_notrace Not_found + | Cons r -> if eq r.key key then r.value else assoc eq key r.rest + let rec try_reassoc : type v c r. (_, v) t -> _ -> c -> v -> (v, c, r) op -> _ -> r = fun t key present future op backoff -> diff --git a/src_lockfree/htbl/htbl_intf.mli b/src_lockfree/htbl/htbl_intf.mli index b66aa32d..b40ae8bc 100644 --- a/src_lockfree/htbl/htbl_intf.mli +++ b/src_lockfree/htbl/htbl_intf.mli @@ -46,6 +46,9 @@ module type HTBL = sig (** [length htbl] returns the number of bindings in the hash table [htbl]. *) (** {2 Looking up bindings} *) + val find_opt : ('k, 'v) t -> 'k -> 'v option + (** [find_opt htbl key] returns [Some] of the current binding of [key] in the + hash table [htbl] or [None] if it does not exist. *) val find_exn : ('k, 'v) t -> 'k -> 'v (** [find_exn htbl key] returns the current binding of [key] in the hash table From 522188ef98c35157b463aaacc2aa964a409b1504 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 30 Oct 2024 16:19:29 +0100 Subject: [PATCH 16/16] More functions tested with stm. --- test/htbl/stm_htbl.ml | 142 +++++++++++++++++++++++++++++++++++------- 1 file changed, 118 insertions(+), 24 deletions(-) diff --git a/test/htbl/stm_htbl.ml b/test/htbl/stm_htbl.ml index d425e2ba..0ec646a0 100644 --- a/test/htbl/stm_htbl.ml +++ b/test/htbl/stm_htbl.ml @@ -29,33 +29,48 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct type cmd = | Try_add of int | Mem of int - | Try_remove of int - | To_keys + | Find_opt of int + | Remove_opt of int + (* | To_keys *) | Remove_all | Length + | Set_exn of int + | Try_compare_and_set of int * int + | Try_compare_and_remove of int let show_cmd c = match c with | Try_add x -> "Try_add " ^ string_of_int x | Mem x -> "Mem " ^ string_of_int x - | Try_remove x -> "Try_remove " ^ string_of_int x - | To_keys -> "To_keys" + | Remove_opt x -> "Remove_opt " ^ string_of_int x + (* | To_keys -> "To_keys" *) | Remove_all -> "Remove_all" + | Find_opt x -> "Find_opt " ^ string_of_int x | Length -> "Length" + | Set_exn k -> "Set_exn " ^ string_of_int k + | Try_compare_and_set (k, v) -> + "Try_compare_and_set " ^ string_of_int k ^ " " ^ string_of_int v + | Try_compare_and_remove x -> "Try_compare_and_remove " ^ string_of_int x - module State = Set.Make (Int) + module State = Map.Make (Int) - type state = State.t - type sut = (int, unit) Htbl.t + type state = int State.t + type sut = (int, int) Htbl.t let arb_cmd _s = [ Gen.int_bound 10 |> Gen.map (fun x -> Try_add x); Gen.int_bound 10 |> Gen.map (fun x -> Mem x); - Gen.int_bound 10 |> Gen.map (fun x -> Try_remove x); - Gen.return To_keys; + Gen.int_bound 10 |> Gen.map (fun x -> Remove_opt x); + (* Gen.return To_keys; *) Gen.return Remove_all; + Gen.int_bound 10 |> Gen.map (fun x -> Find_opt x); Gen.return Length; + Gen.(int_bound 10 >>= fun k -> return (Set_exn k)); + Gen.( + int_bound 10 >>= fun k -> + int_bound 10 >>= fun v -> return (Try_compare_and_set (k, v))); + Gen.int_bound 10 |> Gen.map (fun x -> Try_compare_and_remove x); ] |> Gen.oneof |> make ~print:show_cmd @@ -65,41 +80,120 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct let next_state c s = match c with - | Try_add x -> State.add x s + | Try_add x -> if State.mem x s then s else State.add x x s | Mem _ -> s - | Try_remove x -> State.remove x s - | To_keys -> s + | Remove_opt x -> State.remove x s + (* | To_keys -> s *) | Remove_all -> State.empty + | Find_opt _ -> s | Length -> s + | Set_exn k -> if State.mem k s then State.add k (k + 1) s else s + | Try_compare_and_set (k, v) -> ( + match State.find_opt k s with + | Some v' -> if v' = k then State.add k v s else s + | None -> s) + | Try_compare_and_remove k -> ( + match State.find_opt k s with + | Some v -> if k = v then State.remove k s else s + | None -> s) let precond _ _ = true let run c d = match c with - | Try_add x -> Res (bool, Htbl.try_add d x ()) - | Mem x -> + | Try_add x -> Res (bool, Htbl.try_add d x x) + | Mem x -> Res (bool, Htbl.mem d x) + | Remove_opt x -> Res - ( bool, - match Htbl.find_exn d x with - | _ -> true - | exception Not_found -> false ) - | Try_remove x -> Res (bool, Htbl.try_remove d x) - | To_keys -> Res (seq int, Htbl.to_seq d |> Seq.map fst) - | Remove_all -> Res (seq int, Htbl.remove_all d |> Seq.map fst) + ( option int, + match Htbl.remove_exn d x with + | x -> Some x + | exception Not_found -> None ) + (* | To_keys -> + Res + ( list (list int), + Htbl.to_seq d |> List.of_seq |> List.map (fun (a, b) -> [ a; b ]) + ) *) + | Remove_all -> + Res + ( list (list int), + Htbl.remove_all d |> List.of_seq + |> List.map (fun (a, b) -> [ a; b ]) ) | Length -> Res (int, Htbl.length d) + | Find_opt k -> Res (option int, Htbl.find_opt d k) + | Set_exn k -> + Res (result int exn, protect (fun d -> Htbl.set_exn d k (k + 1)) d) + | Try_compare_and_remove k -> Res (bool, Htbl.try_compare_and_remove d k k) + | Try_compare_and_set (k, v) -> + Res (bool, Htbl.try_compare_and_set d k k v) let postcond c (s : state) res = match (c, res) with | Try_add x, Res ((Bool, _), res) -> res <> State.mem x s | Mem x, Res ((Bool, _), res) -> res = State.mem x s - | Try_remove x, Res ((Bool, _), res) -> res = State.mem x s - | To_keys, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s - | Remove_all, Res ((Seq Int, _), res) -> State.equal (State.of_seq res) s + | Remove_opt k, Res ((Option Int, _), res) -> res = State.find_opt k s + | Remove_all, Res ((List (List Int), _), res) -> ( + try + let res : (int * int) list = + List.map (function [ k; v ] -> (k, v) | _ -> raise Exit) res + in + List.sort + (fun (k, _) (k', _) -> Int.compare k k') + (State.bindings s) + = List.sort (fun (k, _) (k', _) -> Int.compare k k') res + with _ -> false) | Length, Res ((Int, _), res) -> res = State.cardinal s + | Find_opt k, Res ((Option Int, _), res) -> State.find_opt k s = res + | Set_exn k, Res ((Result (Int, Exn), _), res) -> begin + match State.find_opt k s with + | Some v -> res = Ok v + | None -> res = Error Not_found + end + | Try_compare_and_remove k, Res ((Bool, _), res) -> ( + match State.find_opt k s with + | Some v' when v' = k -> res = true + | _ -> res = false) + | Try_compare_and_set (k, _), Res ((Bool, _), res) -> ( + match State.find_opt k s with + | Some v' -> v' = k = res + | None -> res = false) | _, _ -> false end let run () = Stm_run.run ~name:"Htbl" (module Spec) |> exit + + (* let test () = + let open Htbl in + let h = create ~hashed_type:(module Int) () in + let t1 = try_add h 1 1 in + let t2 = try Some (set_exn h 1 2) with Not_found -> None in + let t3 = try_add h 1 1 in + let t4 = try Some (set_exn h 1 3) with Not_found -> None in + (t1, t2, t3, t4) + + let test_m () = + let module State = Map.Make (Int) in + let m = State.empty in + let t1 = State.mem 1 m in + let m = State.add 1 1 m in + let t2 = State.find_opt 1 m in + let m = State.add 1 2 m in + let t3 = State.mem 1 m in + let m = if t3 then m else State.add 1 1 m in + let t4 = State.find_opt 1 m in + (t1, t2, t3, t4) + + let run test n = + let count = ref 0 in + let res = ref [] in + let expected = (true, Some 1, false, Some 2) in + for _ = 1 to n do + let r = test () in + if r <> expected then ( + res := r :: !res; + incr count) + done; + (!count, !res) *) end let () =