STM Out_channel test parallel failure

[jmid]

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_noerr and Open_text.
• All the observed exceptions seem acceptable by the model.
• There are no flush occurrences to trip up the model #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... :thinking: