Add thread for STM

[n-osborne]

should close #81 when finished

[n-osborne]

As noted in #66 for Lin, I expect it would be better to split STM in STM_Domains and STM_Thread.

[jmid]

Thanks! I agree that we are going to change the API anyway to address #66.
To minimize API changes it might indeed be better to add an STM Thread interpretation as part of that...
I'll try to elaborate a bit more in #66...

[n-osborne]

I'm happy to either add this refactoring onto this PR or do it in another.

[jmid]

Great - thanks 🙏 - either is fine I think 👍

[jmid]

Thanks for this! 🙏 (note: we should do the same for Lin - but probably in a separate PR)

Perhaps it can be confusing to a newcomer that agree_test changes meaning across modules? 🤔
One possibility is to

• keep agree_test in the sequential functor output
• keep agree_test_par in the Domain functor output
• use agree_test_conc in the Thread functor output?

@naomi-spargo @OlivierNicole - what do you think?

We are a bit inconsistent naming-wise (StmSpec vs STM_Common).
Since the sub-modules already live inside the STM library an option is to omit the prefix and fully qualify the name:
STM.Domain.Make(...). This comes at the risk of shadowing Domain and Thread from the Stdlib though.

I would love if something similar is possible for the StmSpec.S interface...
Renaming StmSpec.ml to STM.ml and S to Spec would yield the pleasing STM.Spec
with the less pleasing STM.STM.Spec fully qualified name 😬
I am open to suggestions to fix this... 😃

[n-osborne]

Perhaps it can be confusing to a newcomer that agree_test changes meaning across modules? thinking One possibility is to

* keep `agree_test` in the sequential functor output

* keep `agree_test_par` in the `Domain` functor output

* use `agree_test_conc` in the `Thread` functor output?

I was going for making the distinction in the modules' name (less function's name to find...), but I'm totally ok with your proposition.

We are a bit inconsistent naming-wise (StmSpec vs STM_Common). Since the sub-modules already live inside the STM library an option is to omit the prefix and fully qualify the name: STM.Domain.Make(...). This comes at the risk of shadowing Domain and Thread from the Stdlib though.

I agree. Also, the user shouldn't make use of Stdlib.Domain or Stdlib.Thread (which are still available fully qualified) when writing tests with STM, no? In this case, I guess shadowing is not really a big issue. Or is there a use case that I don't see?

I would love if something similar is possible for the StmSpec.S interface... Renaming StmSpec.ml to STM.ml and S to Spec would yield the pleasing STM.Spec with the less pleasing STM.STM.Spec fully qualified name grimacing I am open to suggestions to fix this... smiley

The Spec interface is now included in the STM module, not in an elegant way but we have STM.Spec as the fully qualified name for the user. Note that the user can also access it via STM_Core.Spec. Not sure it is an issue?

[jmid]

Perhaps it can be confusing to a newcomer that agree_test changes meaning across modules? 🤔 One possibility is to

* keep `agree_test` in the sequential functor output

* keep `agree_test_par` in the `Domain` functor output

* use `agree_test_conc` in the `Thread` functor output?

I was going for making the distinction in the modules' name (less function's name to find...), but I'm totally ok with your proposition.

I was also thinking of another convenience:
One could include the output of the sequential functor in both the Domain and Thread functors.
In that case we will need different identifiers to distinguish the different tests and properties.
(I'd still like to keep the sequential functor though)

Also, the user shouldn't make use of Stdlib.Domain or Stdlib.Thread (which are still available fully qualified) when writing tests with STM, no? In this case, I guess shadowing is not really a big issue. Or is there a use case that I don't see?

No, I agree with you.

I would love if something similar is possible for the StmSpec.S interface... Renaming StmSpec.ml to STM.ml and S to Spec would yield the pleasing STM.Spec with the less pleasing STM.STM.Spec fully qualified name grimacing I am open to suggestions to fix this... smiley

The Spec interface is now included in the STM module, not in an elegant way but we have STM.Spec as the fully qualified name for the user. Note that the user can also access it via STM_Core.Spec. Not sure it is an issue?

Nice! No, I don't think this is an issue.
I guess we can also restrict access further by limiting the public package visibility and/or adding .mli files.

[n-osborne]

So I've added an interface file for STM and cleaned up a bit the dune file.
STM_Core should not be shared with the world as a path (the content is still included in STM).

[jmid]

Excellent - looks good! 👍

I was also thinking of another convenience:
One could include the output of the sequential functor in both the Domain and Thread functors.
In that case we will need different identifiers to distinguish the different tests and properties.
(I'd still like to keep the sequential functor though)

Any thoughts on the above convenience?
For a user only interested in, e.g., parallel Domain tests it would save one functor application 🤷‍♂️

As to the functor/module names, this uses a mixture of underscores _ and CamelCase: STM_Core, STM_Domain, ...
I was just looking at https://discuss.ocaml.org/t/capitalized-underscore-vs-camelcase/502 to understand the OCaml convention.
It seems underscores are agreed upon. Since Domain and Thread refer to Stdlib module names, I can see the point in keeping them like that - and changing only one occurrence STM_core will then stand out and seem inconsistent, so overall I'm OK with the module naming you propose 🙏

As to tests, it would be nice to include just one STM_Thread application, e.g., in src/neg_test to make sure that this functor indeed works as intended. Ideally the Spec of such a test can then live in a third file and be shared across two executables with STM_Thread and STM_Domain.

[n-osborne]

Thanks 😃

I was also thinking of another convenience:
One could include the output of the sequential functor in both the Domain and Thread functors.
In that case we will need different identifiers to distinguish the different tests and properties.
(I'd still like to keep the sequential functor though)

Any thoughts on the above convenience? For a user only interested in, e.g., parallel Domain tests it would save one functor application man_shrugging

That's true, but does a user interested in e.g. STM_Domain is necessarily interested in STM_Seq?
Also, that would meant the with both STM_Domain.Make and STM_Thread.Make built, the user would have STM_Seq twice.
That's not a problem because of shadowing, but I don't find it very elegant.

As a user, I don't mind applying one more functor. And w.r.t design, it's not a strong opinion, but I like the clean "one functor per kind of test" 😃

As to tests, it would be nice to include just one STM_Thread application, e.g., in src/neg_test to make sure that this functor indeed works as intended. Ideally the Spec of such a test can then live in a third file and be shared across two executables with STM_Thread and STM_Domain.

I was waiting for the refactoring to settle a bit down before adding more Thread tests. I agree that a negative test is the bare minimum.

[jmid]

I think the easiest for you would be to run git rebase main on your PR branch with an up-to-date main branch
and resolve any conflicts underway to avoid "fixing commits".

[OlivierNicole]

@naomi-spargo @OlivierNicole - what do you think?

Sorry I hadn't reacted to this, since I get notifications from all multicoretests activity I don't always go read the messages… I think the decision has been taken now?

[jmid]

I think the decision has been taken now?

We are still open to input to arrive at a nice interface. Your perspective is therefore welcome!
Furthermore, I expect that we will make an analogous split in Lin following this PR.

[jmid]

A "default interpreter" feels a bit overkill when there are only two "backend interpreters" 🤔
The alternative to including a "default" interpreter targeting Domain and overriding it in STM_Thread would be to let each of STM_Domain and STM_Thread provide their own.

Can you share your thoughts on this choice? (I might be missing something)

[n-osborne]

I agree this is not the best design. I was focusing on having agree_test_conc finding the expected bugs (which still fail).

There is also the re-exportation of four functions in STM_Seq (the reason is that they are needed in src/lockfree/ws_deque_test.ml) which is not a great design and is related to this one.

[OlivierNicole]

I think the decision has been taken now?

We are still open to input to arrive at a nice interface. Your perspective is therefore welcome! Furthermore, I expect that we will make an analogous split in Lin following this PR.

The interface you have arrived at looks OK to me.

[n-osborne]

rebased on latest main with QCheck 0.19

[jmid]

The latest run starts by triggering an error in dune in the CI:
https://github.com/jmid/multicoretests/runs/7279773909?check_suite_focus=true#step:6:14

I suggest

• creating a minimal reproducable test case and filing an issue on dune
• figuring out why it errors here (it seems related to STM_Core?

[n-osborne]

Since #145 the interface documentation has been pulled out into a separate .mli-file. In it's current state the PR reverses #145 and the STM documentation added since. I'd be grateful if the STM.mli content could be split up into .mlis for the proposed modules, to avoid having to redo it pray

I've now restored the lost documentation and put it in the right places. This leads to spot again a few duplicated code. I also added documentation to function newly exposed (because of the splitting in different modules).

Since the PR has been rebased a couple of times, I'm wondering whether it represents a refactoring of the latest STM code. The reverted comments make me suspect it is not thinking

I think it is good. But I'll take another look with fresh eyes.

From a user perspective, a user has to list 3 dependencies (libraries qcheck-stm.base qcheck-stm.sequential qcheck-stm.domain) to write an STM test running both sequentially and using Domain. I understand that the first holds the functor input's module interface, and that the latter two contain one "mode" each. Still, that's definitely more than the previous (libraries STM) - and all of these then have to explained to potential new users. Do you see any way to simplify this requirement?

I completely agree and that was something that was bothering me. As qcheck-stm.base is always necessary, it could be re-exposed by the other, so the user wouldn't have to add it in its dependencies. It is not a big library, so I guess it is ok to have it twice (in qcheck-multicoretests.sequential and in qcheck-multicoretsts.domain).

[n-osborne]

The divergence that appeared in one (or more) of the rebasing is now corrected.
Modifications in main:lib/STM.ml didn't show in stm-thread:lib/STM_*.ml and a diff didn't really help, so I've traced all the code movement done by this PR.

The list of all the definition present in main has been build with the following command followed by minimal clean up (I believe that it does not forgot anything):

grep -E "^type|^ type|^let|^ let|^ val|^module" lib/STM.ml

type 'a ty = ..                                        --> STM_spec.ml
type _ ty +=                                           --> STM_spec.ml
type 'a ty_show =                                      --> STM_spec.ml
let unit =                                             --> STM_spec.ml
let bool =                                             --> STM_spec.ml
let char =                                             --> STM_spec.ml
let int =                                              --> STM_spec.ml
let int32 =                                            --> STM_spec.ml
let int64 =                                            --> STM_spec.ml
let float =                                            --> STM_spec.ml
let string =                                           --> STM_spec.ml
let bytes =                                            --> STM_spec.ml
let option spec =                                      --> STM_spec.ml
let exn =                                              --> STM_spec.ml
let show_result show_ok show_err =                     --> STM_spec.ml
let result spec_ok spec_err =                          --> STM_spec.ml
let list spec =                                        --> STM_spec.ml
let array spec =                                       --> STM_spec.ml
let seq spec =                                         --> STM_spec.ml
type res =                                             --> STM_spec.ml
let show_res (Res ((_,show), v)) =                     --> STM_spec.ml
module type StmSpec =                                  --> STM_spec.ml (renamed as Spec)
  type cmd                                             --> STM_spec.ml
  type state                                           --> STM_spec.ml
  type sut                                             --> STM_spec.ml
  val arb_cmd : state -> cmd arbitrary                 --> STM_spec.ml
  val show_cmd : cmd -> string                         --> STM_spec.ml
  val init_state : state                               --> STM_spec.ml
  val next_state : cmd -> state -> state               --> STM_spec.ml
  val init_sut : unit -> sut                           --> STM_spec.ml
  val cleanup : sut -> unit                            --> STM_spec.ml
  val precond : cmd -> state -> bool                   --> STM_spec.ml
  val run : cmd -> sut -> res                          --> STM_spec.ml
  val postcond : cmd -> state -> res -> bool           --> STM_spec.ml
module Make(Spec : StmSpec) =                          --> STM_internal.ml
  let rec gen_cmds arb s fuel =                        --> STM_internal.ml
  let rec cmds_ok s cs =                               --> STM_internal.ml
  let arb_cmds s =                                     --> STM_internal.ml
  let consistency_test ~count ~name =                  --> STM_internal.ml
  let rec interp_agree s sut cs =                      --> STM_internal.ml
  let rec check_disagree s sut cs =                    --> STM_internal.ml
  let print_seq_trace trace =                          --> STM_sequential.ml 
  let agree_prop =                                     --> STM_sequential.ml
  let agree_test ~count ~name =                        --> STM_sequential.ml
  let neg_agree_test ~count ~name =                    --> STM_sequential
  let check_and_next (c,res) s =                       --> STM_internal.ml
  let interp_sut_res sut cs =                          --> STM_sequential.ml & STM_domain.ml (redifined)
  let rec all_interleavings_ok pref cs1 cs2 s =        --> STM_internal.ml
  let rec check_obs pref cs1 cs2 s =                   --> STM_internal.ml
  let gen_cmds_size gen s size_gen =                   --> STM_internal.ml & STM_sequential.ml
  let shrink_cmd arb cmd state =                       --> STM_internal.ml
  let rec shrink_cmd_list arb cs state =               --> STM_internal.ml
  let shrink_triple_elems arb0 arb1 arb2 (seq,p1,p2) = --> STM_internal.ml
  let shrink_triple arb0 arb1 arb2 =                   --> STM_internal.ml reexposed in STM_sequential.ml
  let arb_triple seq_len par_len arb0 arb1 arb2 =      --> STM_internal.ml reexposed in STM_domain.ml
  let arb_cmds_par seq_len par_len =                   --> STM_internal.ml reexposed in STM_domain.ml
  let agree_prop_par (seq_pref,cmds1,cmds2) =          --> STM_domain.ml
  let agree_test_par ~count ~name =                    --> STM_domain.ml
  let neg_agree_test_par ~count ~name =                --> STM_domain.ml
module AddGC(Spec : StmSpec) : StmSpec                 --> STM_Spec.ml
  type cmd =                                           --> STM_Spec.ml
  type state =                                         --> STM_Spec.ml
  type sut   =                                         --> STM_Spec.ml
  let init_state  =                                    --> STM_Spec.ml
  let init_sut () =                                    --> STM_Spec.ml
  let cleanup sut =                                    --> STM_Spec.ml
  let show_cmd c =                                     --> STM_Spec.ml
  let gen_cmd s =                                      --> STM_Spec.ml
  let shrink_cmd s c =                                 --> STM_Spec.ml
  let arb_cmd s =                                      --> STM_Spec.ml
  let next_state c s =                                 --> STM_Spec.ml
  let precond c s =                                    --> STM_Spec.ml
  let run c s =                                        --> STM_Spec.ml
  let postcond c s r =                                 --> STM_Spec.ml

[shym]

I took @jmid’s last comment as a cue to have a fresh look at this PR ;-)

First of all, I would have preferred to see it structured into at least the following steps (of one or more commits):

1. refactoring, by splitting STM into _domain and _sequential libraries
2. adding STM_thread
3. cosmetic changes (I think I saw a couple of them on the way).

As it is not structured thus, I went on to review the global diff rather than the commits, trusting git to tell what is interesting from what I could skip: git diff --color-moved=dimmed-zebra $(git merge-base main @) @. So I only reviewed what seemed more than code shuffling. I opened a small PR to polish it. In particular, when qcheck-stm.sequential or qcheck-stm.domain is needed, qcheck-stm.base is implicitly added by dune, so no need to mention explicitly, which answers one of @jmid’s remarks. Another commit my small PR fixes a few counts that were changed on main and not on the PR. Those were the only mishaps left I saw.

During that review I noticed another thing I’d rather see changed: some lines are really long; I’m not completely against using more than 80 columns since we seldom have so little screen space available and enforcing it can make code less legible, but I think more than, say, 140 is never legible anyway (and that’s what I see in full screen, pretty much).

[jmid]

I have taken another pass over the PR, going over the differences between shym/polish-stm-threads and jmid/main.
I've then written commits to keep the diff minimal:

• removing/deleting changed white space
• keeping code changes to a minimum
• reverting a few CI tests that were enabled by the PR and could cause the CI test runs to differ more than necessary
• adjusting typos in documentation
• adjusting a few test names

The result is available here: https://github.com/jmid/multicoretests/tree/more-polish-stm-threads

You should be able to see the (slightly smaller) difference against main here
(a dummy PR that displays the diff against main, so press 'Files changed' but don't press 'Create pull request'):
https://github.com/jmid/multicoretests/compare/main...jmid:multicoretests:more-polish-stm-threads?expand=1

[n-osborne]

Thanks @jmid for this new this new polish. I'm totally ok for it to be merged on this PR.

[jmid]

I continued by looking at the proposed STM interfaces:

check_obs and shrink_triple with the below signatures involve triples and hence morally belong in STM_domain rather than STM_sequential:

 val check_obs : (Spec.cmd * res) list -> (Spec.cmd * res) list -> (Spec.cmd * res) list -> Spec.state -> bool
 val shrink_triple : (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.Shrink.t

I also found interp_sut_res in STM_sequential even though it isn't used there.

 val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * res) list

This is a bit of a historical artifact, since the sequential mode uses check_disagree which interleaves running of sut commands with checking the received results against the model (as opposed to running to completion first and then checking). Since the binding isn't relevant ATM, I suggest removing it.

The above changes are available on the revise-stm-thread-interfaces branch: https://github.com/jmid/multicoretests/tree/revise-stm-thread-interfaces along with

• the required adjustments to lockfree/ws_deque_test.ml and
• an update to an outdated comment I spotted

[jmid]

I made a few more changes yesterday which I've now pushed to https://github.com/jmid/multicoretests/tree/revise-stm-thread-interfaces

• I added a short documentation header to each module
• I tried dune build @doc and the spotted module Make (Spec : STM_base.STM_spec.Spec) : sig ... end which made me simplify the type-annotation in functor arguments
• I reverted to include Util so that users only have to open STM_base
• I updated the examples in doc/ to the new STM structure

Overall, I'm OK to merge this and then adjust it along the way.
The CI-logs reveal that bytecode fail consistently on a few Thread-tests.
This is to be expected at the Thread-mode is still flaky. I'm surprised that the Thread tests run as expected native code!

Questions I'm wondering about

• How do we limit the visibility of STM_internal for users?
• What is the advantage of having a basically empty STM_base with only module aliases?
• Should we inline STM_spec in STM_base avoid splitting into too many files?

I agree with @shym about squashing the commits down to a few key commits to clean up the history.
At 40+ commits spread among 3 contributors that sounds non-trivial unless we'll go for collapsing it down to one... 😬

[n-osborne]

I made a few more changes yesterday which I've now pushed to https://github.com/jmid/multicoretests/tree/revise-stm-thread-interfaces

* I added a short documentation header to each module

* I tried `dune build @doc` and the spotted `module Make (Spec : STM_base.STM_spec.Spec) : sig ... end` which made me simplify the type-annotation in functor arguments

* I reverted to `include Util` so that users only have to `open STM_base`

* I updated the examples in `doc/` to the new STM structure

Thanks ! I was not sure about the examples in doc/ (whether to keep the paper version or to update them).

Overall, I'm OK to merge this and then adjust it along the way. The CI-logs reveal that bytecode fail consistently on a few Thread-tests. This is to be expected at the Thread-mode is still flaky. I'm surprised that the Thread tests run as expected native code!

Questions I'm wondering about

* How do we limit the visibility of `STM_internal` for users?

We can't, because among these users, there are STM_sequential, STM_domain and STM_thread. The idea was that the name should be enough to tell the (human) users that the module shouldn't be used directly.

* What is the advantage of having a basically empty `STM_base` with only module aliases?

Dune was building this module anyway (IIRC), so we've (me and @shym) added it manually and included STM_Spec,

* Should we inline `STM_spec` in `STM_base` avoid splitting into too many files?

but now I think it is a good idea to inline it rather that include it.

I agree with @shym about squashing the commits down to a few key commits to clean up the history. At 40+ commits spread among 3 contributors that sounds non-trivial unless we'll go for collapsing it down to one... grimacing

My part is particularly messy (tried some refactoring that didn't work w.r.t avoiding the unnecessarily load of Stdlib.Thread, etc...).
I can try to clean it up a bit without breaking everything.

[jmid]

OK, thanks I commit the latest changes to n-osborne/stm-thread and let you know 👍

[jmid]

OK, I've now pushed my remaining commits from the other branch.

Is it OK with you @shym to start rebasing and squashing commits?

[shym]

As I was the one suggesting rewriting history, I can do it indeed ;-)

[shym]

About the visibility of STM_internal, we indeed cannot hide it. But I think we could use an alert to make a strong statement this should not be used lightly.

[jmid]

As I was the one suggesting rewriting history, I can do it indeed ;-)

You are welcome to!

[jmid]

I've taken a stab at cleaning up the history and squashing this morning.
It was not possible to split into the 3 commits suggested by @shym unless I started breaking up existing commits by @n-osborne. As this seemed a bit overkill I therefore squashed them all into a single co-authored commit.

I'll let the CI run and then plan to merge this afternoon.

[jmid]

Note: One cannot simply inline STM_spec into STM_base as STM_internal depends on the Spec module type, thus creating a cycle. One would therefore have to inline both files, perhaps renaming STM_internal.Make to Make_internal.
If we want to, we can do so in a separate PR.

[jmid]

The final CI tests hit weird behaviour:

• one MacOSX runner is sig KILL'ed during the install of ppx_lib (we've seen this before @shym haven't we?)
• another MacOSX runner timed out after 3 hours, during what I think was a src/lockfree/ws_deque_test.ml test run - with no output lines printed from the test in question - and with none of the previous tests taking particularly long to run... 🤔

[jmid]

In the interest of moving forward with the release I'll merge this PR.
Overall, I think we were just unfortunate with the last run - and that nothing more is broken than usual.
For example, #180 which builds on top of this PR has 4 successful MacOSX CI runs...
Ideally we should create issues and pursue the observed failures further:

• bytecode Thread tests fail as usual, since the bytecode interpreter is even less likely to interrupt Thread tests at the right wrong moment (I think)
• one bytecode test hit a segfault on the Ephemeron test on trunk https://github.com/jmid/multicoretests/actions/runs/3444725852/jobs/5747632136#step:8:851
• one MacOSX got killed during ppx_lib install after only 10min https://github.com/jmid/multicoretests/actions/runs/3444725851/jobs/5747632328#step:6:527
• another MacOSX run on beta1 timed out during what I think was a src/lockfree/ws_deque_test.ml
  https://github.com/jmid/multicoretests/actions/runs/3444725863/jobs/5747632278#step:8:768