From bb5ec1ab62292668c6c225d8874394012be95663 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Tue, 25 Jul 2023 18:18:39 +0300 Subject: [PATCH] Remove the `Op` API --- README.md | 100 +++------------------- bench/bench_op.ml | 44 ---------- bench/main.ml | 1 - src/kcas/kcas.ml | 61 +------------- src/kcas/kcas.mli | 121 +++------------------------ test/kcas/dune | 2 +- test/kcas/example.ml | 14 ---- test/kcas/test.ml | 134 +++++++++++++----------------- test/kcas/test_overlapping_loc.ml | 57 ------------- 9 files changed, 86 insertions(+), 448 deletions(-) delete mode 100644 bench/bench_op.ml delete mode 100644 test/kcas/example.ml delete mode 100644 test/kcas/test_overlapping_loc.ml diff --git a/README.md b/README.md index 09e78914..a5578db5 100644 --- a/README.md +++ b/README.md @@ -120,21 +120,17 @@ val x : int Loc.t = One can then manipulate the locations individually: ```ocaml -# Loc.set a 6 +# Loc.set a 10 - : unit = () # Loc.get a -- : int = 6 -``` - -Attempt primitive operations over multiple locations: +- : int = 10 -```ocaml -# Op.atomically [ - Op.make_cas a 6 10; - Op.make_cas b 0 52 - ] +# Loc.compare_and_set b 0 52 - : bool = true + +# Loc.get b +- : int = 52 ``` Block waiting for changes to locations: @@ -170,16 +166,12 @@ And now we have it: The API of **Kcas** is divided into submodules. The main modules are - [`Loc`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Loc/index.html), - providing an abstraction of _shared memory locations_, + providing an abstraction of _shared memory locations_, and - [`Xt`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Xt/index.html), - providing _explicit transaction log passing_ over shared memory locations, and - -- [`Op`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html), - providing an interface for _primitive operations_ over multiple shared memory - locations. + providing _explicit transaction log passing_ over shared memory locations. -The following sections discuss each of the above in turn. +The following sections discuss both of the above in turn. ### Creating and manipulating individual shared memory locations @@ -192,9 +184,7 @@ In other words, an application that uses [`Atomic`](https://v2.ocaml.org/api/Atomic.html), but then needs to perform atomic operations over multiple atomic locations, could theoretically just rebind `module Atomic = Loc` and then use the -[`Op`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html), -and/or -[`Xt`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Xt/index.html) APIs +[`Xt`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Xt/index.html) API to perform operations over multiple locations. This should not be done just-in-case, however, as, even though **Kcas** is efficient, it does naturally have higher overhead than the Stdlib @@ -449,10 +439,8 @@ val a_queue : int queue = {front = ; back = } #### Composing transactions -The main benefit of the +The main feature of the [`Xt`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Xt/index.html) API -over the -[`Op`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html) API is that transactions are composable. In fact, we already wrote transactions that recorded multiple primitive shared memory accesses to the explicitly passed transaction log. Nothing prevents us from writing transactions calling other @@ -1049,72 +1037,6 @@ val a_cache : (int, string) cache = As an exercise, implement an operation to `remove` associations from a cache and an operation to change the capacity of the cache. -### Programming with primitive operations - -In addition to the transactional interface, **Kcas** also provides the -[`Op`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html) -interface for performing a list of primitive operations. To program with -primitive operations one simply makes a list of CAS operations using -[`make_cas`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html#val-make_cas) -and then attempts them using -[`atomically`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html#val-atomically). -Typically that needs to be done inside a loop of some kind as such an attempt -can naturally fail. - -Let's first -[`make`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Loc/index.html#val-make) -two locations representing stacks: - -```ocaml -# let stack_a = Loc.make [19] - and stack_b = Loc.make [76] -val stack_a : int list Loc.t = -val stack_b : int list Loc.t = -``` - -Here is a function that can atomically move an element from given `source` stack -to the given `target` stack: - -```ocaml -# let rec move ?(backoff = Backoff.default) - source - target = - match Loc.get source with - | [] -> raise Exit - | (elem::rest) as old_source -> - let old_target = Loc.get target in - let ops = [ - Op.make_cas source old_source rest; - Op.make_cas target old_target (elem::old_target) - ] in - if not (Op.atomically ops) then - let backoff = Backoff.once backoff in - move ~backoff source target -val move : ?backoff:Backoff.t -> 'a list Loc.t -> 'a list Loc.t -> unit = - -``` - -Note that we also used the -[`Backoff`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Backoff/index.html) -module provided by **Kcas** above. - -Now we can simply call `move`: - -```ocaml -# move stack_a stack_b -- : unit = () - -# Loc.get stack_a -- : int list = [] - -# Loc.get stack_b -- : int list = [19; 76] -``` - -As one can see, the API provided by -[`Op`](https://ocaml-multicore.github.io/kcas/doc/kcas/Kcas/Op/index.html) is -quite low-level and is not intended for application level programming. - ## Designing lock-free algorithms with k-CAS The key benefit of k-CAS, or k-CAS-n-CMP, and transactions in particular, is diff --git a/bench/bench_op.ml b/bench/bench_op.ml deleted file mode 100644 index 73282c97..00000000 --- a/bench/bench_op.ml +++ /dev/null @@ -1,44 +0,0 @@ -open Kcas -open Bench - -let run_one ?(n_locs = 2) ?(factor = 1) - ?(n_iter = 10 * factor * Util.iter_factor) () = - let locs = Loc.make_array n_locs 0 in - - let to_1 = - locs |> Array.map (fun loc -> Op.make_cas loc 0 1) |> Array.to_list - in - let to_0 = - locs |> Array.map (fun loc -> Op.make_cas loc 1 0) |> Array.to_list - in - - let init _ = () in - let work _ () = - let rec loop i = - if i > 0 then begin - Op.atomically to_1 |> ignore; - Op.atomically to_0 |> ignore; - loop (i - 2) - end - in - loop n_iter - in - - let times = Times.record ~n_domains:1 ~init ~work () in - - let name metric = Printf.sprintf "%s/%d loc op" metric n_locs in - - List.concat - [ - Stats.of_times times - |> Stats.scale (1_000_000_000.0 /. Float.of_int n_iter) - |> Stats.to_json ~name:(name "time per op") - ~description:"Time to perform a single op" ~units:"ns"; - Times.invert times |> Stats.of_times - |> Stats.scale (Float.of_int n_iter /. 1_000_000.0) - |> Stats.to_json ~name:(name "ops over time") - ~description:"Number of operations performed over time" ~units:"M/s"; - ] - -let run_suite ~factor = - [ 1; 2; 4; 8 ] |> List.concat_map @@ fun n_locs -> run_one ~n_locs ~factor () diff --git a/bench/main.ml b/bench/main.ml index eee7685a..748d4fd5 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -1,6 +1,5 @@ let benchmarks = [ - ("Kcas Op", Bench_op.run_suite); ("Kcas Xt", Bench_xt.run_suite); ("Kcas parallel CMP", Bench_parallel_cmp.run_suite); ("Kcas_data Hashtbl", Bench_hashtbl.run_suite); diff --git a/src/kcas/kcas.ml b/src/kcas/kcas.ml index e73f2a70..b8eb2787 100644 --- a/src/kcas/kcas.ml +++ b/src/kcas/kcas.ml @@ -348,7 +348,6 @@ let[@inline] determine_for_owner casn cass = fenceless_get casn == After let[@inline never] impossible () = failwith "impossible" -let[@inline never] overlap () = failwith "kcas: location overlap" let[@inline never] invalid_retry () = failwith "kcas: invalid use of retry" type splay = Miss : splay | Hit : 'a loc * 'a state -> splay @@ -615,63 +614,6 @@ module Loc = struct let fenceless_get loc = eval (fenceless_get (as_atomic loc)) end -let[@inline] insert cass loc state = - let x = loc.id in - match cass with - | CASN { loc = a; lt = NIL; _ } when x < a.id -> - CASN { loc; state; lt = NIL; gt = cass; awaiters = [] } - | CASN { loc = a; gt = NIL; _ } when a.id < x -> - CASN { loc; state; lt = cass; gt = NIL; awaiters = [] } - | _ -> begin - match splay ~hit_parent:false x cass with - | _, Hit _, _ -> overlap () - | lt, Miss, gt -> CASN { loc; state; lt; gt; awaiters = [] } - end - -module Op = struct - type t = CAS : 'a Loc.t * 'a * 'a -> t - - let[@inline] make_cas loc before after = CAS (loc, before, after) - let[@inline] make_cmp loc expected = CAS (loc, expected, expected) - - let[@inline] is_on_loc op loc = - match op with CAS (loc', _, _) -> Obj.magic loc' == loc - - let[@inline] get_id = function CAS (loc, _, _) -> loc.id - - let atomic = function - | CAS (loc, before, after) -> - if before == after then Loc.get loc == before - else Loc.compare_and_set loc before after - - let atomically ?(mode = Mode.lock_free) = function - | [] -> true - | [ op ] -> atomic op - | first :: rest -> - let casn = Atomic.make (mode :> status) in - let rec run cass = function - | [] -> determine_for_owner casn cass - | CAS (loc, before, after) :: rest -> - if before == after && is_obstruction_free casn loc then - (* Fenceless is safe as there are fences in [determine]. *) - let state = fenceless_get (as_atomic loc) in - before == eval state && run (insert cass loc state) rest - else - run - (insert cass loc { before; after; casn; awaiters = [] }) - rest - in - let (CAS (loc, before, after)) = first in - if before == after && is_obstruction_free casn loc then - (* Fenceless is safe as there are fences in [determine]. *) - let state = fenceless_get (as_atomic loc) in - before == eval state - && run (CASN { loc; state; lt = NIL; gt = NIL; awaiters = [] }) rest - else - let state = { before; after; casn; awaiters = [] } in - run (CASN { loc; state; lt = NIL; gt = NIL; awaiters = [] }) rest -end - module Xt = struct (* NOTE: You can adjust comment blocks below to select whether or not to use an unsafe cast to avoid a level of indirection due to [Atomic.t]. *) @@ -791,6 +733,9 @@ module Xt = struct unsafe_update ~xt loc (fun actual -> if actual == before then after else actual) + let compare_and_set ~xt loc before after = + compare_and_swap ~xt loc before after == before + let exchange ~xt loc after = unsafe_update ~xt loc (fun _ -> after) let fetch_and_add ~xt loc n = unsafe_update ~xt loc (( + ) n) let incr ~xt loc = unsafe_update ~xt loc inc |> ignore diff --git a/src/kcas/kcas.mli b/src/kcas/kcas.mli index bc7708e4..a1268413 100644 --- a/src/kcas/kcas.mli +++ b/src/kcas/kcas.mli @@ -53,21 +53,17 @@ One can then manipulate the locations individually: {[ - # Loc.set a 6 + # Loc.set a 10 - : unit = () # Loc.get a - - : int = 6 - ]} - - Attempt primitive operations over multiple locations: + - : int = 10 - {[ - # Op.atomically [ - Op.make_cas a 6 10; - Op.make_cas b 0 52 - ] + # Loc.compare_and_set b 0 52 - : bool = true + + # Loc.get b + - : int = 52 ]} Block waiting for changes to locations: @@ -284,12 +280,8 @@ end (** {1 Manipulating multiple locations atomically} - Multiple shared memory locations can be manipulated atomically using either - - - the {!Xt} module, to explicitly pass a transaction log to record accesses, - or - - - the {!Op} module, to specify a list of primitive operations to perform. + Multiple shared memory locations can be manipulated atomically using the + {!Xt} module to explicitly pass a transaction log to record accesses. Atomic operations over multiple shared memory locations are performed in two or three phases: @@ -441,6 +433,10 @@ module Xt : sig val swap : xt:'x t -> 'a Loc.t -> 'a Loc.t -> unit (** [swap ~xt l1 l2] is equivalent to [set ~xt l1 @@ exchange ~xt l2 @@ get ~xt l1]. *) + val compare_and_set : xt:'x t -> 'a Loc.t -> 'a -> 'a -> bool + (** [compare_and_set ~xt r before after] is equivalent to + [compare_and_swap ~xt r before after == before]. *) + val compare_and_swap : xt:'x t -> 'a Loc.t -> 'a -> 'a -> 'a (** [compare_and_swap ~xt r before after] is equivalent to @@ -563,96 +559,3 @@ module Xt : sig (** [unsafe_update ~xt r f] is equivalent to [update ~xt r f], but does not assert against misuse. *) end - -(** Multi-word compare-and-set operations on shared memory locations. - - This module provides a multi-word compare-and-set (MCAS) interface for - manipulating multiple locations atomically. This is a low-level interface - not intended for most users. - - As an example, consider an implementation of doubly-linked circular - lists. Instead of using a mutable field, [ref], or [Atomic.t], one would use - a shared memory location, or {!Loc.t}, for the pointers in the node type: - - {[ - type 'a node = { - succ: 'a node Loc.t; - pred: 'a node Loc.t; - datum: 'a; - } - ]} - - To remove a node safely one wants to atomically update the [succ] and [pred] - pointers of the predecessor and successor nodes and to also update the - [succ] and [pred] pointers of a node to point to the node itself, so that - removal becomes an {{:https://en.wikipedia.org/wiki/Idempotence} idempotent} - operation. Using a multi-word compare-and-set one could implement the - [remove] operation as follows: - - {[ - let rec remove ?(backoff = Backoff.default) node = - (* Read pointer to the predecessor node and... *) - let pred = Loc.get node.pred in - (* ..check whether the node has already been removed. *) - if pred != node then - let succ = Loc.get node.succ in - let ok = Op.atomically [ - (* Update pointers in this node: *) - Op.make_cas node.succ succ node; - Op.make_cas node.pred pred node; - (* Update pointers to this node: *) - Op.make_cas pred.succ node succ; - Op.make_cas succ.pred node pred; - ] in - if not ok then - (* Someone modified the list around us, so backoff and retry. *) - remove ~backoff:(Backoff.once backoff) node - ]} - - The list given to {!Op.atomically} contains specifications of the individual - compare-and-set operations to perform. A single {!Op.make_cas} specifies an - operation to compare the current value of a location with the expected value - and, in case they are the same, set the value of the location to the desired - value. - - Programming with like this is similar to programming with single-word - compare-and-set except that the operation is extended to being able to work - on multiple words. *) -module Op : sig - type t - (** Type of operations on shared memory locations. *) - - val make_cas : 'a Loc.t -> 'a -> 'a -> t - (** [make_cas r before after] specifies an operation that attempts to set the - shared memory location [r] to the [after] value and succeeds if the - current content of [r] is the [before] value. *) - - val make_cmp : 'a Loc.t -> 'a -> t - (** [make_cmp r expected] specifies an operation that succeeds if the current - value of the shared memory location [r] is the [expected] value. *) - - val get_id : t -> int - (** [get_id op] returns the unique id of the shared memory reference targeted - by the [op]eration. *) - - val is_on_loc : t -> 'a Loc.t -> bool - (** [is_on_loc op r] determines whether the target of [op] is the shared - memory location [r]. *) - - val atomic : t -> bool - (** [atomic op] attempts to perform the specified operation atomically. - Returns [true] on success and [false] on failure. *) - - val atomically : ?mode:Mode.t -> t list -> bool - (** [atomically ops] attempts to perform the specified operations atomically. - If used in {!Mode.obstruction_free} may raise {!Mode.Interference}. - Otherwise returns [true] on success and [false] on failure. The default - for [atomically] is {!Mode.lock_free}. - - The algorithm requires provided operations to follow a global total order. - To eliminate a class of bugs, the operations are sorted automatically. If - the operations are given in either ascending or descending order of the - targeted shared memory location ids, then sorting is done in linear time - [O(n)] and does not increase the time complexity of the algorithm. - Otherwise sorting may take linearithmic time [O(n*log(n))]. *) -end diff --git a/test/kcas/dune b/test/kcas/dune index 147c9b47..e78098c1 100644 --- a/test/kcas/dune +++ b/test/kcas/dune @@ -1,5 +1,5 @@ (tests - (names test test_overlapping_loc ms_queue_test example threads loc_modes) + (names test ms_queue_test threads loc_modes) (libraries alcotest kcas diff --git a/test/kcas/example.ml b/test/kcas/example.ml deleted file mode 100644 index 80786bf3..00000000 --- a/test/kcas/example.ml +++ /dev/null @@ -1,14 +0,0 @@ -(* construct atomic variables *) -let atomic_1, atomic_2 = (Kcas.Loc.make 0, Kcas.Loc.make 3) in - -(* construct kcas operation *) -let kcas = [ Kcas.Op.make_cas atomic_1 0 1; Kcas.Op.make_cas atomic_2 3 4 ] in - -(* apply constructed kcas *) -ignore (Kcas.Op.atomically kcas); - -(* atomic_1 = 1, atomic_2 = 4 *) -assert (Kcas.Loc.get atomic_1 = 1); -assert (Kcas.Loc.get atomic_2 = 4); - -Printf.printf "Example OK!\n%!" diff --git a/test/kcas/test.ml b/test/kcas/test.ml index 5830bfeb..3cee2698 100644 --- a/test/kcas/test.ml +++ b/test/kcas/test.ml @@ -48,23 +48,26 @@ let test_non_linearizable () = let a = Loc.make 0 and b = Loc.make 0 in - let cass1a = [ Op.make_cmp b 0; Op.make_cas a 0 1 ] - and cass1b = [ Op.make_cmp b 0; Op.make_cas a 1 0 ] - and cass2a = [ Op.make_cas b 0 1; Op.make_cmp a 0 ] - and cass2b = [ Op.make_cas b 1 0; Op.make_cmp a 0 ] in - - let atomically cs = - if Random.bool () then - try Op.atomically ~mode:Mode.obstruction_free cs - with Mode.Interference -> false - else Op.atomically cs + let cass1a ~xt = + (Xt.get ~xt b == 0 && Xt.compare_and_set ~xt a 0 1) || Retry.invalid () + and cass1b ~xt = + (Xt.get ~xt b == 0 && Xt.compare_and_set ~xt a 1 0) || Retry.invalid () + and cass2a ~xt = + (Xt.compare_and_set ~xt b 0 1 && Xt.get ~xt a == 0) || Retry.invalid () + and cass2b ~xt = + (Xt.compare_and_set ~xt b 1 0 && Xt.get ~xt a == 0) || Retry.invalid () + in + + let atomically tx = + if Random.bool () then Xt.commit ~mode:Mode.obstruction_free tx + else Xt.commit tx in let thread1 () = Barrier.await barrier; while not !test_finished do - if atomically cass1a then - while not (atomically cass1b) do + if atomically { tx = cass1a } then + while not (atomically { tx = cass1b }) do if is_single then Domain.cpu_relax (); assert (Loc.get a == 1 && Loc.get b == 0) done @@ -73,8 +76,8 @@ let test_non_linearizable () = and thread2 () = Barrier.await barrier; for _ = 1 to n_iter do - if atomically cass2a then - while not (atomically cass2b) do + if atomically { tx = cass2a } then + while not (atomically { tx = cass2b }) do if is_single then Domain.cpu_relax (); assert (Loc.get a == 0 && Loc.get b == 1) done @@ -95,7 +98,7 @@ let test_set () = (* *) -let test_casn () = +let test_no_skew () = let barrier = Barrier.make 3 in let test_finished = Atomic.make false in @@ -103,8 +106,12 @@ let test_casn () = let a2 = Loc.make 0 in let thread1 () = - let c1 = [ Op.make_cas a1 0 1; Op.make_cas a2 0 1 ] in - let c2 = [ Op.make_cas a1 1 0; Op.make_cas a2 1 0 ] in + let c1 ~xt = + Xt.compare_and_set ~xt a1 0 1 && Xt.compare_and_set ~xt a2 0 1 + in + let c2 ~xt = + Xt.compare_and_set ~xt a1 1 0 && Xt.compare_and_set ~xt a2 1 0 + in Barrier.await barrier; @@ -112,38 +119,38 @@ let test_casn () = assert_kcas a1 0; assert_kcas a2 0; - let out1 = Op.atomically c1 in + let out1 = Xt.commit { tx = c1 } in assert out1; assert_kcas a1 1; assert_kcas a2 1; - let out2 = Op.atomically c2 in + let out2 = Xt.commit { tx = c2 } in assert out2 done; Atomic.set test_finished true and thread2 () = - let c1 = [ Op.make_cas a1 1 0; Op.make_cas a2 0 1 ] in - let c2 = [ Op.make_cas a1 0 1; Op.make_cas a2 1 0 ] in + let c1 ~xt = Xt.get ~xt a1 == 0 && Xt.get ~xt a2 == 1 in + let c2 ~xt = Xt.get ~xt a2 == 1 && Xt.get ~xt a2 == 0 in Barrier.await barrier; while not (Atomic.get test_finished) do - let out1 = Op.atomically c1 in - let out2 = Op.atomically c2 in + let out1 = Xt.commit { tx = c1 } in + let out2 = Xt.commit { tx = c2 } in assert (not out1); assert (not out2); if is_single then Domain.cpu_relax () done and thread3 () = - let c1 = [ Op.make_cas a1 0 1; Op.make_cas a2 1 0 ] in - let c2 = [ Op.make_cas a1 1 0; Op.make_cas a2 0 1 ] in + let c1 ~xt = Xt.get ~xt a1 == 1 && Xt.get ~xt a2 == 0 in + let c2 ~xt = Xt.get ~xt a2 == 0 && Xt.get ~xt a2 == 1 in Barrier.await barrier; while not (Atomic.get test_finished) do - let out1 = Op.atomically c1 in - let out2 = Op.atomically c2 in + let out1 = Xt.commit { tx = c1 } in + let out2 = Xt.commit { tx = c2 } in assert (not out1); assert (not out2); if is_single then Domain.cpu_relax () @@ -154,7 +161,7 @@ let test_casn () = (* *) -let test_read_casn () = +let test_get_seq () = let barrier = Barrier.make 4 in let test_finished = Atomic.make false in @@ -163,9 +170,12 @@ let test_read_casn () = let mutator () = Barrier.await barrier; - for i = 0 to nb_iter do - let c = [ Op.make_cas a1 i (i + 1); Op.make_cas a2 i (i + 1) ] in - assert (Op.atomically c) + for _ = 0 to nb_iter do + let tx ~xt = + Xt.incr ~xt a1; + Xt.incr ~xt a2 + in + Xt.commit { tx } done; Atomic.set test_finished true and getter () = @@ -212,23 +222,27 @@ let test_stress n nb_loop = if n > 0 then loop (n - 1) (Loc.make 0 :: out) else out in loop n [] - and make_kcas0 r_l = - let rec loop r_l out = - match r_l with h :: t -> loop t (Op.make_cas h 0 1 :: out) | [] -> out + and make_kcas0 ~xt r_l = + let rec loop ~xt r_l = + match r_l with + | h :: t -> Xt.compare_and_set ~xt h 0 1 && loop ~xt t + | [] -> true in - loop r_l [] - and make_kcas1 r_l = - let rec loop r_l out = - match r_l with h :: t -> loop t (Op.make_cas h 1 0 :: out) | [] -> out + loop ~xt r_l + and make_kcas1 ~xt r_l = + let rec loop ~xt r_l = + match r_l with + | h :: t -> Xt.compare_and_set ~xt h 1 0 && loop ~xt t + | [] -> true in - loop r_l [] + loop ~xt r_l in let r_l = make_loc n in - let kcas0 = make_kcas0 r_l in - let kcas1 = make_kcas1 r_l in + let kcas0 ~xt = make_kcas0 ~xt r_l in + let kcas1 ~xt = make_kcas1 ~xt r_l in for _ = 1 to nb_loop do - assert (Op.atomically kcas0); - assert (Op.atomically kcas1) + assert (Xt.commit { tx = kcas0 }); + assert (Xt.commit { tx = kcas1 }) done (* *) @@ -244,35 +258,6 @@ let in_place_shuffle array = array.(j) <- t done -let test_presort () = - let n_incs = 10 * Util.iter_factor and n_domains = 3 and n_locs = 5 in - - let barrier = Barrier.make n_domains in - - let locs = Array.init n_locs (fun _ -> Loc.make 0) in - - let mk_inc locs = - in_place_shuffle locs; - let x = Loc.get locs.(0) in - let y = x + 1 in - Array.fold_left (fun cs r -> Op.make_cas r x y :: cs) [] locs - in - - let thread () = - let locs = Array.copy locs in - Random.self_init (); - Barrier.await barrier; - for _ = 1 to n_incs do - while not (Op.atomically (mk_inc locs)) do - Domain.cpu_relax () - done - done - in - - run_domains (List.init n_domains (Fun.const thread)); - - locs |> Array.iter (fun r -> assert (Loc.get r = n_incs * n_domains)) - (* *) let test_presort_and_is_in_log_xt () = @@ -650,14 +635,13 @@ let () = ( "non linearizable", [ Alcotest.test_case "" `Quick test_non_linearizable ] ); ("set", [ Alcotest.test_case "" `Quick test_set ]); - ("casn", [ Alcotest.test_case "" `Quick test_casn ]); - ("read casn", [ Alcotest.test_case "" `Quick test_read_casn ]); + ("no skew", [ Alcotest.test_case "" `Quick test_no_skew ]); + ("get seq", [ Alcotest.test_case "" `Quick test_get_seq ]); ( "stress", [ Alcotest.test_case "" `Quick (fun () -> test_stress (10 * Util.iter_factor) 1_0); ] ); - ("presort", [ Alcotest.test_case "" `Quick test_presort ]); ( "is_in_log", [ Alcotest.test_case "" `Quick test_presort_and_is_in_log_xt ] ); ("updates", [ Alcotest.test_case "" `Quick test_updates ]); diff --git a/test/kcas/test_overlapping_loc.ml b/test/kcas/test_overlapping_loc.ml deleted file mode 100644 index b7e36169..00000000 --- a/test/kcas/test_overlapping_loc.ml +++ /dev/null @@ -1,57 +0,0 @@ -module Loc = Kcas.Loc -module Op = Kcas.Op - -let conflicting_overlap () = - (* [cas_2] acts on the same location as [cas_1] - and has conflicting values. kCAS should be failing. - *) - let v_1 = Loc.make 0 in - let cas_1 = Op.make_cas v_1 0 1 in - let cas_2 = Op.make_cas v_1 2 3 in - - match Op.atomically [ cas_1; cas_2 ] with - | exception _ -> () - | _ -> assert false - -let conflicting_duplicate () = - (* [cas_2] acts on the same location as [cas_1] - and has conflicting values. kCAS should fail. - - It may seem innocuous, since the final value of v_1 - matches even if the CAS succeeds. But it's not. Both - threads think they have successfully CASed v_1 and may - rely on that knowledge afterwards (e.g. use old value - as index in array). - *) - let v_1 = Loc.make 0 in - let cas_1 = Op.make_cas v_1 0 1 in - let cas_2 = Op.make_cas v_1 0 1 in - match Op.atomically [ cas_1; cas_2 ] with - | exception _ -> () - | _ -> assert false - -let meldable_overlap () = - (* [cas_2] acts on the same location as [cas_1]. - This is not something that we can handle in the - general case, but in this particular one, - parameters allow the two CASes to be melded into - one operation. - - Or, perhaps, melding should be left to the user. - *) - let v_1 = Loc.make 0 in - let cas_1 = Op.make_cas v_1 0 1 in - let cas_2 = Op.make_cas v_1 1 2 in - match Op.atomically [ cas_1; cas_2 ] with - | exception _ -> () - | _ -> assert false - -let _ = - Alcotest.run "Overlapping loc" - [ - ( "conflicting overlap", - [ Alcotest.test_case "" `Quick conflicting_overlap ] ); - ( "conflicting duplicate", - [ Alcotest.test_case "" `Quick conflicting_duplicate ] ); - ("meldable overlap", [ Alcotest.test_case "" `Quick meldable_overlap ]); - ]