Skip to content

Commit

Permalink
Change/Fix to use a symmetric barrier to synchronize domains
Browse files Browse the repository at this point in the history
  • Loading branch information
polytypic committed Jan 14, 2025
1 parent c27768b commit 6c86871
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 7 deletions.
2 changes: 1 addition & 1 deletion CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

## NEXT RELEASE

- ...
- #509: Change/Fix to use a symmetric barrier to synchronize domains

## 0.6

Expand Down
11 changes: 8 additions & 3 deletions lib/STM_domain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,9 +25,14 @@ module Make (Spec: Spec) = struct
let run_par seq_pref cmds1 cmds2 =
let sut = Spec.init_sut () in
let pref_obs = interp_sut_res sut seq_pref in
let wait = Atomic.make true in
let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp_sut_res sut cmds1) with exn -> Error exn) in
let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp_sut_res sut cmds2) with exn -> Error exn) in
let barrier = Atomic.make 2 in
let main cmds () =
Atomic.decr barrier;
while Atomic.get barrier <> 0 do Domain.cpu_relax() done;
try Ok (interp_sut_res sut cmds) with exn -> Error exn
in
let dom1 = Domain.spawn (main cmds1) in
let dom2 = Domain.spawn (main cmds2) in
let obs1 = Domain.join dom1 in
let obs2 = Domain.join dom2 in
let () = Spec.cleanup sut in
Expand Down
11 changes: 8 additions & 3 deletions lib/lin_domain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,14 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
let run_parallel (seq_pref,cmds1,cmds2) =
let sut = Spec.init () in
let pref_obs = interp sut seq_pref in
let wait = Atomic.make true in
let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp sut cmds1) with exn -> Error exn) in
let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in
let barrier = Atomic.make 2 in
let main cmds () =
Atomic.decr barrier;
while Atomic.get barrier <> 0 do Domain.cpu_relax () done;
try Ok (interp sut cmds) with exn -> Error exn
in
let dom1 = Domain.spawn (main cmds1) in
let dom2 = Domain.spawn (main cmds2) in
let obs1 = Domain.join dom1 in
let obs2 = Domain.join dom2 in
Spec.cleanup sut ;
Expand Down

0 comments on commit 6c86871

Please sign in to comment.