@@ -215,8 +215,6 @@ module Mode = struct
215215
216216 let lock_free = After
217217 let obstruction_free = Before
218-
219- exception Interference
220218end
221219
222220let [@ inline] isnt_int x = not (Obj. is_int (Obj. repr x))
@@ -351,29 +349,6 @@ and is_after = function
351349 | R After -> true
352350 end
353351
354- let [@ inline] determine_for_owner which root =
355- (* Fenceless is safe as [which] is private at this point. *)
356- fenceless_set (root_as_atomic which) (R root);
357- (* The end result is a cyclic data structure, which is why we cannot
358- initialize the [which] atomic directly. *)
359- match determine which 0 (T root) with
360- | status ->
361- if a_cmp_followed_by_a_cas < status then
362- (* We only want to [raise Interference] in case it is the verify step
363- that fails. The idea is that in [lock_free] mode the attempt might
364- have succeeded as the compared locations would have been set in
365- [lock_free] mode preventing interference. If failure happens before
366- the verify step then the [lock_free] mode would have likely also
367- failed. *)
368- finish which root (verify which (T root))
369- || raise_notrace Mode. Interference
370- else
371- a_cmp = status
372- || finish which root (if 0 < = status then After else Before )
373- | exception Exit ->
374- (* Fenceless is safe as there was a fence before. *)
375- fenceless_get (root_as_atomic which) == R After
376-
377352let [@ inline never] impossible () = failwith " impossible"
378353let [@ inline never] invalid_retry () = failwith " kcas: invalid use of retry"
379354
@@ -826,7 +801,8 @@ module Xt = struct
826801 let state = node_r.state in
827802 if is_cmp which state then state
828803 else
829- (* Fenceless is safe inside transactions as each log update has a fence. *)
804+ (* Fenceless is safe inside transactions as each log update
805+ has a fence. *)
830806 let current = fenceless_get (as_atomic node_r.loc) in
831807 if state.before != eval current then Retry. invalid ()
832808 else current
@@ -904,40 +880,57 @@ module Xt = struct
904880 xt.which < - Undetermined { root = R mode };
905881 reset_quick xt
906882
883+ let success xt result =
884+ Timeout. cancel (timeout_as_atomic xt);
885+ Action. run xt.post_commit result
886+
907887 let rec commit backoff mode xt tx =
908888 match tx ~xt with
909889 | result -> begin
910890 match xt.tree with
911- | T Leaf ->
912- Timeout. cancel (timeout_as_atomic xt);
913- Action. run xt.post_commit result
891+ | T Leaf -> success xt result
914892 | T (Node { loc; state; lt = T Leaf ; gt = T Leaf ; _ } ) ->
915- if is_cmp xt.which state then begin
916- Timeout. cancel (timeout_as_atomic xt);
917- Action. run xt.post_commit result
918- end
893+ if is_cmp xt.which state then success xt result
919894 else begin
920895 state.which < - W After ;
921896 let before = state.before in
922897 if isnt_int before then state.before < - Obj. magic () ;
923- (* Fenceless is safe inside transactions as each log update has a fence. *)
898+ (* Fenceless is safe inside transactions as each log update has a
899+ fence. *)
924900 let state_old = fenceless_get (as_atomic loc) in
925- if cas_with_state loc before state state_old then begin
926- Timeout. cancel (timeout_as_atomic xt);
927- Action. run xt.post_commit result
928- end
901+ if cas_with_state loc before state state_old then
902+ success xt result
929903 else commit (Backoff. once backoff) mode (reset_quick xt) tx
930904 end
931905 | T (Node node_r ) -> begin
932906 let root = Node node_r in
933- match determine_for_owner xt.which root with
934- | true ->
935- Timeout. cancel (timeout_as_atomic xt);
936- Action. run xt.post_commit result
937- | false -> commit (Backoff. once backoff) mode (reset mode xt) tx
938- | exception Mode. Interference ->
939- commit (Backoff. once backoff) Mode. lock_free
940- (reset Mode. lock_free xt) tx
907+ (* Fenceless is safe as [which] is private at this point. *)
908+ fenceless_set (root_as_atomic xt.which) (R root);
909+ (* The end result is a cyclic data structure, which is why we cannot
910+ initialize the [which] atomic directly. *)
911+ match determine xt.which 0 (T root) with
912+ | status ->
913+ if a_cmp_followed_by_a_cas < status then begin
914+ if finish xt.which root (verify xt.which (T root)) then
915+ success xt result
916+ else begin
917+ (* We switch to [Mode.lock_free] as there was
918+ interference. *)
919+ commit (Backoff. once backoff) Mode. lock_free
920+ (reset Mode. lock_free xt) tx
921+ end
922+ end
923+ else if
924+ a_cmp = status
925+ || finish xt.which root
926+ (if 0 < = status then After else Before )
927+ then success xt result
928+ else commit (Backoff. once backoff) mode (reset mode xt) tx
929+ | exception Exit ->
930+ (* Fenceless is safe as there was a fence before. *)
931+ if fenceless_get (root_as_atomic xt.which) == R After then
932+ success xt result
933+ else commit (Backoff. once backoff) mode (reset mode xt) tx
941934 end
942935 end
943936 | exception Retry. Invalid ->
0 commit comments