Skip to content

Commit

Permalink
Merge pull request #23 from ocaml-multicore/fix-gkmz-non-linearizable…
Browse files Browse the repository at this point in the history
…-case

Fix bug to handle non-linearizable cases with `cas r x x` correctly
  • Loading branch information
polytypic authored Feb 8, 2023
2 parents 44939c1 + 86d00e4 commit 3290886
Show file tree
Hide file tree
Showing 3 changed files with 47 additions and 8 deletions.
4 changes: 4 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,10 @@

All notable changes to this project will be documented in this file.

## 0.1.8

* Fix a bug in GKMZ implementation (@polytypic, review: @bartoszmodelski)

## 0.1.7

* Change to use the new GKMZ algorithm (@polytypic, review: @bartoszmodelski)
Expand Down
17 changes: 9 additions & 8 deletions src/kcas.ml
Original file line number Diff line number Diff line change
Expand Up @@ -70,21 +70,22 @@ let finish casn (`Undetermined cass as undetermined)

let rec determine casn undetermined skip = function
| NIL -> skip || finish casn undetermined `After
| CAS (atom, state, lt, gt) as eq ->
| CAS (atom, desired, lt, gt) as eq ->
determine casn undetermined true lt
&&
let state' = Atomic.get atom.state in
if state == state' then determine casn undetermined skip gt
let current = Atomic.get atom.state in
if desired == current then determine casn undetermined skip gt
else
let before = state.before in
let before' = state'.before and after' = state'.after in
let expected = desired.before in
if
(before == before' && before == after')
|| before == if is_after state'.casn then after' else before'
expected == current.after
&& (current.casn == casn_after || is_after current.casn)
|| expected == current.before
&& (current.casn == casn_before || not (is_after current.casn))
then
let status = Atomic.get casn in
if status != (undetermined :> status) then status == `After
else if Atomic.compare_and_set atom.state state' state then
else if Atomic.compare_and_set atom.state current desired then
determine casn undetermined skip gt
else determine casn undetermined skip eq
else finish casn undetermined `Before
Expand Down
34 changes: 34 additions & 0 deletions test/test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,39 @@ module Barrier = struct
done
end

let test_non_linearizable () =
let barrier = Barrier.make 2
and n_iter = 1_000_000
and test_finished = ref false in

let a = Kcas.ref 0 and b = Kcas.ref 0 in

let cass1a = [ Kcas.mk_cas b 0 0; Kcas.mk_cas a 0 1 ]
and cass1b = [ Kcas.mk_cas b 0 0; Kcas.mk_cas a 1 0 ]
and cass2a = [ Kcas.mk_cas b 0 1; Kcas.mk_cas a 0 0 ]
and cass2b = [ Kcas.mk_cas b 1 0; Kcas.mk_cas a 0 0 ] in

let thread1 () =
Barrier.await barrier;
while not !test_finished do
if Kcas.kCAS cass1a then
while not (Kcas.kCAS cass1b) do
assert (Kcas.get a == 1 && Kcas.get b == 0)
done
done
and thread2 () =
Barrier.await barrier;
for _ = 1 to n_iter do
if Kcas.kCAS cass2a then
while not (Kcas.kCAS cass2b) do
assert (Kcas.get a == 0 && Kcas.get b == 1)
done
done;
test_finished := true
in

[ thread2; thread1 ] |> List.map Domain.spawn |> List.iter Domain.join

(* test 1 *)
let test_set () =
let a = Kcas.ref 0 in
Expand Down Expand Up @@ -209,6 +242,7 @@ let test_presort () =
refs |> Array.iter (fun r -> assert (Kcas.get r = n_incs * n_domains))

let () =
test_non_linearizable ();
test_set ();
test_casn ();
test_read_casn ();
Expand Down

0 comments on commit 3290886

Please sign in to comment.