Skip to content

Commit a35efe3

Browse files
committed
Use GADT to avoid closures
1 parent bf0d66d commit a35efe3

File tree

1 file changed

+70
-53
lines changed

1 file changed

+70
-53
lines changed

src/kcas/kcas.ml

+70-53
Original file line numberDiff line numberDiff line change
@@ -685,83 +685,100 @@ module Xt = struct
685685
(* Fenceless is safe as we are accessing a private location. *)
686686
xt_r.mode == `Obstruction_free && 0 <= loc.id
687687

688-
let[@inline] update_new loc f xt lt gt =
689-
(* Fenceless is safe inside transactions as each log update has a fence. *)
688+
type (_, _) up =
689+
| Get : (unit, 'a) up
690+
| Fetch_and_add : (int, int) up
691+
| Exchange : ('a, 'a) up
692+
| Fn : ('a -> 'a, 'a) up
693+
| Compare_and_swap : ('a * 'a, 'a) up
694+
695+
let[@inline] update :
696+
type c a.
697+
'x t -> a loc -> c -> (c, a) up -> tree -> tree -> a state -> a -> a =
698+
fun xt loc c up lt gt state before ->
699+
let after =
700+
match up with
701+
| Get -> before
702+
| Fetch_and_add -> before + c
703+
| Exchange -> c
704+
| Compare_and_swap -> if fst c == before then snd c else before
705+
| Fn -> begin
706+
try c before
707+
with exn ->
708+
tree_as_ref xt := T (Node { loc; state; lt; gt; awaiters = [] });
709+
raise exn
710+
end
711+
in
712+
let state =
713+
if before == after && is_obstruction_free xt loc then state
714+
else { before; after; which = W xt; awaiters = [] }
715+
in
716+
tree_as_ref xt := T (Node { loc; state; lt; gt; awaiters = [] });
717+
before
718+
719+
let[@inline] update_new :
720+
type c a. 'x t -> a loc -> c -> (c, a) up -> tree -> tree -> a =
721+
fun xt loc c up lt gt ->
690722
let state = fenceless_get (as_atomic loc) in
691723
let before = eval state in
692-
match f before with
693-
| after ->
694-
let state =
695-
if before == after && is_obstruction_free xt loc then state
696-
else { before; after; which = W xt; awaiters = [] }
697-
in
698-
tree_as_ref xt := T (Node { loc; state; lt; gt; awaiters = [] });
699-
before
700-
| exception exn ->
701-
tree_as_ref xt := T (Node { loc; state; lt; gt; awaiters = [] });
702-
raise exn
703-
704-
let[@inline] update_top loc f xt state' lt gt =
705-
let state = Obj.magic state' in
706-
if is_cmp xt state then begin
707-
let before = eval state in
708-
let after = f before in
709-
let state =
710-
if before == after then state
711-
else { before; after; which = W xt; awaiters = [] }
724+
update xt loc c up lt gt state before
725+
726+
let[@inline] update_top :
727+
type c a. 'x t -> a loc -> c -> (c, a) up -> 'b state -> tree -> tree -> a
728+
=
729+
fun xt loc c up state' lt gt ->
730+
let state : a state = Obj.magic state' in
731+
if is_cmp xt state then update xt loc c up lt gt state (eval state)
732+
else
733+
let before = state.after in
734+
let after =
735+
match up with
736+
| Get -> before
737+
| Fetch_and_add -> before + c
738+
| Exchange -> c
739+
| Compare_and_swap -> if fst c == before then snd c else before
740+
| Fn -> c before
712741
in
742+
let state = if before == after then state else { state with after } in
713743
tree_as_ref xt := T (Node { loc; state; lt; gt; awaiters = [] });
714744
before
715-
end
716-
else
717-
let current = state.after in
718-
let state = { state with after = f current } in
719-
tree_as_ref xt := T (Node { loc; state; lt; gt; awaiters = [] });
720-
current
721745

722-
let[@inline] unsafe_update ~xt loc f =
746+
let unsafe_update ~xt loc c up =
723747
let loc = Loc.to_loc loc in
724748
maybe_validate_log xt;
725749
let x = loc.id in
726750
match !(tree_as_ref xt) with
727-
| T Leaf -> update_new loc f xt (T Leaf) (T Leaf)
751+
| T Leaf -> update_new xt loc c up (T Leaf) (T Leaf)
728752
| T (Node { loc = a; lt = T Leaf; _ }) as tree when x < a.id ->
729-
update_new loc f xt (T Leaf) tree
753+
update_new xt loc c up (T Leaf) tree
730754
| T (Node { loc = a; gt = T Leaf; _ }) as tree when a.id < x ->
731-
update_new loc f xt tree (T Leaf)
755+
update_new xt loc c up tree (T Leaf)
732756
| T (Node { loc = a; state; lt; gt; _ }) when Obj.magic a == loc ->
733-
update_top loc f xt state lt gt
757+
update_top xt loc c up state lt gt
734758
| tree -> begin
735759
match splay ~hit_parent:false x tree with
736-
| l, T Leaf, r -> update_new loc f xt l r
737-
| l, T (Node node_r), r -> update_top loc f xt node_r.state l r
760+
| l, T Leaf, r -> update_new xt loc c up l r
761+
| l, T (Node node_r), r -> update_top xt loc c up node_r.state l r
738762
end
739763

740-
let[@inline] protect xt f x =
741-
let tree = !(tree_as_ref xt) in
742-
let y = f x in
743-
assert (!(tree_as_ref xt) == tree);
744-
y
745-
746-
let get ~xt loc = unsafe_update ~xt loc Fun.id
747-
let set ~xt loc after = unsafe_update ~xt loc (fun _ -> after) |> ignore
748-
let modify ~xt loc f = unsafe_update ~xt loc (protect xt f) |> ignore
764+
let get ~xt loc = unsafe_update ~xt loc () Get
765+
let set ~xt loc after = unsafe_update ~xt loc after Exchange |> ignore
766+
let modify ~xt loc f = unsafe_update ~xt loc f Fn |> ignore
749767

750768
let compare_and_swap ~xt loc before after =
751-
unsafe_update ~xt loc (fun actual ->
752-
if actual == before then after else actual)
769+
unsafe_update ~xt loc (before, after) Compare_and_swap
753770

754771
let compare_and_set ~xt loc before after =
755772
compare_and_swap ~xt loc before after == before
756773

757-
let exchange ~xt loc after = unsafe_update ~xt loc (fun _ -> after)
758-
let fetch_and_add ~xt loc n = unsafe_update ~xt loc (( + ) n)
759-
let incr ~xt loc = unsafe_update ~xt loc inc |> ignore
760-
let decr ~xt loc = unsafe_update ~xt loc dec |> ignore
761-
let update ~xt loc f = unsafe_update ~xt loc (protect xt f)
774+
let exchange ~xt loc after = unsafe_update ~xt loc after Exchange
775+
let fetch_and_add ~xt loc n = unsafe_update ~xt loc n Fetch_and_add
776+
let incr ~xt loc = unsafe_update ~xt loc 1 Fetch_and_add |> ignore
777+
let decr ~xt loc = unsafe_update ~xt loc (-1) Fetch_and_add |> ignore
778+
let update ~xt loc f = unsafe_update ~xt loc f Fn
762779
let swap ~xt l1 l2 = set ~xt l1 @@ exchange ~xt l2 @@ get ~xt l1
763-
let unsafe_modify ~xt loc f = unsafe_update ~xt loc f |> ignore
764-
let unsafe_update ~xt loc f = unsafe_update ~xt loc f
780+
let unsafe_modify ~xt loc f = unsafe_update ~xt loc f Fn |> ignore
781+
let unsafe_update ~xt loc f = unsafe_update ~xt loc f Fn
765782

766783
let[@inline] to_blocking ~xt tx =
767784
match tx ~xt with None -> Retry.later () | Some value -> value

0 commit comments

Comments
 (0)