STM parallel Sys tests on macOS

[jmid]

The new shiny arm64 test runners turn on some red lights on the test suite.

In particular, the parallel STM tests of Sys had 2/3 macOS failures on yesterday's run for #324:
https://github.com/ocaml-multicore/multicoretests/pull/324/checks?check_run_id=14034561144
On 5.0 the test triggered a parallel issue - but on both 5.1 and 5.2 it didn't.

macOS arm64 5.1:
https://ocaml-multicoretests.ci.dev:8100/job/2023-06-06/085608-ci-ocluster-build-854d7c

random seed: 475469294
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    11.4s STM Sys test sequential

[ ]    0    0    0    0 / 1000     0.0s STM Sys test parallel
[ ]  169    0    0  169 / 1000    48.7s STM Sys test parallel
[ ]  380    0    0  380 / 1000   108.7s STM Sys test parallel
[ ]  587    0    0  587 / 1000   168.7s STM Sys test parallel
[ ]  795    0    0  795 / 1000   228.8s STM Sys test parallel
[✗] 1000    0    0 1000 / 1000   288.0s STM Sys test parallel

--- Failure --------------------------------------------------------------------

Test STM Sys test parallel failed:

Negative test STM Sys test parallel succeeded but was expected to fail
================================================================================
failure (1 tests failed, 0 tests errored, ran 2 tests)

macOS arm64 5.2
https://ocaml-multicoretests.ci.dev:8100/job/2023-06-06/085608-ci-ocluster-build-637e23

random seed: 306002888
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    11.5s STM Sys test sequential

[ ]    0    0    0    0 / 1000     0.0s STM Sys test parallel
[ ]  169    0    0  169 / 1000    48.8s STM Sys test parallel
[ ]  376    0    0  376 / 1000   108.9s STM Sys test parallel
[ ]  581    0    0  581 / 1000   169.1s STM Sys test parallel
[ ]  792    0    0  792 / 1000   229.3s STM Sys test parallel
[ ]  997    0    0  997 / 1000   289.4s STM Sys test parallel
[✗] 1000    0    0 1000 / 1000   290.5s STM Sys test parallel

--- Failure --------------------------------------------------------------------

Test STM Sys test parallel failed:

Negative test STM Sys test parallel succeeded but was expected to fail
================================================================================
failure (1 tests failed, 0 tests errored, ran 2 tests)

I'm hoping this may be solved by #304 that extends the Sys surface covered - and hence the potential parallel issues triggered.

[jmid]

I realized now that we are considering this a positive test on Linux (with a reduced count of 200), which also explains why this is only an issue under macOS arm64:

multicoretests/src/sys/stm_tests.ml

Lines 317 to 332 in 6a549cd

	let uname_os () =
	let ic = Unix.open_process_in "uname -s" in
	let os = In_channel.input_line ic in
	ignore (Unix.close_process_in ic);
	os
	module Sys_seq = STM_sequential.Make(SConf)
	module Sys_dom = STM_domain.Make(SConf)
	;;
	QCheck_base_runner.run_tests_main [
	Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential";
	if Sys.unix && uname_os () = Some "Linux"
	then Sys_dom.agree_test_par ~count:200 ~name:"STM Sys test parallel"
	else Sys_dom.neg_agree_test_par ~count:1000 ~name:"STM Sys test parallel"
	]

Here's an branch to do the same on arm64:
https://github.com/ocaml-multicore/multicoretests/tree/sys-tests-on-arm64

[jmid]

Reopening, as the merge of #405 to main found an unexpected counterexample - and thus made the positive test fail.

[jmid]

On a scheduled GitHub actions workflow testing 5.1.1 (amd64 - not ARM) this found an unexpected counterexample:
https://github.com/ocaml-multicore/multicoretests/actions/runs/8585619722/job/23527213449

random seed: 518817204
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     8.0s STM Out_channel test sequential

[ ]    0    0    0    0 / 1000     0.0s STM Out_channel test parallel
[ ] 1126    0    0  996 / 1000    53.6s STM Out_channel test parallel (shrinking:    0.0005)
[✗] 1127    0    1  996 / 1000    77.1s STM Out_channel test parallel

--- Failure --------------------------------------------------------------------

Test STM Out_channel test parallel failed (0 shrink steps):

                                                              |                         
                                                           Length                       
                                     Output ("U\030M\235\r\016(\216\194Z1... (truncated)
                                                    Output_string "\195"                
                                               Output ("n\146\203\204", 5, 98)          
                                                         Is_buffered                    
                                                           Length                       
                                            Output ("nh\t7\007\250~v\023", 5, 4)        
                                                    Set_binary_mode true                
                                                         Close_noerr                    
                                                            Flush                       
                                                        Output_byte 2                   
                                     Output_bytes "c\019dG\015\243\145\15... (truncated)
                                                  Output ("\020\197", 5, 8)             
                                                          Open_text                     
                                                           Length                       
                                                 Output_bytes "{\217\128Cg"             
                                                             Pos                        
                                                    Set_binary_mode false               
                                                              |                         
                                   .----------------------------------------------------.
                                   |                                                    |                         
                                 Flush                                               Length                       
                                Seek 9L                                          Output_char 'k'                  
                              Is_buffered                            Output_substring ("\243j\163", 81, 74)       
                          Set_buffered false                                          Flush                       
                              Close_noerr                                Output_substring ("@Wi", 9, 39)          
                                 Flush                                          Set_buffered true                 
                                 Close                                                 Pos                        
                               Open_text                                           Is_buffered                    
                               Seek 77L                                  Output ("\129\178Q\181 ", 3, 5)          
                             Output_byte 0                                        Output_byte 8                   
                           Set_buffered true                                  Set_binary_mode false               
                                                                                       Pos                        


+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test STM Out_channel test parallel:

  Results incompatible with linearized model

                                                                                                   |                                               
                                                                                            Length : Ok (0)                                        
                                                                     Output ("U\030M\235\r\016(\216\194Z1... (truncated) : Ok (())                 
                                                                                     Output_string "\195" : Ok (())                                
                                                                  Output ("n\146\203\204", 5, 98) : Error (Invalid_argument("output"))             
                                                                                        Is_buffered : Ok (true)                                    
                                                                                            Length : Ok (0)                                        
                                                                             Output ("nh\t7\007\250~v\023", 5, 4) : Ok (())                        
                                                                                     Set_binary_mode true : Ok (())                                
                                                                                         Close_noerr : Ok (())                                     
                                                                                            Flush : Ok (())                                        
                                                                        Output_byte 2 : Error (Sys_error("Bad file descriptor"))                   
                                                     Output_bytes "c\019dG\015\243\145\15... (truncated) : Error (Sys_error("Bad file descriptor"))
                                                                     Output ("\020\197", 5, 8) : Error (Invalid_argument("output"))                
                                                                                          Open_text : Ok (())                                      
                                                                                            Length : Ok (0)                                        
                                                                                  Output_bytes "{\217\128Cg" : Ok (())                             
                                                                                              Pos : Ok (5)                                         
                                                                                    Set_binary_mode false : Ok (())                                
                                                                                                   |                                               
                                                   .-----------------------------------------------------------------------------------------------.
                                                   |                                                                                               |                                               
                                            Flush : Ok (())                                                                                 Length : Ok (0)                                        
                                           Seek 9L : Ok (())                                                                           Output_char 'k' : Ok (())                                   
                                        Is_buffered : Ok (true)                                          Output_substring ("\243j\163", 81, 74) : Error (Invalid_argument("output_substring"))     
                                      Set_buffered false : Ok (())                                                          Flush : Error (Sys_error("Bad file descriptor"))                       
                                         Close_noerr : Ok (())                                               Output_substring ("@Wi", 9, 39) : Error (Invalid_argument("output_substring"))        
                                            Flush : Ok (())                                                                           Set_buffered true : Ok (())                                  
                                            Close : Ok (())                                                                                 Pos : Ok (65536)                                       
                                          Open_text : Ok (())                                                                           Is_buffered : Ok (true)                                    
                                           Seek 77L : Ok (())                                                     Output ("\129\178Q\181 ", 3, 5) : Error (Invalid_argument("output"))             
                                        Output_byte 0 : Ok (())                                                         Output_byte 8 : Error (Sys_error("Bad file descriptor"))                   
                                      Set_buffered true : Ok (())                                                                   Set_binary_mode false : Ok (())                                
                                                                                                                                            Pos : Ok (65536)                                       

================================================================================
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.