Revisit uses of fenceless_get

Author: polytypic

src/kcas/kcas.ml

@@ -148,12 +148,14 @@ let rec verify casn = function
   | NIL -> `After
   | CASN { loc; state; lt; gt; _ } -> (
       if lt == NIL then
+        (* Fenceless is safe as [finish] has a fence after. *)
         if is_cmp casn state && fenceless_get (as_atomic loc) != state then
           `Before
         else verify casn gt
       else
         match verify casn lt with
         | `After ->
+            (* Fenceless is safe as [finish] has a fence after. *)
             if is_cmp casn state && fenceless_get (as_atomic loc) != state then
               `Before
             else verify casn gt
@@ -162,7 +164,9 @@ let rec verify casn = function
 let finish casn (`Undetermined cass as undetermined) (status : determined) =
   if Atomic.compare_and_set casn (undetermined :> status) (status :> status)
   then release casn cass status
-  else fenceless_get casn == `After
+  else
+    (* Fenceless is safe as we have a fence above. *)
+    fenceless_get casn == `After
 
 let a_cmp = 1
 let a_cas = 2
@@ -190,6 +194,7 @@ let rec determine casn status = function
                && (current.casn == casn_before || not (is_after current.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 _ ->
                 (* We now know that the operation wasn't finished when we read
@@ -217,6 +222,7 @@ let rec determine casn status = function
           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 -> (
       match determine casn 0 cass with
@@ -225,14 +231,17 @@ and is_after casn =
             (if a_cmp_followed_by_a_cas < status then verify casn cass
              else if 0 <= status then `After
              else `Before)
-      | exception Exit -> fenceless_get casn == `After)
+      | exception Exit ->
+          (* Fenceless is safe as there was a fence before. *)
+          fenceless_get casn == `After)
   | `After -> true
   | `Before -> false
 
 let determine_for_owner casn cass =
-  let undetermined = `Undetermined cass in
   (* 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 ->
@@ -247,7 +256,9 @@ let determine_for_owner casn cass =
       else
         a_cmp = status
         || finish casn undetermined (if 0 <= status then `After else `Before)
-  | exception Exit -> fenceless_get casn == `After
+  | exception Exit ->
+      (* Fenceless is safe as there was a fence before. *)
+      fenceless_get casn == `After
   [@@inline]
 
 let impossible () = failwith "impossible" [@@inline never]
@@ -307,6 +318,7 @@ module Retry = struct
 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_new =
     let awaiters = awaiter :: state_old.awaiters in
@@ -322,6 +334,7 @@ let[@tail_mod_cons] rec remove_first x' removed = function
   | x :: xs -> if x == x' then xs else x :: remove_first x' removed xs
 
 let rec remove_awaiter loc before awaiter =
+  (* Fenceless is safe as we have fence after. *)
   let state_old = fenceless_get (as_atomic loc) in
   if before == eval state_old then
     let removed = ref true in
@@ -340,40 +353,56 @@ let block loc before =
       raise cancellation_exn)
 
 let rec update_no_alloc backoff loc state f =
-  let state' = fenceless_get (as_atomic loc) in
-  let before = eval state' in
+  (* 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 before = eval state_old in
   match f before with
   | after ->
       state.after <- after;
       if before == after then before
-      else if Atomic.compare_and_set (as_atomic loc) state' state then (
+      else if Atomic.compare_and_set (as_atomic loc) state_old state then (
         state.before <- after;
-        resume_awaiters before state'.awaiters)
+        resume_awaiters before state_old.awaiters)
       else update_no_alloc (Backoff.once backoff) loc state f
   | exception Retry.Later ->
       block loc before;
       update_no_alloc backoff loc state f
 
+let update_with_state backoff loc f state_old =
+  let before = eval state_old in
+  match f before with
+  | after ->
+      if before == after then before
+      else
+        let state = new_state after in
+        if Atomic.compare_and_set (as_atomic loc) state_old state then
+          resume_awaiters before state_old.awaiters
+        else update_no_alloc (Backoff.once backoff) loc state f
+  | exception Retry.Later ->
+      let state = new_state before in
+      block loc before;
+      update_no_alloc backoff loc state f
+
 let rec exchange_no_alloc backoff loc state =
-  let state' = fenceless_get (as_atomic loc) in
-  let before = eval state' in
+  let state_old = Atomic.get (as_atomic loc) in
+  let before = eval state_old in
   if before == state.after then before
-  else if Atomic.compare_and_set (as_atomic loc) state' state then
-    resume_awaiters before state'.awaiters
+  else if Atomic.compare_and_set (as_atomic loc) state_old state then
+    resume_awaiters before state_old.awaiters
   else exchange_no_alloc (Backoff.once backoff) loc state
 
 let 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
   [@@inline]
 
-let cas loc before state =
-  let state' = fenceless_get (as_atomic loc) in
-  let before' = state'.before and after' = state'.after in
+let cas_with_state loc before state state_old =
+  let before' = state_old.before and after' = state_old.after in
   ((before == before' && before == after')
-  || before == if is_after state'.casn then after' else before')
+  || before == if is_after state_old.casn then after' else before')
   && (before == state.after
-     || Atomic.compare_and_set (as_atomic loc) state' state
-        && resume_awaiters true state'.awaiters)
+     || Atomic.compare_and_set (as_atomic loc) state_old state
+        && resume_awaiters true state_old.awaiters)
   [@@inline]
 
 let inc x = x + 1
@@ -415,33 +444,39 @@ module Loc = struct
 
   let compare_and_set loc before after =
     let state = new_state after in
-    cas loc before state
+    let state_old = Atomic.get (as_atomic loc) in
+    cas_with_state loc before state state_old
+
+  let fenceless_update ?(backoff = Backoff.default) loc f =
+    update_with_state backoff loc f (fenceless_get (as_atomic loc))
+
+  let fenceless_modify ?backoff loc f =
+    fenceless_update ?backoff loc f |> ignore
+    [@@inline]
 
   let update ?(backoff = Backoff.default) loc f =
-    let state' = fenceless_get (as_atomic loc) in
-    let before = eval state' in
-    match f before with
-    | after ->
-        if before == after then before
-        else
-          let state = new_state after in
-          if Atomic.compare_and_set (as_atomic loc) state' state then
-            resume_awaiters before state'.awaiters
-          else update_no_alloc (Backoff.once backoff) loc state f
-    | exception Retry.Later ->
-        let state = new_state before in
-        block loc before;
-        update_no_alloc backoff loc state f
+    update_with_state backoff loc f (Atomic.get (as_atomic loc))
 
   let modify ?backoff loc f = update ?backoff loc f |> ignore [@@inline]
 
   let exchange ?(backoff = Backoff.default) loc value =
     exchange_no_alloc backoff loc (new_state value)
 
   let set ?backoff loc value = exchange ?backoff loc value |> ignore
-  let fetch_and_add ?backoff loc n = update ?backoff loc (( + ) n)
-  let incr ?backoff loc = update ?backoff loc inc |> ignore
-  let decr ?backoff loc = update ?backoff loc dec |> ignore
+
+  let fetch_and_add ?backoff loc n =
+    if n = 0 then get loc
+    else
+      (* Fenceless is safe as we always update. *)
+      fenceless_update ?backoff loc (( + ) n)
+
+  let incr ?backoff loc =
+    (* Fenceless is safe as we always update. *)
+    fenceless_update ?backoff loc inc |> ignore
+
+  let decr ?backoff loc =
+    (* Fenceless is safe as we always update. *)
+    fenceless_update ?backoff loc dec |> ignore
 
   let has_awaiters loc =
     let state = Atomic.get (as_atomic loc) in
@@ -489,6 +524,7 @@ module Op = struct
           | [] -> 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 before or after. *)
                 let state = fenceless_get (as_atomic loc) in
                 before == eval state && run (insert cass loc state) rest
               else
@@ -498,7 +534,7 @@ module Op = struct
         in
         let (CAS (loc, before, after)) = first in
         if before == after && is_obstruction_free casn loc then
-          let state = fenceless_get (as_atomic loc) in
+          let state = Atomic.get (as_atomic loc) in
           before == eval state
           && run (CASN { loc; state; lt = NIL; gt = NIL; awaiters = [] }) rest
         else
@@ -517,6 +553,7 @@ module Xt = struct
 
   let validate_one casn loc state =
     let before = if is_cmp casn state then eval state else state.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 ()
     [@@inline]
 
@@ -540,6 +577,7 @@ module Xt = struct
     [@@inline]
 
   let update0 loc f xt lt gt =
+    (* Fenceless is safe inside transactions as each log update has a fence. *)
     let state = fenceless_get (as_atomic loc) in
     let before = eval state in
     match f before with
@@ -667,6 +705,7 @@ module Xt = struct
               let state =
                 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 ()
                   else current
@@ -745,7 +784,10 @@ module Xt = struct
               let before = state.before in
               state.before <- state.after;
               state.casn <- casn_after;
