Add agree_prop_par_asym to STM_domain

[jmid]

This PR fixes #310 by adding an asymmetric property agree_prop_par_asym to STM_domain.
This is handy to run tests that spawn only 1 child domain to run and interpret cmds in parallel with the parent domain.
To make printing of such triples nicer, the PR includes a new triple generator STM_domain.arb_triple_asym that has a corresponding "symmetric printer" set.

I pinned the patched version locally to see how this would help clean up the existing ws_deque test from lockfree.
For comparison, here's a diff:

diff --git a/test/ws_deque/stm_ws_deque.ml b/test/ws_deque/stm_ws_deque.ml
index fd502bc..90af0d1 100644
--- a/test/ws_deque/stm_ws_deque.ml
+++ b/test/ws_deque/stm_ws_deque.ml
@@ -63,56 +63,22 @@ end
 module WSDT_seq = STM_sequential.Make (WSDConf)
 module WSDT_dom = STM_domain.Make (WSDConf)
 
-(* The following definitions differ slightly from those in multicoretests:lib/STM.ml.
-   This has to do with how work-stealing deques are supposed to be used according to spec:
-   - [agree_prop_par] differs in that it only spawns one domain ("a stealer domain")
-     in parallel with the original "owner domain" (it also uses [Semaphore.Binary]) *)
-let agree_prop_par (seq_pref, owner, stealer) =
-  assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref @ owner));
-  assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref @ stealer));
-  let sut = WSDConf.init_sut () in
-  let pref_obs = WSDT_dom.interp_sut_res sut seq_pref in
-  let sema = Semaphore.Binary.make false in
-  let stealer_dom =
-    Domain.spawn (fun () ->
-        Semaphore.Binary.release sema;
-        WSDT_dom.interp_sut_res sut stealer)
-  in
-  while not (Semaphore.Binary.try_acquire sema) do
-    Domain.cpu_relax ()
-  done;
-  let own_obs = WSDT_dom.interp_sut_res sut owner in
-  let stealer_obs = Domain.join stealer_dom in
-  let res =
-    WSDT_dom.check_obs pref_obs own_obs stealer_obs WSDConf.init_state
-  in
-  let () = WSDConf.cleanup sut in
-  res
-  || Test.fail_reportf "  Results incompatible with linearized model:\n\n%s"
-     @@ Util.print_triple_vertical ~center_prefix:false STM.show_res
-          (List.map snd pref_obs, List.map snd own_obs, List.map snd stealer_obs)
-
-(* [arb_cmds_par] differs in what each triple component generates:
-   "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *)
-let arb_cmds_par =
-  WSDT_dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd
-
 (* A parallel agreement test - w/repeat and retries combined *)
-let agree_test_par ~count ~name =
-  let rep_count = 50 in
-  Test.make ~retries:10 ~count ~name arb_cmds_par
-    (repeat rep_count agree_prop_par)
-
-(* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *)
-let agree_test_par_negative ~count ~name =
-  WSDT_dom.neg_agree_test_par ~count ~name
+let agree_test_par_asym ~count ~name =
+  let rep_count = 20 in
+  let seq_len,par_len = 20,12 in
+  Test.make ~retries:10 ~count ~name
+    (* "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *)
+    (WSDT_dom.arb_triple_asym seq_len par_len WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd)
+    (repeat rep_count WSDT_dom.agree_prop_par_asym)
 
 let () =
   let count = 1000 in
   QCheck_base_runner.run_tests_main
     [
       WSDT_seq.agree_test ~count ~name:"STM Lockfree.Ws_deque test sequential";
-      agree_test_par ~count ~name:"STM Lockfree.Ws_deque test parallel";
-      agree_test_par_negative ~count
-        ~name:"STM Lockfree.Ws_deque test parallel, negative";
+      agree_test_par_asym ~count ~name:"STM Lockfree.Ws_deque test parallel";
+      (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *)
+      WSDT_dom.neg_agree_test_par
+                          ~count ~name:"STM Lockfree.Ws_deque test parallel, negative";

I realize that

• I left some commented out code which needs removing
• This needs a Changes entry

[jmid]

CC @lyrm as this could be helpful in ocaml-multicore/saturn#61

[lyrm]

Great ! Thanks !

[jmid]

PR rebased on top of the merged #318.
To make this convenient I've reexported all_interleavings_ok in STM_domain.
Because of the pulled-out precondition check of #318, one therefore has to specify it in a custom test property as an additional line, e.g., something along these lines:

+let agree_test_par_asym ~count ~name =
+  let rep_count = 20 in
+  let seq_len,par_len = 20,12 in
+  Test.make ~retries:10 ~count ~name
+    (* "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *)
+    (WSDT_dom.arb_triple_asym seq_len par_len WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd)
+    (fun ((seq_pref,cmds1,cmds2) as triple) ->
+      assume (WSDT_dom.all_interleavings_ok seq_pref cmds1 cmds2 WSDConf.init_state);
+      repeat rep_count WSDT_dom.agree_prop_par_asym triple)

(We could also go further and export a version of all_interleavings_ok (perhaps under a different name) that simply accepts the triple, e.g., so that the latter lines could be simplified to something like:

+    (fun triple ->
+      assume (WSDT_dom.interleavings_ok triple);
+      repeat rep_count WSDT_dom.agree_prop_par_asym triple)

[shym]

Maybe we could expose {neg_,}agree_test_par_asym functions, similar to the symmetric ones. I understand the idea that those tests are probably more useful with different command generators for each part but it would:

• make it easier to switch from symmetric to asymmetric testing (I would be curious to try it out on the whole test suite),
• give a reference implementation for the cases when you do need to tune it,
• it could maybe take as optional arguments the various arb_cmd if that’s the most probable tuning.

[shym]

Is there a reason to use a Semaphore rather than an Atomic like in the symmetric version?

[shym]

Using Semaphore, we could say Semaphore.Binary.acquire sema rather than using a loop. I don’t know if that would entail an undesirable delay, though.

[jmid]

I've

• added the suggested {neg_,}agree_test_par_asym bindings in 83bdd6f
• adjusted the API to export a triple-accepting all_interleavings_ok as suggested above

As to the choice of Atomic and while vs. Semaphore.Binary with while or try_acquire,
initially the Lockfree test wouldn't trigger with the former on macOS so I tried a Semaphore:
7ed7479
which seemed to please the macOS gods at the time aka work.
It may have been caused by another issue or better replaced by try_acquire.
We should definitely measure - but we could also do so in a separate PR.

[jmid]

CI summary:

• a Windows 5.0 threadomain crash
• failure to trigger the Out_channel issue on Windows trunk and macOS trunk (push + pull request run)

None of these are related to the current PR

[shym]

I just reviewed the 4 extra commits: well done!
I think this is ready for merging.

[shym]

I just notice this line because it appears in the diff: the 4 agree_test_par accept those labelled parameters but it is documented on two of them. The labels are self-explanatory, though.

[jmid]

Fair enough! Addressed in b6a471a

[jmid]

CI summary:

• Windows bytecode trunk triggered a Thread CList failure
• Windows and macOs trunk both failed to trigger the Out_channel issue
• Windows bytecode 5.1 and trunk both timedout on the threadomains test
• Cygwin trunk (PR and push) both timed out due to Lin DSL Weak HashSet test with Domain taking a long time