search

ocaml-multicore / multicoretests

PBT testsuite and libraries for testing multicore OCaml
https://ocaml-multicore.github.io/multicoretests/
BSD 2-Clause "Simplified" License
37 stars 16 forks source link

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

Open jmid opened 2 months ago

jmid commented 2 months ago

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... :smile:

jmid commented 1 week ago

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.