Add STM Array tearing test

[jmid]

This is the STM Array tearing test mentioned in #528 (comment)

As mentioned there, this is written as a separate STM test to not "just" trigger sequential consistency counterexamples, but instead test for powers-of-2, without the need for a model (read: sans model updates).

The test is in a decent state ATM. The last focused run with 50 repetitions triggered 14 and 23 counterexamples on the two musl workflows - a much better error rate than the Lin Dynarray misbehaving test we started with... 🙂

I'm still considering @gasche's idea of using an option element type though, as tearing of those would generally lead to invalid pointers - and therefore a likely crash.

[jmid]

Note: the fix has now been merged to trunk (5.5) and cherry picked to (the forthcoming) 5.4: ocaml/ocaml#13950

The test should probably be disabled on ocaml.5.3 and below though...

[jmid]

Ah, so the musl.5.3 workflow triggered a test failure, where copy observed tearing when run in parallel with sort
(the other 35 workflows passed):

random seed: 469412481
generated error fail pass / total     time test name

[ ]    0    0    0    0 / 1000     0.0s STM Array test sequential
[ ]    0    0    0    0 / 1000     0.0s STM Array test sequential (generating)
[✓] 1000    0    0 1000 / 1000     0.0s STM Array test sequential

[ ]    0    0    0    0 / 1000     0.0s STM Array test parallel
[✓]    1    0    1    0 / 1000     5.0s STM Array test parallel

[ ]    0    0    0    0 / 1000     0.0s STM Array test tearing parallel
[✗]  699    0    1  698 / 1000    18.1s STM Array test tearing parallel

[...]

  Results incompatible with linearized model

                                                                     |                                
                                                               Get 3 : Ok (1)                         
                                                               Get 8 : Ok (1)                         
                                                     Set (1, 35184372088832) : Ok (())                
                                                                     |                                
                                    .-----------------------------------------------------------------.
                                    |                                                                 |                                
                              Fast_sort : ()                                                      Sort : ()                            
                         Sub (2, 1) : Ok ([|1|])                                                Get 1 : Ok (1)                         
                               Length : 10                                                      Get 1 : Ok (1)                         
           Copy : [|1; 1; 35184372088833; 1; 1; 1; 1; 1; 1; 0|]                                   Sort : ()                            
                       Mem 281474976710656 : false                     Fill (8, 4, 1073741824) : Error (Invalid_argument("Array.fill"))
       Exists ({35184372088832 -> false; 1 ... (truncated) : false        Exists ({268435456 -> false; 1 -> tr... (truncated) : true   
                       Set (0, 268435456) : Ok (())                                         Mem 4294967296 : false                     

There's a lot of visual noise in this counterexample, as only 1-2 1-bits give rise to a slew of decimal digits.
I'm pushing a revision where elements are instead printed in hexadecimal.

[jmid]

CI summary for 28e142a: all 36 workflows passed (i.e., no tearing was triggered on musl.5.3)

I'm pushing a couple of other commits:

• to reuse power_of_2s for both generation and postcond_tear
• to add the tearing issue to the README

[jmid]

Tearing triggered again and illustrates the less noisy hex printing of elements.
Here Array.copy observes 0x0 presumably because the individual bytes of the entry a copied individually in parallel with the mutating stable_sort:

random seed: 141732614
generated error fail pass / total     time test name

[ ]    0    0    0    0 / 1000     0.0s STM Array test sequential
[ ]    0    0    0    0 / 1000     0.0s STM Array test sequential (generating)
[✓] 1000    0    0 1000 / 1000     0.0s STM Array test sequential

[ ]    0    0    0    0 / 1000     0.0s STM Array test parallel
[✓]    1    0    1    0 / 1000     7.7s STM Array test parallel

[ ]    0    0    0    0 / 1000     0.0s STM Array test tearing parallel
[✗]  642    0    1  641 / 1000    16.8s STM Array test tearing parallel

[...]

  Results incompatible with linearized model

                                                                                                       |                                                
                                                                                                       |                                                
                                                     .--------------------------------------------------------------------------------------------------.
                                                     |                                                                                                  |                                                
                                        Get 5 : Ok (0x40000000000)                                                                    Fill (3, 7, 0x40000000000) : Ok (())                               
                                      Set (9, 0x800000000) : Ok (())                                                                            Stable_sort : ()                                         
     Copy : [|0x1; 0x1; 0x1; 0x40000000000; 0x40000000000; 0x0; 0x1; 0x1; 0x40000000000; 0x800000000|]                                                                                                   
                Find_opt ({34359738368 -> false; 439... (truncated) : Some (0x40000000000)                                                                                                               
                                                Length : 10                                                                                                                                              

The test still needs a guard to only trigger on >5.3 to limit future CI alarms, but should otherwise be good to go...

[jmid]

CI summary for aa871d0 (rebased on main and with a <5.4 guard added: all 50 workflows passed.

I've also experimented a bit with the suggestion of switching to heap-allocated array elements (say int option),
hoping to trigger crashes on those in case of tearing, and ultimately save us from a separate test for it.
However even with 100 repetitions I was not able to trigger a tearing crash.

As such, it seems reasonable to go with the current PR. Merging.

[jmid]

CI summary for merge to main: all 51 workflows passed