Skip to content

Initial STM precond fix, add Domainslib.Chan tests #67

New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Merged
merged 4 commits into from
May 18, 2022
Merged

Conversation

jmid
Copy link
Collaborator

@jmid jmid commented May 11, 2022

This PR provides an initial implementation STM precond support for parallel mode using a generate-and-filter approach.
Following Claessen-al:ICFP09 we keep only cmd list triples where all interleavings satisfy all preconditions.

The precond implementation is enough to get the second part running:
This part tests the Domainslib.Chan module. This requires precond to avoid

  • recv blocking on an empty channel
  • send blocking on a full channel

For the Domainslib.Chan tests, this means that we need to generate around twice as many triples as the test count.
I've also checked that the run time of the other STM tests is not affected noticably. For reference we now have the following STM tests:

src/atomic/atomic_test.ml
src/buffer/buffer_stm_test.ml           ;; expected to fail
src/domainslib/chan_tests.ml
src/lazy/lazy_stm_test.ml               ;; expected to fail
src/lockfree/ws_deque_test.ml
src/neg_tests/conclist_test.ml          ;; expected to fail
src/neg_tests/ref_test.ml               ;; expected to fail

Ping @n-osborne 👀

let rec check_obs pref cs1 cs2 s = match pref with
(* checks that all interleavings of a cmd triple satisfies all preconditions *)
let rec all_interleavings_ok pref cs1 cs2 s =
match pref with
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As the prefix is sequential, it should be valid by construction (?). So, do we really need to check it here or could we just compute the spawn_state?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point! 👍
From a generation perspective I completely agree.
From a shrinking perspective, I don't think we can be sure that the prefix continues to be valid precond-wise, e.g., if the cmd list shrinker removes cmds from the sequential prefix...

Such shrinking reminds me that it would be good to actually test that this combination works - a negative test (triggering shrinking) with a non-constant precond....

@jmid
Copy link
Collaborator Author

jmid commented May 15, 2022

Rerunning jobs as trunk has now been patched for the MacOS segfault.

@jmid jmid force-pushed the add-channel-tests branch from 703f2d2 to eb1846a Compare May 18, 2022 12:40
@jmid
Copy link
Collaborator Author

jmid commented May 18, 2022

Rebased on top of #63 - also bumping max_gen to 3 * count...

@jmid
Copy link
Collaborator Author

jmid commented May 18, 2022

Ran this manually on the MacMini also - 5 times.

  • 3 runs were all green
  • one run triggered the Buffer failure (first time on MacOS I think)
  • another run failed to trigger the expected 2 failures in src/lazy/lazy_stm_test.ml

The latter only runs 100 iterations though - so bumping this count to 200...

@jmid
Copy link
Collaborator Author

jmid commented May 18, 2022

Runs fine on manual MacOS tests - merging

@jmid jmid merged commit 8af9f80 into main May 18, 2022
@jmid jmid deleted the add-channel-tests branch May 18, 2022 16:48
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants