Estimate the search space

[symbiont-stevan-andjelkovic]

In order to display progress and to gauge how well our lineage-driven optimisations are working we should try to estimate the search space.

For a first draft, that also includes notes about the tricky parts, see #174.

[symbiont-stevan-andjelkovic]

In PR #184 we added an explanation of how to estimate the random search fault space given a failure specification, given one concrete test run.

There are several ways to improve on this.

For starters we need to figure out how many interesting concrete programs there are to being with. Typically property based testing focuses on this aspect, i.e. generate random test cases, but because in distributed systems a very small test case, e.g. a write followed by a read, has so much non-determinism this aspect is less important than exploring the non-determinism.

It would also be interesting to estimate what the fault space is if the random search is augmented with information about the network trace (i.e. which events actually happened in the concrete run) and memory of which faults it already tried in previous runs. This would make it closer to what lineage-driven fault injection (LDFI) does, but with very simple constraints (don't try what you've already tried, as opposed to try to eliminate possibilities based on what we know). The tricky part here is that as we introduce faults, they might trigger retries which spawn new messages that were not in the original network trace. We could perhaps make an estimate given that no new messages are spawned at the start of the test, and then in addition calculate how many new messages are spawned per run on average and how much they enlarge the fault space as we run the test.

To make the estimate closer to what actually happens during LDFI we would need to take all the constraints it produces into account, which seems hard. A possible alternative is to get some statistics from the SAT solver itself about its estimated search space? This would enable us to compare how efficient LDFI is verses random search or even one version of LDFI vs another with slightly tweaked constraints.

It would also be interesting, but hard, to take symmetries or equivalence classes of states into account, e.g. doesn't it really matter which of the 4 follower nodes we choose to crash?

A simpler problem would be to run a sweep search where we start with a small failure specification and iteratively make it bigger until we reach some timeout, and basically see how far we get as a measure of how efficient it is for a bug free program. By analogy this would be closer to a benchmark, while properly estimating the search space is closer to calculating the complexity of the algorithm.

[symbiont-stevan-andjelkovic]

For an explanation of how LDFI cuts down the fault space and how to estimate the number of runs needed see #196.

[symbiont-stevan-andjelkovic]

For starters we need to figure out how many interesting concrete programs there are to being with.

One possible way to compute this would be to: identify test case equivalence classes up to a certain depth, e.g. write(k1, v1) || write(k2, v2); ... is equivalent to write(k2, v2) || write(k1, v1); .... This can perhaps be done by generating a new random test case, run it to produce a history and a model, hash the response part of the history and the model, repeat, all test cases with the same hash are in the same equivalence class.