-              if cas loc before state then Action.run xt.post_commit result
+              (* 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
+                Action.run xt.post_commit result
               else commit (Backoff.once backoff) mode (reset_quick xt) tx
         | cass -> (
             match determine_for_owner xt.casn cass with

src/kcas/kcas.mli

@@ -141,6 +141,14 @@ module Loc : sig
   val fenceless_get : 'a t -> 'a
   (** [fenceless_get r] is like [get r] except that [fenceless_get]s may be
       reordered. *)
+
+  val fenceless_update : ?backoff:Backoff.t -> 'a t -> ('a -> 'a) -> 'a
+  (** [fenceless_update r f] is like [update r f] except that in case [f x == x]
+      the update may be reordered. *)
+
+  val fenceless_modify : ?backoff:Backoff.t -> 'a t -> ('a -> 'a) -> unit
+  (** [fenceless_modify r f] is like [modify r f] except that in case [f x == x]
+      the modify may be reordered. *)
 end
 
 (** {1 Manipulating multiple locations atomically}

src/kcas_data/hashtbl.ml

@@ -353,18 +353,21 @@ end
 
 let find_opt t k =
   let t = Loc.get t in
+  (* Fenceless is safe as we have a fence above. *)
   t.buckets |> bucket_of t.hash k |> Loc.fenceless_get
   |> Assoc.find_opt t.equal k
 
 let find_all t k =
   let t = Loc.get t in
+  (* Fenceless is safe as we have a fence above. *)
   t.buckets |> bucket_of t.hash k |> Loc.fenceless_get
   |> Assoc.find_all t.equal k
 
 let find t k = match find_opt t k with None -> raise Not_found | Some v -> v
 
 let mem t k =
   let t = Loc.get t in
+  (* Fenceless is safe as we have a fence above. *)
   t.buckets |> bucket_of t.hash k |> Loc.fenceless_get |> Assoc.mem t.equal k
 
 let clear t = Kcas.Xt.commit { tx = Xt.clear t }
@@ -388,6 +391,7 @@ let snapshot ?length ?record t =
   in
   Kcas.Xt.commit { tx };
   Kcas.Xt.commit { tx = Xt.perform_pending t } |> ignore;
+  (* Fenceless is safe as commit above has fences. *)
   Loc.fenceless_get snapshot
 
 let to_seq t =
@@ -463,6 +467,7 @@ let filter_map_inplace fn t =
   in
   Kcas.Xt.commit { tx };
   Kcas.Xt.commit { tx = Xt.perform_pending t } |> ignore;
+  (* Fenceless is safe as commit above has fences. *)
   match Loc.fenceless_get raised with Done -> () | exn -> raise exn
 
 let stats t =

src/kcas_data/mvar.ml

@@ -25,12 +25,18 @@ module Xt = struct
 end
 
 let is_empty mv = Magic_option.is_none (Loc.get mv)
-let put mv value = Loc.modify mv (Magic_option.put_or_retry value)
+
+let put mv value =
+  (* Fenceless is safe as we always update. *)
+  Loc.fenceless_modify mv (Magic_option.put_or_retry value)
 
 let try_put mv value =
   Loc.compare_and_set mv Magic_option.none (Magic_option.some value)
 
-let take mv = Magic_option.get_unsafe (Loc.update mv Magic_option.take_or_retry)
+let take mv =
+  (* Fenceless is safe as we always update. *)
+  Magic_option.get_unsafe (Loc.fenceless_update mv Magic_option.take_or_retry)
+
 let take_opt mv = Magic_option.to_option (Loc.exchange mv Magic_option.none)
 let peek mv = Loc.get_as Magic_option.get_or_retry mv
 let peek_opt mv = Magic_option.to_option (Loc.get mv)

src/kcas_data/queue.ml

@@ -122,15 +122,25 @@ end
 
 let is_empty q = Kcas.Xt.commit { tx = Xt.is_empty q }
 let length q = Kcas.Xt.commit { tx = Xt.length q }
-let add x q = Loc.modify q.back @@ Elems.cons x
+
+let add x q =
+  (* Fenceless is safe as we always update. *)
+  Loc.fenceless_modify q.back @@ Elems.cons x
+
 let push = add
 
 let take_opt q =
-  match Loc.update q.front Elems.tl_safe |> Elems.hd_opt with
+  (* Fenceless is safe as we revert to a transaction in case we didn't update. *)
+  match Loc.fenceless_update q.front Elems.tl_safe |> Elems.hd_opt with
   | None -> Kcas.Xt.commit { tx = Xt.take_opt q }
   | some -> some
 
-let take_blocking q = Kcas.Xt.commit { tx = Xt.take_blocking q }
+let take_blocking q =
+  (* Fenceless is safe as we revert to a transaction in case we didn't update. *)
+  match Loc.fenceless_update q.front Elems.tl_safe |> Elems.hd_opt with
+  | None -> Kcas.Xt.commit { tx = Xt.take_blocking q }
+  | Some elem -> elem
+
 let take_all q = Kcas.Xt.commit { tx = Xt.take_all q }
 
 let peek_opt q =

src/kcas_data/stack.ml

@@ -25,10 +25,18 @@ end
 
 let length s = Loc.get s |> Elems.length
 let is_empty s = Loc.get s == Elems.empty
-let push x s = Loc.modify s @@ Elems.cons x
+
+let push x s =
+  (* Fenceless is safe as we always update. *)
+  Loc.fenceless_modify s @@ Elems.cons x
+
 let pop_opt s = Loc.update s Elems.tl_safe |> Elems.hd_opt
 let pop_all s = Loc.exchange s Elems.empty |> Elems.to_seq
-let pop_blocking s = Loc.update s Elems.tl_or_retry |> Elems.hd_unsafe
+
+let pop_blocking s =
+  (* Fenceless is safe as we always update. *)
+  Loc.fenceless_update s Elems.tl_or_retry |> Elems.hd_unsafe
+
 let top_opt s = Loc.get s |> Elems.hd_opt
 let top_blocking s = Loc.get_as Elems.hd_or_retry s
 let clear s = Loc.set s Elems.empty