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 random tests generator #15

Open
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

art-w
Copy link

@art-w art-w commented Feb 26, 2023

An attempt at improving the test coverage:

  1. Randomly generate a little program that do atomic operations
  2. Run this program with a random scheduler to sample the possible values that the atomics can hold after execution
  3. Run it again with dscheck and check that it can find all of those outcomes (otherwise it means that dscheck wrongly skipped a branch)
  4. goto 1

Currently this is all a bit cheap! The program generator could produce more interesting logic. The random sampling is also super naïve since it favors "easy to find" outcomes, but that seems exhaustive enough at the moment (since dscheck rarely discovers more endings, the programs are too simple to hide anything).

I initially wrote this to test #3 but haven't found any bugs yet. I did confirm that it would have found the issues in the previous version of this PR :) What I did not expect is that it also produces broken programs on main, I thought this branch was super exhaustive and rock solid. I've extracted the buggy cases in a new testsuite if someone wants to take a look, it's a bit weird.

@art-w art-w mentioned this pull request Mar 23, 2023
@bartoszmodelski
Copy link
Contributor

This looks good. Our current test-suite is too small and mostly covers positive cases, while experience shows that we should focus on negative ones. Auto-generation is a nice shortcut for that, and we can always move useful tests to the permanent testsuite.

Is there a way to stop it from generating operations inside the main thread? It's really a place for declaration of domains and final assertions, and tracing is off there. Likewise for nested spawns (although this one we should fix at some point).

@art-w
Copy link
Author

art-w commented Apr 5, 2023

Hm yeah, we could pass some arguments to gen_expr to indicate if we are at the root or within a spawn and generate different stuff... but I think the cases you mention should be fixed in the scheduler if they are causing any issues, it's too easy to trip on them :P

@bartoszmodelski bartoszmodelski mentioned this pull request Apr 17, 2023
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