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

STM: Catch exceptions in next_state for nicer UX #400

Merged
merged 10 commits into from
Oct 11, 2023
Merged

Conversation

jmid
Copy link
Collaborator

@jmid jmid commented Oct 9, 2023

In STM, the next_state function describes how the pure model description changes across each cmd.
As documented, ideally this function should be pure.

Surprises lurk when this is not the case, such as ocaml-gospel/ortac#150 points 1. and 3. since
next_state is run both

  • during generation in gen_cmds (sequential), gen_cmds_size (sequential/parallel), and gen_triple (parallel)
  • during precondition asserts cmds_ok (sequential) and all_interleavings_ok (parallel)

With no generated input to print this thus yields unhelpful error messages such as:

ERROR: uncaught exception in generator for test STM test exception during next_state parallel after 1000 steps:
Exception: Dune__exe__Stm_next_state_exc.Random_next_state_failure

This PR catches exceptions in next_state in these former cases, leaving exception raising to the sequential and parallel QCheck properties, where input can be printed and shrunk.

As a result, an end-user instead receives a minimal call sequence giving rise to the exception in both sequential mode:

   Add 96


exception Dune__exe__Stm_next_state_exc.Random_next_state_failure

and in parallel mode:

                        |                
                     Add 9090            
                        |                
             .---------------------.
             |                     |                


exception Dune__exe__Stm_next_state_exc.Random_next_state_failure

The PR furthermore

  • adds a regression test to the internal test suite
  • updates the documentation for the changed functions

@jmid
Copy link
Collaborator Author

jmid commented Oct 11, 2023

CI summary for c549513:

Out of 63 runs, 7 failed: 5 were genuine defects and 3 were test suite reliability related

@jmid
Copy link
Collaborator Author

jmid commented Oct 11, 2023

CI summary for 17514a4:

Out of 63 runs, 1 failed (a genuine defect)

None of the failures from the two runs are related to the PR, so I'll merge.

@jmid jmid merged commit d74e47a into main Oct 11, 2023
52 of 53 checks passed
@jmid jmid deleted the catch-next-state-exc branch October 11, 2023 08:15
@jmid
Copy link
Collaborator Author

jmid commented Oct 12, 2023

CI summary for merge to main:

Out of 38 runs 6 failed with 4 genuine issues and 2 borderline ones (asym, Cygwin threads)

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.

1 participant