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

Unexpected STM Sys parallel test counterexample on s390x and ppc64le #466

Open
jmid opened this issue Jul 5, 2024 · 1 comment
Open
Labels
test suite reliability Issue concerns tests that should behave more predictably

Comments

@jmid
Copy link
Collaborator

jmid commented Jul 5, 2024

The STM Sys test parallel test on s390x with OCaml 5.1.0 found an unexpected counterexample:
https://ocaml-multicoretests.ci.dev:8100/job/2024-07-05/135811-ci-ocluster-build-a950ab

random seed: 462089430
generated error fail pass / total     time test name

[ ]    0    0    0    0 / 1000     0.0s STM Sys test sequential
[ ]    0    0    0    0 / 1000     0.0s STM Sys test sequential (generating)
[✓] 1000    0    0 1000 / 1000     1.5s STM Sys test sequential

[ ]    0    0    0    0 /  200     0.0s STM Sys test parallel
[✗]   58    0    1   57 /  200    10.3s STM Sys test parallel

[ ]    0    0    0    0 / 1000     0.0s STM Sys stress test parallel
[ ]  750    0    0  750 / 1000    48.5s STM Sys stress test parallel
[✓] 1000    0    0 1000 / 1000    63.1s STM Sys stress test parallel

--- Failure --------------------------------------------------------------------

Test STM Sys test parallel failed (4 shrink steps):

                                                              |                         
                                                         Readdir []                     
                                                 File_exists ["ccc"; "ddd"]             
                                     Mkfile (["ccc"; "ccc"; "ccc"; "bbb";... (truncated)
                                                      Mkdir ([], "ddd")                 
                                                     Mkfile ([], "aaa")                 
                                     Mkfile (["ccc"; "bbb"; "eee"; "eee";... (truncated)
                                                     File_exists ["ddd"]                
                                                      Mkdir ([], "eee")                 
                                                     Mkfile ([], "ddd")                 
                                                              |                         
                                   .----------------------------------------------------.
                                   |                                                    |                         
                              Readdir []                              Rmdir (["ccc"; "ccc"; "aaa"], "ddd")        
                            Readdir ["eee"]                                     Mkdir ([], "aaa")                 
                            Readdir ["bbb"]                                     Rmdir ([], "eee")                 
                           Rmdir ([], "eee")                   Mkfile (["bbb"; "aaa"; "ccc"; "bbb";... (truncated)
                           Mkdir ([], "aaa")                                    Mkdir ([], "bbb")                 
                           Rmdir ([], "ddd")                                    Rmdir ([], "ddd")                 
                                                                      Readdir ["aaa"; "aaa"; "ddd"; "ddd"]        


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

Messages for test STM Sys test parallel:

  Results incompatible with linearized model

                                                                                                                                           |                                                                   
                                                                                                                                 Readdir [] : Ok ([||])                                                        
                                                                                                                           File_exists ["ccc"; "ddd"] : false                                                  
                                                                         Mkfile (["ccc"; "ccc"; "ccc"; "bbb";... (truncated) : Error (Sys_error("_sandbox/ccc/ccc/ccc/bbb/bbb/bbb: No such file or directory"))
                                                                                                                              Mkdir ([], "ddd") : Ok (())                                                      
                                                                                                                              Mkfile ([], "aaa") : Ok (())                                                     
                                                                         Mkfile (["ccc"; "bbb"; "eee"; "eee";... (truncated) : Error (Sys_error("_sandbox/ccc/bbb/eee/eee/aaa/ccc: No such file or directory"))
                                                                                                                               File_exists ["ddd"] : true                                                      
                                                                                                                              Mkdir ([], "eee") : Ok (())                                                      
                                                                                                          Mkfile ([], "ddd") : Error (Sys_error("_sandbox/ddd: File exists"))                                  
                                                                                                                                           |                                                                   
                                                                       .---------------------------------------------------------------------------------------------------------------------------------------.
                                                                       |                                                                                                                                       |                                                                   
                                                          Readdir [] : Ok ([|"aaa"|])                                                                   Rmdir (["ccc"; "ccc"; "aaa"], "ddd") : Error (Sys_error("_sandbox/ccc/ccc/aaa/ddd: No such file or directory"))            
                                 Readdir ["eee"] : Error (Sys_error("_sandbox/eee: No such file or directory"))                                                                Mkdir ([], "aaa") : Error (Sys_error("_sandbox/aaa: File exists"))                                  
                                                          Readdir ["bbb"] : Ok ([||])                                                                                                             Rmdir ([], "eee") : Ok (())                                                      
                                Rmdir ([], "eee") : Error (Sys_error("_sandbox/eee: No such file or directory"))                             Mkfile (["bbb"; "aaa"; "ccc"; "bbb";... (truncated) : Error (Sys_error("_sandbox/bbb/aaa/ccc/bbb/eee/ddd: No such file or directory"))
                                       Mkdir ([], "aaa") : Error (Sys_error("_sandbox/aaa: File exists"))                                                                                         Mkdir ([], "bbb") : Ok (())                                                      
                                Rmdir ([], "ddd") : Error (Sys_error("_sandbox/ddd: No such file or directory"))                                                                                  Rmdir ([], "ddd") : Ok (())                                                      
                                                                                                                                                             Readdir ["aaa"; "aaa"; "ddd"; "ddd"] : Error (Sys_error("_sandbox/aaa/aaa/ddd/ddd: Not a directory"))                 

================================================================================
failure (1 tests failed, 0 tests errored, ran 3 tests)
File "src/sys/dune", line 4, characters 7-16:
4 |  (name stm_tests)
           ^^^^^^^^^
(cd _build/default/src/sys && ./stm_tests.exe --verbose)
Command exited with code 1.

Currently we consider the test positive on Linux and run only 200 iterations.
As such, it should be commended to find a counterexample in only 58 attempts... 😄

@jmid jmid added the test suite reliability Issue concerns tests that should behave more predictably label Jul 5, 2024
@jmid jmid changed the title Unexpected STM Sys test parallel test counterexample on s390x Unexpected STM Sys parallel test counterexample on s390x Jul 5, 2024
@jmid
Copy link
Collaborator Author

jmid commented Sep 3, 2024

Saw this on ppc64le 5.2 too in #469
https://ocaml-multicoretests.ci.dev:8100/job/2024-09-03/111022-ci-ocluster-build-4bdab6

random seed: 461619666
generated error fail pass / total     time test name

[ ]    0    0    0    0 / 1000     0.0s STM Sys test sequential
[ ]    0    0    0    0 / 1000     0.0s STM Sys test sequential (generating)
[✓] 1000    0    0 1000 / 1000     3.9s STM Sys test sequential

[ ]    0    0    0    0 /  200     0.0s STM Sys test parallel
[ ]   50    0    0   50 /  200    63.4s STM Sys test parallel (shrinking:    3.0003)
[ ]   50    0    0   50 /  200   124.1s STM Sys test parallel (shrinking:    7.0002)
[✗]   51    0    1   50 /  200   180.0s STM Sys test parallel

[ ]    0    0    0    0 / 1000     0.0s STM Sys stress test parallel
[ ]   27    0    0   27 / 1000     4.1s STM Sys stress test parallel
[ ]  514    0    0  514 / 1000    64.2s STM Sys stress test parallel
[ ]  953    0    0  953 / 1000   124.2s STM Sys stress test parallel
[✓] 1000    0    0 1000 / 1000   129.3s STM Sys stress test parallel

--- Failure --------------------------------------------------------------------

Test STM Sys test parallel failed (28 shrink steps):

                             |           
                     Mkdir ([], "eee")   
                             |           
                  .---------------------.
                  |                     |           
             Readdir []         Mkdir ([], "ddd")   
                                Rmdir ([], "eee")   


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

Messages for test STM Sys test parallel:

  Results incompatible with linearized model

                                     |                     
                        Mkdir ([], "eee") : Ok (())        
                                     |                     
                  .------------------------------------.
                  |                                    |                     
       Readdir [] : Ok ([||])             Mkdir ([], "ddd") : Ok (())        
                                          Rmdir ([], "eee") : Ok (())        

================================================================================
failure (1 tests failed, 0 tests errored, ran 3 tests)
File "src/sys/dune", line 4, characters 7-16:
4 |  (name stm_tests)
           ^^^^^^^^^
(cd _build/default/src/sys && ./stm_tests.exe --verbose)
Command exited with code 1.

@jmid jmid changed the title Unexpected STM Sys parallel test counterexample on s390x Unexpected STM Sys parallel test counterexample on s390x and ppc64le Sep 3, 2024
@jmid jmid mentioned this issue Sep 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
test suite reliability Issue concerns tests that should behave more predictably
Projects
None yet
Development

No branches or pull requests

1 participant