diff --git a/CHANGES.md b/CHANGES.md index be5de668c..68b4fa94d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,7 +2,7 @@ ## NEXT RELEASE -- ... +- #509: Change/Fix to use a symmetric barrier to synchronize domains ## 0.6 diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index 18a883c2a..b00a36b51 100644 --- a/lib/STM_domain.ml +++ b/lib/STM_domain.ml @@ -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 diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml index 57eced2b6..1feafd82a 100644 --- a/lib/lin_domain.ml +++ b/lib/lin_domain.ml @@ -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 ;