Allow non-deterministic next states

[jayaprabhakar]

At present, the Step function allows non deterministic outputs, but the next state must be determined based on current state, input, and output. (Being able to specify the output allows some amount of non-determinism but still limited)

There are some use cases where the next states could be different even if there are no differences in the output. For example: with paxos with 3 nodes, after a Put, it doesn't matter whether 3 nodes agreed or only 2 modes agreed. The system could be in either state even in a sequential system. (This could be tested differently, but for some usecase, being able to represent the non determinism is helpful. )

Is it possible to allow non-deterministic next states? I couldn't fully understand the algorithm, but from my understanding it allows non determinism on the states and it's currently limited by the API.

Proposal: instead of Step function returning a single next state, if the function could have a slice of possible next states, it would work.
Please let me know on the feasiblity.

[serathius]

Etcd implements non determinism in model as multiple alternative states that fork for equivalent states and collapse. See implementation in https://github.com/etcd-io/etcd/blob/main/tests/robustness/model/non_deterministic.go

[jayaprabhakar]

Thanks, I will go over it in detail.
A brief look, this is what I understand. Can you correct me if I missed something?

1. Instead of keeping state as a single possible states, use the set of alternatives as the state.
2. Each time the Step function is called, advance each of the possible alternatives to the next level, removing invalid states.
3. If the set becomes empty, mark the Step function itself as invalid.

Is the correct? Just curious does this affect the visualizations or the linearization violations?

Also, do you think this could be made into a reusable library?

[anishathalye]

There are some use cases where the next states could be different even if there are no differences in the output. For example: with paxos with 3 nodes, after a Put, it doesn't matter whether 3 nodes agreed or only 2 modes agreed. The system could be in either state even in a sequential system.

For the implementation state, yes; but why is this information part of the state of a sequential specification? At a higher level: what is the spec of the system you're trying to test?

Is it possible to allow non-deterministic next states? I couldn't fully understand the algorithm, but from my understanding it allows non determinism on the states and it's currently limited by the API.

Proposal: instead of Step function returning a single next state, if the function could have a slice of possible next states, it would work.

In theory, yes, we could support this, in that the implementation is basically just a (smart) brute force search, and so this would just increase the search space. An even easier way is to support writing nondeterministic specifications, and support converting them to deterministic specifications using a power set construction, which is what @serathius is doing in etcd.

Also, do you think this could be made into a reusable library?

Yes! I've implemented this in 9c11fdd.

Just curious does this affect the visualizations or the linearization violations?

This transformation is sound: checking with respect to a nondeterministic specification (if we wanted to implement support for that directly in the checker) would return the same result as checking with respect to the deterministic version following the power set construction. It affects visualizations, in that we now need to visualize sets of states rather than single states. You can see an example here:

You can download the HTML file for the interactive visualization here: vis.html.zip

I've taken a simple approach and written the default functionality to show the set as { ... }; you can override this by calling NondeterministicModel.ToModel() and then mutating the .DescribeState attribute of the resulting Model.

[jayaprabhakar]

Thanks @anishathalye for the quick turnaround.

but why is this information part of the state of a sequential specification? At a higher level: what is the spec of the system you're trying to test?

I am the developer of FizzBee, formal verification platform. First, the developers would be able to model the system at a higher level and validate their design is correct. Once the design is validated, we can use that model/state space to test the implementation. If we can validate the design meets the implementation, and since we already verified the design is correct, then it will give a higher confidence that the implementation is correct.

For the Paxos example, if we are looking at it at the user level to check if the transactions appear sequential, we don't really need to know the details. But if we want to validate the recovery process or lower level details, we will need to capture such information. With that, I believe we would need shorter histories to validate the smaller functionality, so this could be more effective.

In addition to this, many distributed systems do not provide linearizable consistency levels. But when we validate the implementation at a lower level, I think we could use the linearizability testing tools like porcupine to match the history with the model.

[anishathalye]

Neat, thanks for sharing!

I'm going to close this issue since we have nondeterministic model support now. If you have any other feature requests, please let me know.