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

Improve reporting in Dynarray lin test #529

Closed

Conversation

OlivierNicole
Copy link
Contributor

By raising an exception rather than aborting the program. This should help with #528 when the bug surfaces again.

By raising an exception rather than aborting the program.
@jmid
Copy link
Collaborator

jmid commented Jan 27, 2025

Thanks! Unfortunately I don't think this will make a big difference in helping uncover the bug.
To illustrate, I've patched the Lin Dynarray test specification to always fail:

diff --git a/src/dynarray/lin_tests.ml b/src/dynarray/lin_tests.ml
index 33680a0b..54982172 100644
--- a/src/dynarray/lin_tests.ml
+++ b/src/dynarray/lin_tests.ml
@@ -10,7 +10,7 @@ module Dynarray_api = struct
 
   let get_check a i =
     let v = Dynarray.get a i in
-    if not (Obj.is_int (Obj.repr v)) then (Printf.eprintf "dummy found!\n%!"; exit 1) else v
+    if (*not (Obj.is_int (Obj.repr v))*) true then failwith "dummy found!" else v
 
   let api =
     (*let int_not_too_big = int_bound 2048 in*)

With this patch, the test always fails on the first Lin input generated (they all contain a get I guess), however after shrinking I have yet to see one with get in its reported counterexample:

$ dune exec src/dynarray/lin_tests.exe -- -v
random seed: 497616361
generated error fail pass / total     time test name
[✓]    1    0    1    0 / 1000     1.5s Lin Dynarray test with Domain
[✓] 1000    0    0 1000 / 1000     3.1s Lin Dynarray stress test with Domain

--- Info -----------------------------------------------------------------------

Negative test Lin Dynarray test with Domain failed as expected (27 shrink steps):

                              |          
                              |          
                   .---------------------.
                   |                     |          
                reset t         append_seq t <0; 0> 


+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test Lin Dynarray test with Domain:

  Results incompatible with sequential execution

                                                                 |                              
                                                                 |                              
                                  .-------------------------------------------------------------.
                                  |                                                             |                              
                          reset t : Ok (())                        append_seq t <0; 0> : Error (Invalid_argument("Array.blit"))

================================================================================
success (ran 2 tests)
  • for the negative parallel Lin test, get may indeed raise an exception (Lin doesn't let us express which ones are OK and which are not) and
  • for the parallel Lin stress test, get is therefore only raising an exception (as expected) and thus passing that test.

Overall, as a result this could potentially hide occurrences of the bug!

As you've earlier suggested on #528, I think the best option is to try reproducing with an STM test that allows to specify acceptable behaviour more specifically... 🤔

@OlivierNicole
Copy link
Contributor Author

Right, I see how that couldn’t work! I have botched up the STM test to make it closer to the Lin test that uncovered the bug here: https://github.com/OlivierNicole/multicoretests/tree/track-dynarray-bug and am now trying to reproduce the bug.

@OlivierNicole
Copy link
Contributor Author

Closing as there is no clear change that can be included into the main branch at this point.

@OlivierNicole OlivierNicole deleted the better_dynarray_test branch January 29, 2025 09:26
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