From 06780c88f99d7f7650d3bdebfd50a5a11c5a4445 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 17 Aug 2023 12:48:47 +0300 Subject: [PATCH] WIP: Attempts to tweak internals --- src/kcas/kcas.ml | 445 +++++++++++++++++++++++++---------------------- 1 file changed, 236 insertions(+), 209 deletions(-) diff --git a/src/kcas/kcas.ml b/src/kcas/kcas.ml index e73f2a70..70dc3157 100644 --- a/src/kcas/kcas.ml +++ b/src/kcas/kcas.ml @@ -123,15 +123,19 @@ let[@inline] resume_awaiters = function | [ awaiter ] -> resume_awaiter awaiter | awaiters -> List.iter resume_awaiter awaiters -type 'a state = { - mutable before : 'a; - mutable after : 'a; - mutable casn : casn; - awaiters : awaiter list; -} +type 'a state = + | State : { + mutable before : 'a; + mutable after : 'a; + mutable casn : [ `Determined | `Undetermined ] casn; + awaiters : awaiter list; + } + -> 'a state and cass = - | CASN : { + | Bef : cass + | Aft : cass + | Cas : { loc : 'a loc; state : 'a state; lt : cass; @@ -139,14 +143,11 @@ and cass = mutable awaiters : awaiter list; } -> cass - | NIL : cass - -and casn = status Atomic.t -and status = - | Before (** [false] *) - | After (** [true] *) - | Undetermined of cass +and _ casn = + | Before : [> `Determined ] casn + | After : [> `Determined ] casn + | Undetermined : { mutable cass : cass } -> [> `Undetermined ] casn (* 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] and reduce the @@ -177,91 +178,94 @@ let[@inline] make_loc padded state id = if padded then Multicore_magic.copy_as_padded record else record *) -let[@inline] is_cmp casn state = state.casn != casn -let[@inline] is_cas casn state = state.casn == casn +external casn_as_atomic : [ `Undetermined ] casn -> cass Atomic.t = "%identity" + +external casn_upcast : + [> `Undetermined ] casn -> [ `Determined | `Undetermined ] casn = "%identity" + +let[@inline] is_node = function Bef | Aft -> false | Cas _ -> true +let[@inline] is_cmp casn (State state) = state.casn != casn_upcast casn +let[@inline] is_cas casn (State state) = state.casn == casn_upcast casn module Mode = struct - type t = status + type t = cass - let lock_free = After - let obstruction_free = Before + let lock_free = Aft + let obstruction_free = Bef exception Interference end -let casn_after = Atomic.make After -let casn_before = Atomic.make Before - let rec release_after casn = function - | NIL -> true - | CASN r -> - let lt = r.lt in - if lt != NIL then release_after casn lt |> ignore; - let state = r.state in + | Bef | Aft -> true + | Cas cas_r -> + let lt = cas_r.lt in + if is_node lt then release_after casn lt |> ignore; + let (State state_r as state) = cas_r.state in if is_cas casn state then begin - state.before <- state.after; - state.casn <- casn_after; - resume_awaiters r.awaiters + state_r.before <- state_r.after; + state_r.casn <- After; + resume_awaiters cas_r.awaiters end; - release_after casn r.gt + release_after casn cas_r.gt let rec release_before casn = function - | NIL -> false - | CASN r -> - let lt = r.lt in - if lt != NIL then release_before casn lt |> ignore; - let state = r.state in + | Bef | Aft -> false + | Cas cas_r -> + let lt = cas_r.lt in + if is_node lt then release_before casn lt |> ignore; + let (State state_r as state) = cas_r.state in if is_cas casn state then begin - state.after <- state.before; - state.casn <- casn_before; - resume_awaiters r.awaiters + state_r.after <- state_r.before; + state_r.casn <- Before; + resume_awaiters cas_r.awaiters end; - release_before casn r.gt + release_before casn cas_r.gt let release casn cass status = - if status == After then release_after casn cass else release_before casn cass + if status == Aft then release_after casn cass else release_before casn cass let rec verify casn = function - | NIL -> After - | CASN r -> - let lt = r.lt in - if lt == NIL then - (* Fenceless is safe as [finish] has a fence after. *) - let state = r.state in - if is_cmp casn state && fenceless_get (as_atomic r.loc) != state then - Before - else verify casn r.gt - else + | Bef | Aft -> Aft + | Cas cas_r -> + let lt = cas_r.lt in + if is_node lt then let status = verify casn lt in - if status == After then - let state = r.state in + if status == Aft then + let state = cas_r.state in (* Fenceless is safe as [finish] has a fence after. *) - if is_cmp casn state && fenceless_get (as_atomic r.loc) != state then - Before - else verify casn r.gt + if is_cmp casn state && fenceless_get (as_atomic cas_r.loc) != state + then Bef + else verify casn cas_r.gt else status + else + (* Fenceless is safe as [finish] has a fence after. *) + let state = cas_r.state in + if is_cmp casn state && fenceless_get (as_atomic cas_r.loc) != state + then Bef + else verify casn cas_r.gt let finish casn cass undetermined status = - if Atomic.compare_and_set casn undetermined status then + if Atomic.compare_and_set (casn_as_atomic casn) undetermined status then release casn cass status else (* Fenceless is safe as we have a fence above. *) - fenceless_get casn == After + fenceless_get (casn_as_atomic casn) == Aft let a_cmp = 1 let a_cas = 2 let a_cmp_followed_by_a_cas = 4 -let rec determine casn status = function - | NIL -> status - | CASN r as eq -> +let rec determine (casn : [ `Undetermined ] casn) status = function + | Bef | Aft -> status + | Cas r as eq -> let lt = r.lt in - let status = if lt != NIL then determine casn status lt else status in + let status = if is_node lt then determine casn status lt else status in if status < 0 then status else let loc = r.loc in - let current = Atomic.get (as_atomic loc) in - let state = r.state in + let (State current_r as current) = Atomic.get (as_atomic loc) in + let (State state_r as state) = r.state in if state == current then let a_cas_or_a_cmp = 1 + Bool.to_int (is_cas casn state) in let a_cmp_followed_by_a_cas = a_cas_or_a_cmp * 2 land (status * 4) in @@ -270,16 +274,16 @@ let rec determine casn status = function r.gt else let matches_expected () = - let expected = state.before in - expected == current.after - && (current.casn == casn_after || is_after current.casn) - || expected == current.before - && (current.casn == casn_before || not (is_after current.casn)) + let expected = state_r.before in + expected == current_r.after + && (current_r.casn == After || is_after current_r.casn) + || expected == current_r.before + && (current_r.casn == Before || not (is_after current_r.casn)) in if (not (is_cmp casn state)) && matches_expected () then (* Fenceless is safe as there are fences before and after. *) - match fenceless_get casn with - | Undetermined _ -> + match fenceless_get (casn_as_atomic casn) with + | Cas _ -> (* We now know that the operation wasn't finished when we read [current], but it is possible that the [loc]ation has been updated since then by some other domain helping us (or even @@ -293,7 +297,7 @@ let rec determine casn status = function late as some other domain might finish the operation after the [compare_and_set] and miss the awaiters. *) begin - match current.awaiters with + match current_r.awaiters with | [] -> () | awaiters -> r.awaiters <- awaiters end; @@ -303,32 +307,35 @@ let rec determine casn status = function (status lor a_cas lor a_cmp_followed_by_a_cas) r.gt else determine casn status eq - | After | Before -> raise_notrace Exit + | Bef | Aft -> raise_notrace Exit else -1 -and is_after casn = - (* Fenceless at most gives old [Undetermined] and causes extra work. *) - match fenceless_get casn with - | Undetermined cass as undetermined -> begin - match determine casn 0 cass with - | status -> - finish casn cass undetermined - (if a_cmp_followed_by_a_cas < status then verify casn cass - else if 0 <= status then After - else Before) - | exception Exit -> - (* Fenceless is safe as there was a fence before. *) - fenceless_get casn == After - end - | After -> true +and is_after = function | Before -> false + | After -> true + | Undetermined _ as casn -> begin + (* Fenceless at most gives old [Undetermined] and causes extra work. *) + match fenceless_get (casn_as_atomic casn) with + | Cas _ as cass -> begin + match determine casn 0 cass with + | status -> + finish casn cass cass + (if a_cmp_followed_by_a_cas < status then verify casn cass + else if 0 <= status then Aft + else Bef) + | exception Exit -> + (* Fenceless is safe as there was a fence before. *) + fenceless_get (casn_as_atomic casn) == Aft + end + | Bef -> false + | Aft -> true + end let[@inline] determine_for_owner casn cass = + (* Fenceless is safe as [casn] is private at this point. *) + fenceless_set (casn_as_atomic casn) cass; (* The end result is a cyclic data structure, which is why we cannot initialize the [casn] atomic directly. *) - let undetermined = Undetermined cass in - (* Fenceless is safe as [casn] is private at this point. *) - fenceless_set casn undetermined; match determine casn 0 cass with | status -> if a_cmp_followed_by_a_cas < status then @@ -338,14 +345,14 @@ let[@inline] determine_for_owner casn cass = [lock_free] mode preventing interference. If failure happens before the verify step then the [lock_free] mode would have likely also failed. *) - finish casn cass undetermined (verify casn cass) + finish casn cass cass (verify casn cass) || raise_notrace Mode.Interference else a_cmp = status - || finish casn cass undetermined (if 0 <= status then After else Before) + || finish casn cass cass (if 0 <= status then Aft else Bef) | exception Exit -> (* Fenceless is safe as there was a fence before. *) - fenceless_get casn == After + fenceless_get (casn_as_atomic casn) == Aft let[@inline never] impossible () = failwith "impossible" let[@inline never] overlap () = failwith "kcas: location overlap" @@ -354,41 +361,41 @@ let[@inline never] invalid_retry () = failwith "kcas: invalid use of retry" type splay = Miss : splay | Hit : 'a loc * 'a state -> splay let[@inline] make_casn loc state lt gt = - CASN { loc; state; lt; gt; awaiters = [] } + Cas { loc; state; lt; gt; awaiters = [] } let rec splay ~hit_parent x = function - | NIL -> (NIL, Miss, NIL) - | CASN { loc = a; state = s; lt = l; gt = r; _ } as t -> - if x < a.id && ((not hit_parent) || l != NIL) then + | Bef | Aft -> (Bef, Miss, Bef) + | Cas { loc = a; state = s; lt = l; gt = r; _ } as t -> + if x < a.id && ((not hit_parent) || is_node l) then match l with - | NIL -> (NIL, Miss, t) - | CASN { loc = pa; state = ps; lt = ll; gt = lr; _ } -> - if x < pa.id && ((not hit_parent) || ll != NIL) then + | Bef | Aft -> (Bef, Miss, t) + | Cas { loc = pa; state = ps; lt = ll; gt = lr; _ } -> + if x < pa.id && ((not hit_parent) || is_node ll) then let lll, n, llr = splay ~hit_parent x ll in (lll, n, make_casn pa ps llr (make_casn a s lr r)) - else if pa.id < x && ((not hit_parent) || lr != NIL) then + else if pa.id < x && ((not hit_parent) || is_node lr) then let lrl, n, lrr = splay ~hit_parent x lr in (make_casn pa ps ll lrl, n, make_casn a s lrr r) else (ll, Hit (pa, ps), make_casn a s lr r) - else if a.id < x && ((not hit_parent) || r != NIL) then + else if a.id < x && ((not hit_parent) || is_node r) then match r with - | NIL -> (t, Miss, NIL) - | CASN { loc = pa; state = ps; lt = rl; gt = rr; _ } -> - if x < pa.id && ((not hit_parent) || rl != NIL) then + | Bef | Aft -> (t, Miss, Bef) + | Cas { loc = pa; state = ps; lt = rl; gt = rr; _ } -> + if x < pa.id && ((not hit_parent) || is_node rl) then let rll, n, rlr = splay ~hit_parent x rl in (make_casn a s l rll, n, make_casn pa ps rlr rr) - else if pa.id < x && ((not hit_parent) || rr != NIL) then + else if pa.id < x && ((not hit_parent) || is_node rr) then let rrl, n, rrr = splay ~hit_parent x rr in (make_casn pa ps (make_casn a s l rl) rrl, n, rrr) else (make_casn a s l rl, Hit (pa, ps), rr) else (l, Hit (a, s), r) let[@inline] new_state after = - { before = after; after; casn = casn_after; awaiters = [] } + State { before = after; after; casn = After; awaiters = [] } -let[@inline] eval state = - let before = state.before and after = state.after in - if before == after || is_after state.casn then after else before +let[@inline] eval (State state_r) = + let before = state_r.before and after = state_r.after in + if before == after || is_after state_r.casn then after else before module Retry = struct exception Later @@ -403,10 +410,10 @@ end let add_awaiter loc before awaiter = (* Fenceless is safe as we have fence after. *) - let state_old = fenceless_get (as_atomic loc) in + let (State state_old_r as state_old) = fenceless_get (as_atomic loc) in let state_new = - let awaiters = awaiter :: state_old.awaiters in - { before; after = before; casn = casn_after; awaiters } + let awaiters = awaiter :: state_old_r.awaiters in + State { before; after = before; casn = After; awaiters } in before == eval state_old && Atomic.compare_and_set (as_atomic loc) state_old state_new @@ -419,12 +426,14 @@ let[@tail_mod_cons] rec remove_first x' removed = function let rec remove_awaiter loc before awaiter = (* Fenceless is safe as we have fence after. *) - let state_old = fenceless_get (as_atomic loc) in + let (State state_old_r as state_old) = fenceless_get (as_atomic loc) in if before == eval state_old then let removed = ref true in - let awaiters = remove_first awaiter removed state_old.awaiters in + let awaiters = remove_first awaiter removed state_old_r.awaiters in if !removed then - let state_new = { before; after = before; casn = casn_after; awaiters } in + let state_new = + State { before; after = before; casn = After; awaiters } + in if not (Atomic.compare_and_set (as_atomic loc) state_old state_new) then remove_awaiter loc before awaiter @@ -440,20 +449,20 @@ let block timeout loc before = end; Timeout.unawait timeout alive -let rec update_no_alloc timeout backoff loc state f = +let rec update_no_alloc timeout backoff loc (State state_r as state) f = (* Fenceless is safe as we have had a fence before if needed and there is a fence after. *) - let state_old = fenceless_get (as_atomic loc) in + let (State state_old_r as state_old) = fenceless_get (as_atomic loc) in let before = eval state_old in match f before with | after -> - state.after <- after; + state_r.after <- after; if before == after then begin Timeout.cancel timeout; before end else if Atomic.compare_and_set (as_atomic loc) state_old state then begin - state.before <- after; - resume_awaiters state_old.awaiters; + state_r.before <- after; + resume_awaiters state_old_r.awaiters; Timeout.cancel timeout; before end @@ -465,7 +474,7 @@ let rec update_no_alloc timeout backoff loc state f = Timeout.cancel timeout; raise exn -let update_with_state timeout backoff loc f state_old = +let update_with_state timeout backoff loc f (State state_old_r as state_old) = let before = eval state_old in match f before with | after -> @@ -476,7 +485,7 @@ let update_with_state timeout backoff loc f state_old = else let state = new_state after in if Atomic.compare_and_set (as_atomic loc) state_old state then begin - resume_awaiters state_old.awaiters; + resume_awaiters state_old_r.awaiters; Timeout.cancel timeout; before end @@ -489,28 +498,29 @@ let update_with_state timeout backoff loc f state_old = Timeout.cancel timeout; raise exn -let rec exchange_no_alloc backoff loc state = - let state_old = Atomic.get (as_atomic loc) in +let rec exchange_no_alloc backoff loc (State state_r as state) = + let (State state_old_r as state_old) = Atomic.get (as_atomic loc) in let before = eval state_old in - if before == state.after then before + if before == state_r.after then before else if Atomic.compare_and_set (as_atomic loc) state_old state then begin - resume_awaiters state_old.awaiters; + resume_awaiters state_old_r.awaiters; before end else exchange_no_alloc (Backoff.once backoff) loc state let[@inline] is_obstruction_free casn loc = (* Fenceless is safe as we are accessing a private location. *) - fenceless_get casn == (Mode.obstruction_free :> status) && 0 <= loc.id + fenceless_get (casn_as_atomic casn) == Mode.obstruction_free && 0 <= loc.id -let[@inline] rec cas_with_state loc before state state_old = - let before' = state_old.before and after' = state_old.after in +let[@inline] rec cas_with_state loc before (State state_r as state) + (State state_old_r as state_old) = + let before' = state_old_r.before and after' = state_old_r.after in ((before == before' && before == after') - || before == if is_after state_old.casn then after' else before') - && (before == state.after + || before == if is_after state_old_r.casn then after' else before') + && (before == state_r.after || if Atomic.compare_and_set (as_atomic loc) state_old state then begin - resume_awaiters state_old.awaiters; + resume_awaiters state_old_r.awaiters; true end else @@ -609,8 +619,8 @@ module Loc = struct fenceless_update ?backoff loc dec |> ignore let has_awaiters loc = - let state = Atomic.get (as_atomic loc) in - state.awaiters != [] + let (State state_r) = Atomic.get (as_atomic loc) in + state_r.awaiters != [] let fenceless_get loc = eval (fenceless_get (as_atomic loc)) end @@ -618,14 +628,14 @@ 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 = [] } + | Cas { loc = a; lt = Bef | Aft; _ } when x < a.id -> + Cas { loc; state; lt = Bef; gt = cass; awaiters = [] } + | Cas { loc = a; gt = Bef | Aft; _ } when a.id < x -> + Cas { loc; state; lt = cass; gt = Bef; awaiters = [] } | _ -> begin match splay ~hit_parent:false x cass with | _, Hit _, _ -> overlap () - | lt, Miss, gt -> CASN { loc; state; lt; gt; awaiters = [] } + | lt, Miss, gt -> Cas { loc; state; lt; gt; awaiters = [] } end module Op = struct @@ -648,7 +658,7 @@ module Op = struct | [] -> true | [ op ] -> atomic op | first :: rest -> - let casn = Atomic.make (mode :> status) in + let casn = Undetermined { cass = mode } in let rec run cass = function | [] -> determine_for_owner casn cass | CAS (loc, before, after) :: rest -> @@ -658,7 +668,14 @@ module Op = struct before == eval state && run (insert cass loc state) rest else run - (insert cass loc { before; after; casn; awaiters = [] }) + (insert cass loc + (State + { + before; + after; + casn = casn_upcast casn; + awaiters = []; + })) rest in let (CAS (loc, before, after)) = first in @@ -666,10 +683,12 @@ module Op = struct (* 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 + && run (Cas { loc; state; lt = Bef; gt = Bef; awaiters = [] }) rest else - let state = { before; after; casn; awaiters = [] } in - run (CASN { loc; state; lt = NIL; gt = NIL; awaiters = [] }) rest + let state = + State { before; after; casn = casn_upcast casn; awaiters = [] } + in + run (Cas { loc; state; lt = Bef; gt = Bef; awaiters = [] }) rest end module Xt = struct @@ -679,7 +698,7 @@ module Xt = struct (**) type 'x t = { mutable _timeout : Timeout.t; - mutable casn : casn; + mutable casn : [ `Undetermined ] casn; mutable cass : cass; mutable validate_counter : int; mutable post_commit : Action.t; @@ -703,16 +722,16 @@ module Xt = struct let[@inline] timeout_as_atomic r = r._timeout *) - let[@inline] validate_one casn loc state = - let before = if is_cmp casn state then eval state else state.before in + let[@inline] validate_one casn loc (State state_r as state) = + let before = if is_cmp casn state then eval state else state_r.before in (* Fenceless is safe inside transactions as each log update has a fence. *) if before != eval (fenceless_get (as_atomic loc)) then Retry.invalid () let rec validate_all casn = function - | NIL -> () - | CASN r -> + | Bef | Aft -> () + | Cas r -> let lt = r.lt in - if lt != NIL then validate_all casn lt; + if is_node lt then validate_all casn lt; validate_one casn r.loc r.state; validate_all casn r.gt @@ -734,42 +753,43 @@ module Xt = struct | after -> let state = if before == after && is_obstruction_free xt.casn loc then state - else { before; after; casn = xt.casn; awaiters = [] } + else + State { before; after; casn = casn_upcast xt.casn; awaiters = [] } in - xt.cass <- CASN { loc; state; lt; gt; awaiters = [] }; + xt.cass <- Cas { loc; state; lt; gt; awaiters = [] }; before | exception exn -> - xt.cass <- CASN { loc; state; lt; gt; awaiters = [] }; + xt.cass <- Cas { loc; state; lt; gt; awaiters = [] }; raise exn let[@inline] update loc f xt state' lt gt = - let state = Obj.magic state' in + let (State state_r as state) = Obj.magic state' in if is_cmp xt.casn state then begin let before = eval state in let after = f before in let state = if before == after then state - else { before; after; casn = xt.casn; awaiters = [] } + else State { before; after; casn = casn_upcast xt.casn; awaiters = [] } in - xt.cass <- CASN { loc; state; lt; gt; awaiters = [] }; + xt.cass <- Cas { loc; state; lt; gt; awaiters = [] }; before end else - let current = state.after in - let state = { state with after = f current } in - xt.cass <- CASN { loc; state; lt; gt; awaiters = [] }; + let current = state_r.after in + let state = State { state_r with after = f current } in + xt.cass <- Cas { loc; state; lt; gt; awaiters = [] }; current let[@inline] unsafe_update ~xt loc f = maybe_validate_log xt; let x = loc.id in match xt.cass with - | NIL -> update0 loc f xt NIL NIL - | CASN { loc = a; lt = NIL; _ } as cass when x < a.id -> - update0 loc f xt NIL cass - | CASN { loc = a; gt = NIL; _ } as cass when a.id < x -> - update0 loc f xt cass NIL - | CASN { loc = a; state; lt; gt; _ } when Obj.magic a == loc -> + | Bef | Aft -> update0 loc f xt Bef Bef + | Cas { loc = a; lt = Bef | Aft; _ } as cass when x < a.id -> + update0 loc f xt Bef cass + | Cas { loc = a; gt = Bef | Aft; _ } as cass when a.id < x -> + update0 loc f xt cass Bef + | Cas { loc = a; state; lt; gt; _ } when Obj.magic a == loc -> update loc f xt state lt gt | cass -> begin match splay ~hit_parent:false x cass with @@ -812,15 +832,15 @@ module Xt = struct let validate ~xt loc = let x = loc.id in match xt.cass with - | NIL -> () - | CASN { loc = a; lt = NIL; _ } when x < a.id -> () - | CASN { loc = a; gt = NIL; _ } when a.id < x -> () - | CASN { loc = a; state; _ } when Obj.magic a == loc -> + | Bef | Aft -> () + | Cas { loc = a; lt = Bef | Aft; _ } when x < a.id -> () + | Cas { loc = a; gt = Bef | Aft; _ } when a.id < x -> () + | Cas { loc = a; state; _ } when Obj.magic a == loc -> validate_one xt.casn a state | cass -> begin match splay ~hit_parent:true x cass with | lt, Hit (a, state), gt -> - xt.cass <- CASN { loc = a; state; lt; gt; awaiters = [] }; + xt.cass <- Cas { loc = a; state; lt; gt; awaiters = [] }; if Obj.magic a == loc then validate_one xt.casn a state | _, Miss, _ -> impossible () end @@ -828,14 +848,14 @@ module Xt = struct let is_in_log ~xt loc = let x = loc.id in match xt.cass with - | NIL -> false - | CASN { loc = a; lt = NIL; _ } when x < a.id -> false - | CASN { loc = a; gt = NIL; _ } when a.id < x -> false - | CASN { loc = a; _ } when Obj.magic a == loc -> true + | Bef | Aft -> false + | Cas { loc = a; lt = Bef | Aft; _ } when x < a.id -> false + | Cas { loc = a; gt = Bef | Aft; _ } when a.id < x -> false + | Cas { loc = a; _ } when Obj.magic a == loc -> true | cass -> begin match splay ~hit_parent:true x cass with | lt, Hit (a, state), gt -> - xt.cass <- CASN { loc = a; state; lt; gt; awaiters = [] }; + xt.cass <- Cas { loc = a; state; lt; gt; awaiters = [] }; Obj.magic a == loc | _, Miss, _ -> impossible () end @@ -844,27 +864,27 @@ module Xt = struct if cass_snap == cass then cass else match cass with - | NIL -> NIL - | CASN r -> begin + | (Bef | Aft) as nil -> nil + | Cas r -> begin let loc = r.loc in match splay ~hit_parent:false loc.id cass_snap with | lt_mark, Miss, gt_mark -> let lt = rollback casn lt_mark r.lt and gt = rollback casn gt_mark r.gt in let state = - let state = r.state in + let (State state_r as state) = r.state in if is_cmp casn state then state else (* Fenceless is safe inside transactions as each log update has a fence. *) let current = fenceless_get (as_atomic loc) in - if state.before != eval current then Retry.invalid () + if state_r.before != eval current then Retry.invalid () else current in - CASN { loc; state; lt; gt; awaiters = [] } + Cas { loc; state; lt; gt; awaiters = [] } | lt_mark, Hit (loc, state), gt_mark -> let lt = rollback casn lt_mark r.lt and gt = rollback casn gt_mark r.gt in - CASN { loc; state; lt; gt; awaiters = [] } + Cas { loc; state; lt; gt; awaiters = [] } end type 'x snap = cass * Action.t @@ -892,30 +912,30 @@ module Xt = struct let[@inline] call ~xt { tx } = tx ~xt let rec add_awaiters awaiter casn = function - | NIL as cont -> cont - | CASN r as stop -> begin + | (Bef | Aft) as nil -> nil + | Cas r as stop -> begin let lt = r.lt in - match if lt == NIL then lt else add_awaiters awaiter casn lt with - | NIL -> + match if is_node lt then add_awaiters awaiter casn lt else lt with + | Bef | Aft -> if add_awaiter r.loc - (let state = r.state in - if is_cmp casn state then eval state else state.before) + (let (State state_r as state) = r.state in + if is_cmp casn state then eval state else state_r.before) awaiter then add_awaiters awaiter casn r.gt else stop - | CASN _ as stop -> stop + | Cas _ as stop -> stop end let rec remove_awaiters awaiter casn stop = function - | NIL -> () - | CASN r as current -> + | Bef | Aft -> () + | Cas r as current -> let lt = r.lt in - if lt != NIL then remove_awaiters awaiter casn stop lt; + if is_node lt then remove_awaiters awaiter casn stop lt; if current != stop then begin remove_awaiter r.loc - (let state = r.state in - if is_cmp casn state then eval state else state.before) + (let (State state_r as state) = r.state in + if is_cmp casn state then eval state else state_r.before) awaiter; remove_awaiters awaiter casn stop r.gt end @@ -923,31 +943,38 @@ module Xt = struct let initial_validate_period = 16 let[@inline] reset_quick xt = - xt.cass <- NIL; + xt.cass <- Bef; xt.validate_counter <- initial_validate_period; xt.post_commit <- Action.noop; xt let reset mode xt = - xt.casn <- Atomic.make (mode :> status); + xt.casn <- Undetermined { cass = mode }; reset_quick xt let rec commit backoff mode xt tx = match tx ~xt with | result -> begin match xt.cass with - | NIL -> + | Bef | Aft -> Timeout.cancel (timeout_as_atomic xt); Action.run xt.post_commit result - | CASN { loc; state; lt = NIL; gt = NIL; _ } -> + | Cas + { + loc; + state = State state_r as state; + lt = Bef | Aft; + gt = Bef | Aft; + _; + } -> if is_cmp xt.casn state then begin Timeout.cancel (timeout_as_atomic xt); Action.run xt.post_commit result end else - let before = state.before in - state.before <- state.after; - state.casn <- casn_after; + let before = state_r.before in + state_r.before <- state_r.after; + state_r.casn <- After; (* Fenceless is safe inside transactions as each log update has a fence. *) let state_old = fenceless_get (as_atomic loc) in if cas_with_state loc before state state_old then begin @@ -970,22 +997,22 @@ module Xt = struct Timeout.check (timeout_as_atomic xt); commit (Backoff.once backoff) mode (reset_quick xt) tx | exception Retry.Later -> begin - if xt.cass == NIL then invalid_retry (); + if xt.cass == Bef then invalid_retry (); let t = Domain_local_await.prepare_for_await () in let alive = Timeout.await (timeout_as_atomic xt) t.release in match add_awaiters t.release xt.casn xt.cass with - | NIL -> begin + | Bef | Aft -> begin match t.await () with | () -> - remove_awaiters t.release xt.casn NIL xt.cass; + remove_awaiters t.release xt.casn Bef xt.cass; Timeout.unawait (timeout_as_atomic xt) alive; commit (Backoff.reset backoff) mode (reset_quick xt) tx | exception cancellation_exn -> - remove_awaiters t.release xt.casn NIL xt.cass; + remove_awaiters t.release xt.casn Bef xt.cass; Timeout.cancel_alive alive; raise cancellation_exn end - | CASN _ as stop -> + | Cas _ as stop -> remove_awaiters t.release xt.casn stop xt.cass; Timeout.unawait (timeout_as_atomic xt) alive; commit (Backoff.once backoff) mode (reset_quick xt) tx @@ -996,8 +1023,8 @@ module Xt = struct let[@inline] commit ?timeoutf ?(backoff = Backoff.default) ?(mode = Mode.obstruction_free) tx = - let casn = Atomic.make (mode :> status) - and cass = NIL + let casn = Undetermined { cass = mode } + and cass = Bef and validate_counter = initial_validate_period and post_commit = Action.noop in let xt =