File tree Expand file tree Collapse file tree 1 file changed +3
-3
lines changed
Expand file tree Collapse file tree 1 file changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -128,9 +128,9 @@ let agree_prop_par =
128128 assume (WSDT. cmds_ok WSDConf. init_state (seq_pref@ stealer));
129129 let sut = WSDConf. init_sut () in
130130 let pref_obs = WSDT. interp_sut_res sut seq_pref in
131- let wait = Atomic. make true in
132- let stealer_dom = Domain. spawn (fun () -> Atomic. set wait false ; Domain. cpu_relax () ; WSDT. interp_sut_res sut stealer) in
133- while Atomic. get wait do Domain. cpu_relax() done ;
131+ let sema = Semaphore.Binary. make false in
132+ let stealer_dom = Domain. spawn (fun () -> Semaphore.Binary. release sema ; WSDT. interp_sut_res sut stealer) in
133+ while not ( Semaphore.Binary. try_acquire sema) do Domain. cpu_relax() done ;
134134 let own_obs = WSDT. interp_sut_res sut owner in
135135 let stealer_obs = Domain. join stealer_dom in
136136 let res = WSDT. check_obs pref_obs own_obs stealer_obs WSDConf. init_state in
You can’t perform that action at this time.
0 commit comments