multicoretests

multicoretests copied to clipboard

Extend signature DSL with a program printer

2

Each generated test input represents a program of a certain, stylistic form. Upon failure, it would be handy to be able to print the corresponding program - without the interpretive...

jmid

Memory data-race tests

3

This adds three negative tests for references, mutable record fields and arrays, that tends to trigger memory data-races (the tests are very similar, I'll let you choose which ones to...

art-w

#177 adds a custom shrinker for the `multiple-ts` branch, shrinking `cmd` lists from the tail. This heuristic could be adapted to STM too.

jmid

Some of our tests could benefit from taking `Domain.recommended_domain_count` into consideration ```ocaml Domain.recommended_domain_count : unit -> int The recommended maximum number of domains to be spawned. ``` Relevant tests include...

jmid

At the moment, `STM` and `Lin` share fairly little code. I see a few other opportunities that might be worth exploring: - `Spec` in `STM` and `CmdSpec` in `Lin` share...

shym

This PR takes a stab at adding a program printer #56. This first version - prints a corresponding program without performing a sequential consistency search - only supports `Domain` currently...

jmid

Measure statistical significance of Domain setup

4

There's one remaining usage of `cpu_relax` in spinning the first domain while waiting for the second domain to start-up: https://github.com/jmid/multicoretests/blob/8a9a2327e06036f06ca5ef4b1321129ccff557d6/lib/lin.ml#L122-L124 Now that we have statistics in place, it would be...

jmid

Extend signature DSL to function values

1

In OCaml (and FP in general) signatures accepting function values are common (Hashtbl, Array, ...). To test these, it would useful to extend the signature DSL to be able to...

jmid

Both `Lin` and `STM` share a limitation: - `Lin` tests only a single `t` at a time - `STM` tests only a single `sut` at a time This can be...

jmid

STM's predecessor https://github.com/jmid/qcstm contains a range of examples https://github.com/jmid/qcstm/tree/master/examples We should port these to STM which would allow to run them both sequentially and in parallel mode. The primary difference...

jmid