diff --git a/bench/bench_htbl.ml b/bench/bench_htbl.ml new file mode 100644 index 00000000..5fe3e244 --- /dev/null +++ b/bench/bench_htbl.ml @@ -0,0 +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) ~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 Key) () in + + let n_ops = (100 + percent_mem) * n_ops / 100 in + let n_ops = n_ops * n_domains in + + let n_ops_todo = Countdown.create ~n_domains () in + + let before () = + let _ : _ Seq.t = Htbl.remove_all t in + Countdown.non_atomic_set n_ops_todo n_ops + in + 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 = 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 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 ~before ~init ~work () + |> Times.to_thruput_metrics ~n:n_ops ~singular:"operation" ~config + +let run_suite ~budgetf = + 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 ~unsafe (module Htbl) + in + List.fold_right2 + (fun safe unsafe acc -> safe :: unsafe :: acc) + (run ~unsafe:false (module Saturn_lockfree.Htbl)) + (run ~unsafe:true (module Saturn_lockfree.Htbl_unsafe)) + [] diff --git a/bench/dune b/bench/dune index e9d3db44..66c707c8 100644 --- a/bench/dune +++ b/bench/dune @@ -7,6 +7,11 @@ let () = Jbuild_plugin.V1.send @@ {| +(rule + (action + (copy ../src_lockfree/htbl/htbl_intf.mli 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); ] diff --git a/dune-project b/dune-project index 02e3c7b7..918bc36e 100644 --- a/dune-project +++ b/dune-project @@ -7,16 +7,19 @@ (authors "KC Sivaramakrishnan") (maintainers "Carine Morel" "KC Sivaramakrishnan" "Sudha Parimala") (documentation "https://ocaml-multicore.github.io/saturn/") +(using mdx 0.4) + (package (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)) + (mdx (and (>= 0.4) :with-test)) (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)) @@ -32,11 +35,12 @@ (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)) (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 376fa2cc..83d07f6c 100644 --- a/saturn.opam +++ b/saturn.opam @@ -10,11 +10,12 @@ 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} + "mdx" {>= "0.4" & with-test} "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/saturn_lockfree.opam b/saturn_lockfree.opam index 09bd35e1..d15c84d5 100644 --- a/saturn_lockfree.opam +++ b/saturn_lockfree.opam @@ -9,11 +9,12 @@ 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"} "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/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/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 new file mode 100644 index 00000000..128fbf69 --- /dev/null +++ b/src_lockfree/htbl/dune @@ -0,0 +1,28 @@ +(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))))) + +(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.body.ml b/src_lockfree/htbl/htbl.body.ml new file mode 100644 index 00000000..188265c0 --- /dev/null +++ b/src_lockfree/htbl/htbl.body.ml @@ -0,0 +1,826 @@ +open Htbl_utils + +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 | `Nil ]) 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 | `Nil ]) 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); + 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 = + 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 + | 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 _ | Nil -> () + 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 + | 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 | `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 + 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 _ | Nil -> () + 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 _ | Nil -> () + 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 | `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 { 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 + { + 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 _ | Nil -> () + 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 else B (Resize { spine = Sys.opaque_identity Nil }) + 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 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 + && 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 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) -> + 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. *) + mem r key (B resize_r.spine) + +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 + mem r key @@ Atomic_array.unsafe_fenceless_get r.buckets i + +(* *) + +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; _ }) + -> + if size_modifier != Size.used_once then + Size.update_once r.size size_modifier + | _ -> () + end; + + match bucket with + | 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 + 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_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_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 + +(* *) + +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 + 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 after = + 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 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 exists r.equal key cons_r.rest then false + else + let after = + Cons_with_size + { + size_modifier = Size.new_once r.size 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_size t r after mask true + else try_add t key value (Backoff.once backoff) + | 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 + +(* *) + +type ('v, _, _) op = + | Compare : ('v, 'v, bool) 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 -> + 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 | Nil_with_size _) -> not_found op + | B (Cons_with_size cons_r as before) -> begin + if r.equal cons_r.key key then + 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 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 + 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 + adjust_size t r after mask res + else try_dissoc t key present op (Backoff.once backoff) + else not_found op + else + 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 + 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 + | B (Resize _) -> + let _ = finish t (Atomic.get t) in + try_dissoc t key present op Backoff.default + +let[@inline] try_remove t key = try_dissoc t key key Exists Backoff.default + +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 + +(* *) + +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 }) -> 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 _ | Nil) -> + (* 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 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 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. *) + 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/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.mli b/src_lockfree/htbl/htbl.mli new file mode 100644 index 00000000..dc6c2330 --- /dev/null +++ b/src_lockfree/htbl/htbl.mli @@ -0,0 +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.mli b/src_lockfree/htbl/htbl_intf.mli new file mode 100644 index 00000000..b40ae8bc --- /dev/null +++ b/src_lockfree/htbl/htbl_intf.mli @@ -0,0 +1,172 @@ +module type HTBL = sig + (** {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 ()))]} + 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 + 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 in the hash + table [htbl]. + + ℹī¸ 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 in the hash + table [htbl]. + + ℹī¸ 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]. *) + + (** {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 + [htbl] or raises {!Not_found} if no such binding exists. + + @raise Not_found if 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]. *) + + (** {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] 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] 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] 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 + the [before] value on success or raises {!Not_found} if no such binding + exists. + + @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] 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] 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 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 + raises {!Not_found} if no such binding exists. + + @raise Not_found if 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 [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} if the + hash table is empty. + + 🐌 This is an expected constant-time operation with worst-case linear-time + complexity. + + @raise Not_found if the hash table [htbl] is empty. *) + + (** {1 Examples} + + An example top-level session: + {[ + # 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) Htbl.t = + + # Htbl.try_add t 42 "The answer" + - : bool = true + + # Htbl.try_add t 101 "Basics" + - : bool = true + + # Htbl.find_exn t 42 + - : string = "The answer" + + # Htbl.try_add t 101 "The basics" + - : bool = false + + # Htbl.remove_all t |> List.of_seq + - : (int * string) list = [(101, "Basics"); (42, "The answer")] + ]} *) +end diff --git a/src_lockfree/htbl/htbl_unsafe.mli b/src_lockfree/htbl/htbl_unsafe.mli new file mode 100644 index 00000000..dc6c2330 --- /dev/null +++ b/src_lockfree/htbl/htbl_unsafe.mli @@ -0,0 +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_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/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/dscheck_htbl.ml b/test/htbl/dscheck_htbl.ml new file mode 100644 index 00000000..1088c245 --- /dev/null +++ b/test/htbl/dscheck_htbl.ml @@ -0,0 +1,245 @@ +module Atomic = Dscheck.TracedAtomic + +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 () = + 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 () = + 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 () = + (* 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 + + 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 + + let _two_add_resize2 () = + 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 + + 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 + + let _two_remove () = + let random_offset = Random.int 1000 in + 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)))) + + 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-add-resize" `Slow _two_add_resize; + test_case "2-add-resize2" `Slow _two_add_resize2; + 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 () = + (* 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/dune b/test/htbl/dune new file mode 100644 index 00000000..a000a963 --- /dev/null +++ b/test/htbl/dune @@ -0,0 +1,42 @@ +(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.mli 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) + (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_utils dscheck_htbl size) + (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/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] *)) diff --git a/test/htbl/htbls/dune b/test/htbl/htbls/dune new file mode 100644 index 00000000..8ecea0e4 --- /dev/null +++ b/test/htbl/htbls/dune @@ -0,0 +1,8 @@ +(rule + (action + (copy ../../../src_lockfree/htbl/htbl_intf.mli 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..0ec646a0 --- /dev/null +++ b/test/htbl/stm_htbl.ml @@ -0,0 +1,208 @@ +open QCheck +open STM + +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 + + let hash = Fun.id + end + + module Spec = struct + type cmd = + | Try_add of int + | Mem of int + | 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 + | 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 = Map.Make (Int) + + 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 -> 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 + + 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 -> if State.mem x s then s else State.add x x s + | Mem _ -> 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 x) + | Mem x -> Res (bool, Htbl.mem d x) + | Remove_opt x -> + Res + ( 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 + | 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 () = + (* 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