[ocaml5-issue] Out_channel.flush can cause Syserror when used in parallel #444
Open
Description
A Cygwin 5.2 run triggered when merging #443 to main found an unexpected counterexample to STM Out_channel parallel:
https://github.com/ocaml-multicore/multicoretests/actions/runs/8361686850/job/22890359851
random seed: 292949458
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 2.9s STM Out_channel test sequential
[ ] 0 0 0 0 / 1000 0.0s STM Out_channel test parallel
[ ] 620 0 0 542 / 1000 57.1s STM Out_channel test parallel
[ ] 1116 0 0 966 / 1000 117.5s STM Out_channel test parallel (shrinking: 1.0011)
[✗] 1117 0 1 966 / 1000 129.8s STM Out_channel test parallel
--- Failure --------------------------------------------------------------------
Test STM Out_channel test parallel failed (1 shrink steps):
|
Output_substring ("\225\185!\188Q\142\138", 0, 96)
Output_byte 36
Output_bytes "\158\199e\220\253\148\... (truncated)
Flush
Close
Output ("Z\197j", 3, 3)
Open_text
Is_buffered
Set_binary_mode false
Output_substring ("{8)g", 18, 1)
Length
Close_noerr
Open_text
Set_buffered true
|
.----------------------------------------------------.
| |
Close_noerr Set_binary_mode true
Open_text Pos
Output_substring ("\to\128N\186", 7, 6) Set_binary_mode true
Output_char '9' Output_byte 54
Set_binary_mode true Length
Output_bytes "\182U" Flush
Output_char '5' Output_substring ("\014\236\187\146^... (truncated)
Output ("(|$\217\203\206\162t\235", 18, 4) Set_binary_mode true
Pos Is_buffered
Set_binary_mode false Output_byte 1
+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Messages for test STM Out_channel test parallel:
Results incompatible with linearized model
|
Output_substring ("\225\185!\188Q\142\138", 0, 96) : Error (Invalid_argument("output_substring"))
Output_byte 36 : Ok (())
Output_bytes "\158\199e\220\253\148\... (truncated) : Ok (())
Flush : Ok (())
Close : Ok (())
Output ("Z\197j", 3, 3) : Error (Invalid_argument("output"))
Open_text : Ok (())
Is_buffered : Ok (true)
Set_binary_mode false : Ok (())
Output_substring ("{8)g", 18, 1) : Error (Invalid_argument("output_substring"))
Length : Ok (0)
Close_noerr : Ok (())
Open_text : Ok (())
Set_buffered true : Ok (())
|
.--------------------------------------------------------------------------------------------------.
| |
Close_noerr : Ok (()) Set_binary_mode true : Ok (())
Open_text : Ok (()) Pos : Ok (0)
Output_substring ("\to\128N\186", 7, 6) : Error (Invalid_argument("output_substring")) Set_binary_mode true : Ok (())
Output_char '9' : Ok (()) Output_byte 54 : Ok (())
Set_binary_mode true : Ok (()) Length : Ok (0)
Output_bytes "\182U" : Ok (()) Flush : Error (Sys_error("Bad file descriptor"))
Output_char '5' : Ok (()) Output_substring ("\014\236\187\146^... (truncated) : Ok (())
Output ("(|$\217\203\206\162t\235", 18, 4) : Error (Invalid_argument("output")) Set_binary_mode true : Error (Sys_error("Bad file descriptor"))
Pos : Ok (4) Is_buffered : Ok (true)
Set_binary_mode false : Ok (()) Output_byte 1 : Ok (())
================================================================================
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.
AFAICS, the failure can be explained by Flush in the "right leg" causing Sys_error("Bad file descriptor").
This goes against the specification, which says:
val close : t -> unit
Close the given channel, flushing all buffered write operations. Output functions raise a Sys_error exception when they are applied to a closed output
channel, except Out_channel.close and Out_channel.flush , which do nothing when applied to an already closed channel. [...]
This is currently captured in the STM Out_channel test as:
| Flush, Res ((Result (Unit,Exn),_), r) ->
(match s,r with
| Closed, Error (Sys_error _) -> false (* should not generate an error *)
| Closed, Ok () -> true
| Open _, Ok () -> true
| _ -> false)