multicoretests
multicoretests copied to clipboard
Unexpected STM Sys parallel test counterexample on s390x and ppc64le
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: