Test generation

[bartoszmodelski]

(Based on #19)

Now, that we can easily compare traces covered by any exploration, let's automatically generate sample programs and run them under DSCheck. That lets us run automatic search for skipped traces. Heavily inspired by #15.

Includes:

• Generation of conditional statements. It's based on generation of arbitrary function, which takes n inputs and assigns some boolean output to each combination. Conjuction and disjunction execute as in normal programs, that is skipping operations if early exit is possible.
• Random sampling using do_run - slower than just running the test but more likely to find some executions. It's useful for testing current DPOR but also in the future, as more optimised DPOR terminate on many tests on which current DSCheck does not.
• It focuses on the kind of programs we typically run for testing lockfree structures, i.e. spawn n threads with each doing some operations on shared data.

With above, we can either ensure than an implementation has explored at least all the traces that random sampling has seen, or assert that two implementations have seen exactly the same set of traces.

Testing

I haven't written automated tests. I tested it against DSCheck including a bug introduced on purpose e.g. 0.01% chance to skip a transition or insertion of trace.

Sample generations

let a = Atomic.make 0 in
let b = Atomic.make 1 in
let c = Atomic.make 2 in
let d = Atomic.make 3 in
let e = Atomic.make 4 in
let f = Atomic.make 5 in

Domain.spawn (fun () ->
        Atomic.set c 1;
        Atomic.get f |> ignore;
        Atomic.set f 0;
)

Domain.spawn (fun () ->
        Atomic.set e 2;
        Atomic.get c |> ignore;
        Atomic.get d |> ignore;
)

Domain.spawn (fun () ->
        Atomic.set c 0;
        if (IntSet.mem (Atomic.get d) (IntSet.of_list [0; 3])) then (
                Atomic.set a 3;
                Atomic.set d 1;
        );
)

let a = Atomic.make 0 in
let b = Atomic.make 1 in
let c = Atomic.make 2 in

Domain.spawn (fun () -> 
        Atomic.set b 1;
        Atomic.get c |> ignore;
        if (IntSet.mem (Atomic.get c) (IntSet.of_list [0; 1; 2])) then (
                if (IntSet.mem (Atomic.get c) (IntSet.of_list [0])) then (
                        if (IntSet.mem (Atomic.get b) (IntSet.of_list [0; 2])) then (
                                Atomic.get c |> ignore;
                        );
                );
        );
)

Domain.spawn (fun () -> 
        if (IntSet.mem (Atomic.get c) (IntSet.of_list [1; 2])) then (
                Atomic.set c 1;
                Atomic.get a |> ignore;
                if (IntSet.mem (Atomic.get c) (IntSet.of_list [1; 2])) then (
                        if (IntSet.mem (Atomic.get c) (IntSet.of_list [])) then (
                                if (IntSet.mem (Atomic.get c) (IntSet.of_list [1])) then (
                                        Atomic.get a |> ignore;
                                );
                        );
                );
        );
)

Domain.spawn (fun () -> 
        Atomic.get c |> ignore;
        if (IntSet.mem (Atomic.get a) (IntSet.of_list [0; 1]) && IntSet.mem (Atomic.get a) (IntSet.of_list [0; 1])) then (
                Atomic.set c 0;
                if (IntSet.mem (Atomic.get c) (IntSet.of_list [])) then (
                        Atomic.set b 2;
                );
        );
)

let a = Atomic.make 0 in
let b = Atomic.make 1 in
let c = Atomic.make 2 in

Domain.spawn (fun () -> 
        Atomic.get a |> ignore;
        Atomic.set c 2;
        Atomic.set b 0;
        Atomic.get c |> ignore;
        Atomic.get b |> ignore;
        Atomic.set b 2;
)

Domain.spawn (fun () -> 
        if (IntSet.mem (Atomic.get a) (IntSet.of_list [2]) || IntSet.mem (Atomic.get b) (IntSet.of_list [0])) then (
                Atomic.get b |> ignore;
        );
)

Domain.spawn (fun () -> 
        Atomic.get a |> ignore;
        Atomic.set c 1;
        Atomic.set c 0;
        Atomic.get a |> ignore;
        if (IntSet.mem (Atomic.get b) (IntSet.of_list [1])) then (
                if (IntSet.mem (Atomic.get b) (IntSet.of_list [0])) then (
                        Atomic.get c |> ignore;
                );
        );
)

[art-w]

I think #19 is almost mergeable (modulo cleaning up history?), which would make it easier to review this :)

I'm not sure why #15 was rewritten, but okay, some suggestions from that PR:

• Can we generate more operations than Atomic.get and set? In particular the code was tracking which value an atomic was expected to have according to each domain, and would use that to generate an interesting argument for compare_and_set .. old_expected_value ..
• The random --seed parameter was very useful to reproduce the same generated program while fixing bugs in dscheck (typically running the random test would take a while before generating a buggy program, but then you could iterate on this discovered failure until dscheck was fixed)

[bartoszmodelski]

Thanks for looking. I'll wait with #19 to give someone from multicore team a chance to take look.

This was written specifically to test source sets and departs from #15 in quite a few ways. But suggestions sound good:

• I'll add other operations, so we don't have to think about the dependency relation in testing. Although I'm not sure about tracking the values - I'm a bit worried of building logic to generate interesting programs as that lets us introduce biases into what's generated. Conversely, the issues stemming from creating some boring programs are much smaller - the simple programs just get evaluated in no time.
• I'll add the-seed param as well. More reproducibility is always good.

[lyrm]

Not a lot to comment, it seems to be working fine as expected ! (except for some small funny mistakes in the command line part). It would be interesting to have a README specifying a (even simplified) grammar of generated code.

[lyrm]

List.length enabled is len

[lyrm]

It would be great to have default values.

[lyrm]

(I meant : having the default values printed in the -help doc)

[bartoszmodelski]

Changed this to use cmdliner as in #15

[lyrm]

This should be false by default if you want the optional flag to activate it.

[lyrm]

That's actually generated test_count+1 tests :p

[bartoszmodelski]

Rebased after merging the better-traces and addressed feedback.

[lyrm]

Thanks !