Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Add Lin Domain.DLS test #392

Merged
merged 4 commits into from
Sep 12, 2023
Merged

Add Lin Domain.DLS test #392

merged 4 commits into from
Sep 12, 2023

Conversation

jmid
Copy link
Collaborator

@jmid jmid commented Sep 7, 2023

This PR adds a quick Lin stress test of Domain.DLS.

It uses only one DLS.key for a start - not impressive but it is a start.
We might revisit it based on multiple-ts or consider replacing it by an STM test later.

Without the optional ~split_from_parent the child domain does not inherit the key, which makes for a fast negative test.
I did notice that the test takes longer and longer as it progresses, which may be due to the inability to remove DSL.keys again. For this reason, it seems faster to run the negative test first...
We might consider (a) running the property/test in child domain or (b) splitting the two tests to run in separate processes.

Copy link
Collaborator

@shym shym left a comment

Choose a reason for hiding this comment

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

Nice little test!
As keys cannot be freed and as new_key is really only called from init, it might make sense to use a constant key? 🤔 Or allocate a list of keys initially and pick one of them in init?

@jmid
Copy link
Collaborator Author

jmid commented Sep 11, 2023

I grew increasingly unhappy with the short-comings the initial version, and therefore set out to write an STM test addressing some of them in ef4b42d.

The resulting STM test

  • runs the two test properties in a child Domain (to avoid Domain.DLS polution across repetitions) and
  • allocates an initial list of keys as suggested

I also adjusted the Util.repeat and retries parameters as a lot repetition didn't seem necessary to trigger it, and since I needed to write out the properties anyway to run the test properties in a child Domain.

This results in a negative test, that is quickly able to produce a counterexample where simultanious changes in two children are not seen in the sibling:

  Results incompatible with linearized model

                               |                           
                               |                           
            .------------------------------------.
            |                                    |                           
     Set (2, 1) : ()                      Set (0, 43) : ()                   
        Get 0 : 0                            Get 2 : 2            

@jmid jmid force-pushed the add-domain-dls-tests branch from ae5ad69 to dd95793 Compare September 11, 2023 13:08
@jmid
Copy link
Collaborator Author

jmid commented Sep 11, 2023

A round of focused tests confirmed that the STM Domain.DLS test runs fast and works reasonable well.
I've therefore disabled the initial Lin test.

I expect this full CI run to fail its trunk workflows without #12545 merged into ocaml/ocaml.

@jmid
Copy link
Collaborator Author

jmid commented Sep 12, 2023

CI summary

Out of 59 workflows and 19 failures, the 2 non-trunk failures were thus genuine.
I'll merge.

@jmid jmid merged commit 9149a8f into main Sep 12, 2023
@jmid jmid deleted the add-domain-dls-tests branch September 12, 2023 08:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants