STM Out_channel test parallel failure #485
Description
The nightly runs triggered a test failure on Linux 5.1 on STM Out_channel test parallel
https://github.com/ocaml-multicore/multicoretests/actions/runs/11992644802/job/33432727512
random seed: 491672939
generated error fail pass / total time test name
[ ] 0 0 0 0 / 1000 0.0s STM Out_channel test sequential
[ ] 0 0 0 0 / 1000 0.0s STM Out_channel test sequential (generating)
[✓] 1000 0 0 1000 / 1000 0.3s STM Out_channel test sequential
[ ] 0 0 0 0 / 1000 0.0s STM Out_channel test parallel
[✗] 946 0 1 836 / 1000 26.0s STM Out_channel test parallel
--- Failure --------------------------------------------------------------------
Test STM Out_channel test parallel failed (0 shrink steps):
|
Set_buffered true
Set_binary_mode false
Output_char '3'
Pos
Is_buffered
Close_noerr
Set_binary_mode false
Open_text
Set_buffered false
Output_byte 5
Output_substring ("\133\017\197\130\... (truncated)
Output ("\242'\176\194\134!Z[\184u\2... (truncated)
Pos
Seek 8L
|
.----------------------------------------------------.
| |
Output_byte 2 Output ("\025\233;\000\176s[", 1, 2)
Set_buffered false Length
Output_string "\128" Pos
Seek 80L Close_noerr
Output_substring (",\000\242", 8, 65) Open_text
Output_substring ("a\130?\210\017Qp", 8, 9) Pos
+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Messages for test STM Out_channel test parallel:
Results incompatible with linearized model
|
Set_buffered true : Ok (())
Set_binary_mode false : Ok (())
Output_char '3' : Ok (())
Pos : Ok (1)
Is_buffered : Ok (true)
Close_noerr : Ok (())
Set_binary_mode false : Ok (())
Open_text : Ok (())
Set_buffered false : Ok (())
Output_byte 5 : Ok (())
Output_substring ("\133\017\197\130\... (truncated) : Ok (())
Output ("\242'\176\194\134!Z[\184u\2... (truncated) : Ok (())
Pos : Ok (13)
Seek 8L : Ok (())
|
.-------------------------------------------------------------------------------------------.
| |
Output_byte 2 : Error (Sys_error("Bad file descriptor")) Output ("\025\233;\000\176s[", 1, 2) : Ok (())
Set_buffered false : Ok (()) Length : Ok (13)
Output_string "\128" : Error (Sys_error("Bad file descriptor")) Pos : Ok (11)
Seek 80L : Error (Sys_error("Bad file descriptor")) Close_noerr : Ok (())
Output_substring (",\000\242", 8, 65) : Error (Invalid_argument("output_substring")) Open_text : Ok (())
Output_substring ("a\130?\210\017Qp", 8, 9) : Error (Invalid_argument("output_substring")) Pos : Ok (0)
================================================================================
failure (1 tests failed, 0 tests errored, ran 2 tests)
File "src/io/dune", line 40, characters 7-16:
40 | (name stm_tests)
^^^^^^^^^
(cd _build/default/src/io && ./stm_tests.exe --verbose)
Command exited with code 1.
I've scratched my head a bit over this.
Because of the truncation, it is not possible to see the entire strings in the 2 outputs at the end of the sequential prefix.
From what can be observed:
- It seems that the "left leg" behaviour can be explained by operating over a closed channel, i.e., in between the "right leg's"
Close_noerrandOpen_text. - All the observed exceptions seem acceptable by the model.
- There are no
flushoccurrences to trip up the model [ocaml5-issue]Out_channel.flushcan causeSyserrorwhen used in parallel #444
I'm suspecting that a non-printable/control character (null \000, backspace \008, del \127, ...) is tripping up the position/length logic of the model... 🤔