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

Reduce STM.cmds_gen list size #472

Merged
merged 5 commits into from
Sep 17, 2024
Merged

Reduce STM.cmds_gen list size #472

merged 5 commits into from
Sep 17, 2024

Conversation

jmid
Copy link
Collaborator

@jmid jmid commented Aug 30, 2024

STM_sequential uses Gen.sized to generate cmd lists, which means the output size depends on Gen.nat, which may output lists of up size 10.000 with a 5% chance.

Here's are some quick stats to illustrate, here on the Domain.DLS STM test:

multicoretests-latest$ dune exec src/domain/stm_tests_dls.exe -- -v
random seed: 245423950
generated error fail pass / total     time test name
[✓] 1000    0    0 1000 / 1000     0.5s STM Domain.DLS test sequential

+++ Stats for STM Domain.DLS test sequential ++++++++++++++++++++++++++++++++++++++++++++++++++++++++

stats cmd length:
  num: 1000, avg: 364.61, stddev: 1267.28, median 9, min 0, max 9737
     0.. 486: #######################################################         856
   487.. 973: ######                                                           94
   974..1460:                                                                   4
  1461..1947:                                                                   2
  1948..2434:                                                                   5
  2435..2921:                                                                   4
  2922..3408:                                                                   2
  3409..3895:                                                                   2
  3896..4382:                                                                   2
  4383..4869:                                                                   4
  4870..5356:                                                                   2
  5357..5843:                                                                   6
  5844..6330:                                                                   0
  6331..6817:                                                                   2
  6818..7304:                                                                   3
  7305..7791:                                                                   2
  7792..8278:                                                                   0
  8279..8765:                                                                   1
  8766..9252:                                                                   4
  9253..9739:                                                                   5
================================================================================
success (ran 1 tests)

A cmd list of length 9737 is excessive - and now hurts client users of the library, such as Ortac's QCheck-STM plugin!

This PR therefore proposes to replace the distribution with an exponential distribution instead.

For a start I've gone with a mean of 10, and added a bit of skew to avoid generating too many empty cmd lists, which should be less interesting in a state-machine setup. The resulting distribution looks as follows (now with count raised to 10000, and a 230/10000 ~ 2.3% chance of generating empty cmd lists which seems reasonable):

multicoretests-latest$ dune exec src/domain/stm_tests_dls.exe -- -v
random seed: 7625658
generated error  fail  pass / total     time test name
[✓] 10000     0     0 10000 / 10000    15.3s STM Domain.DLS test sequential

+++ Collect ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Collect results for test STM Domain.DLS test sequential:

not mt: 9770 cases
empty : 230 cases

+++ Stats for STM Domain.DLS test sequential ++++++++++++++++++++++++++++++++++++++++++++++++++++++++

stats cmd length:
  num: 10000, avg: 10.27, stddev: 9.95, median 7, min 0, max 79
   0.. 3: #######################################################        2749
   4.. 7: ################################################               2417
   8..11: ###############################                                1568
  12..15: #####################                                          1095
  16..19: ##############                                                  706
  20..23: #########                                                       453
  24..27: ######                                                          314
  28..31: ####                                                            248
  32..35: ##                                                              147
  36..39: ##                                                              116
  40..43: #                                                                62
  44..47:                                                                  39
  48..51:                                                                  24
  52..55:                                                                  28
  56..59:                                                                  14
  60..63:                                                                   9
  64..67:                                                                   4
  68..71:                                                                   3
  72..75:                                                                   2
  76..79:                                                                   2
================================================================================
success (ran 1 tests)

I'm curious to see how this fares on the CI.

Shoutout to @nikolaushuber for reporting this.

Note to self: might warrant a changelog entry.

@jmid
Copy link
Collaborator Author

jmid commented Sep 2, 2024

CI summary for d950ed0: all 45 workflows completed succesfully!

@jmid jmid force-pushed the stm-cmd-list-dist branch from d950ed0 to 65edac1 Compare September 2, 2024 07:47
@jmid
Copy link
Collaborator Author

jmid commented Sep 2, 2024

CI summary for 65edac1: all 45 workflows completed succesfully!

@jmid jmid force-pushed the stm-cmd-list-dist branch from 65edac1 to a661f27 Compare September 17, 2024 08:11
@jmid
Copy link
Collaborator Author

jmid commented Sep 17, 2024

CI summary for a661f27: all 45 workflows completed succesfully!

Merging...

@jmid jmid merged commit b0e1b30 into main Sep 17, 2024
42 checks passed
@jmid jmid deleted the stm-cmd-list-dist branch September 17, 2024 11:15
@jmid
Copy link
Collaborator Author

jmid commented Sep 18, 2024

CI summary for merge to main:

Out of 46 workflows 1 failed with a CI issue

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