From c2adcc8d4d470f6a5391b8f4d686f0249bf0d292 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 16 Nov 2023 15:30:17 +0200 Subject: [PATCH] Work around OCaml 5's `Atomic` issues --- src_lockfree/fixed_atomic.ml | 24 ++++++++++++++++++++++++ src_lockfree/size.ml | 2 ++ src_lockfree/skiplist.ml | 2 ++ test/skiplist/dune | 3 ++- 4 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 src_lockfree/fixed_atomic.ml diff --git a/src_lockfree/fixed_atomic.ml b/src_lockfree/fixed_atomic.ml new file mode 100644 index 00000000..094fc851 --- /dev/null +++ b/src_lockfree/fixed_atomic.ml @@ -0,0 +1,24 @@ +(** This "fixes" [Atomic] of OCaml 5 in two ways: + + * [Atomic.get] is incorrectly subject to CSE optimization in OCaml 5. + + * OCaml 5 generates inefficient accesses of ['a Atomic.t array]s assuming + that the array might be a double array. *) + +include Atomic + +type 'a t = private 'a ref + +open struct + external as_atomic : 'a t -> 'a Atomic.t = "%identity" + external of_atomic : 'a Atomic.t -> 'a t = "%identity" +end + +let[@inline] make x = of_atomic (make x) +let[@inline] get x = get (Sys.opaque_identity (as_atomic x)) +let[@inline] compare_and_set x b a = compare_and_set (as_atomic x) b a +let[@inline] exchange x v = exchange (as_atomic x) v +let[@inline] set x v = set (as_atomic x) v +let[@inline] fetch_and_add x v = fetch_and_add (as_atomic x) v +let[@inline] incr x = incr (as_atomic x) +let[@inline] decr x = decr (as_atomic x) diff --git a/src_lockfree/size.ml b/src_lockfree/size.ml index 7d43421c..f77ed53c 100644 --- a/src_lockfree/size.ml +++ b/src_lockfree/size.ml @@ -1,3 +1,5 @@ +module Atomic = Fixed_atomic + module Snapshot = struct type t = int Atomic.t array diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml index ef806e43..80c33e6c 100644 --- a/src_lockfree/skiplist.ml +++ b/src_lockfree/skiplist.ml @@ -28,6 +28,8 @@ (* TODO: Grow and possibly shrink the skiplist or e.g. adjust search and node generation based on the dynamic number of bindings. *) +module Atomic = Fixed_atomic + (* OCaml doesn't allow us to use one of the unused (always 0) bits in pointers for the marks and an indirection is needed. This representation avoids the indirection except for marked references in nodes to be removed. A GADT with diff --git a/test/skiplist/dune b/test/skiplist/dune index a9bad777..10b80d22 100644 --- a/test/skiplist/dune +++ b/test/skiplist/dune @@ -1,13 +1,14 @@ (rule (progn (copy ../../src_lockfree/skiplist.ml skiplist.ml) + (copy ../../src_lockfree/fixed_atomic.ml fixed_atomic.ml) (copy ../../src_lockfree/bits.ml bits.ml) (copy ../../src_lockfree/size.ml size.ml))) (test (name skiplist_dscheck) (libraries atomic dscheck alcotest multicore-magic) - (modules skiplist size bits skiplist_dscheck)) + (modules skiplist size bits fixed_atomic skiplist_dscheck)) (test (name qcheck_skiplist)