I like how this post bridges the vocabulary of two communities that are otherwise not overlapping much, the TLA+ and property-based testing (PBT) people. In particular I’m thinking about “prophecy variables” and “refinement mappings”, which are not typically used in the context of PBT.
A scenario that I don’t quite see how prophecy variables at the actions would work is: imagine you got a distributed system, say a key value store. Client issues the action “write x 1”, the client request and response don’t timeout, but internally within the network of database nodes timeouts do happen (causing leader re-election, etc), where do the prophecy variables go in this case? Are they part of the “write” action?
For the KV store example, it boils down to whether or not the leader election / replication scheme can all be shown to be an implementation detail of a higher-level spec. If so, you’d likely have an abstract spec that looked something like this:
class KVStore {
store: Map<string, any>;
read(key: string): any { ... }
write(key: string, value: any) { ... }
}
The implementation is likely where the prophecy variables would be added, so that node failures / leader election issues can all be simulated and shown to map to the proper spec states. i.e. a true failure will show up as either a no-op in the spec (stutter state) or some explicit error state, but a failure that recovers looks as though the operation in the spec just succeeded with no issue. The more I’m thinking about it, prophecy variables are just the theoretical concept that’s being implemented with fault injection in deterministic simulations, Jepsen tests, etc.
This becomes more tricky when the cluster logic ends up breaking the assumed guarantees of the simple model, say if it’s not actually serializable. In that case, the model may need to be modified to be more permissive.
A brief philosophical aside. Tests are almost entirely about seeing into the future. By simply writing down the expected outputs of an operation, that means that we know what they should be ahead of time. We are the so called test oracle. In model-based testing, we instead delegate this prediction to the model: the model is the oracle.
Nice way to look at it!
I’ve been putting off learning prophecy variables; in refinement mappings, are they a way of injecting prescience into an algorithm so it can refine non-machine-closed liveness properties of an abstract spec, or is that something else?
The primary purpose of prophecy variables is to enable showing that a spec implements another one when at least one is nondeterministic. All of the examples where I’ve found them useful are when the implementation is nondeterministic and the abstract spec is deterministic.
The specs in the “Simple Prophecy Variables” section (4.2) of Prophecy Made Simple are a good example. The abstract spec is a process that receives a stream of integers and calculates their cumulative average. The implementation does the same thing, except there’s also an “undo” operation, where an integer can be ignored after being received and the average never gets calculated for it. Since that implementation spec is nondeterministic, you can’t write a refinement mapping because you’ll eventually hit a case where two states in the implementation try to map to a single one in the spec, and they conflict. The prophecy variable solves this by telling you which operation will be taken ahead of time, so you can use that to relate to the correct abstract states. This makes more sense visually, I could send you a diagram if you want.
This undo example is basically the exact same thing as nondeterministic errors, and that’s what made me realize that a prophecy variable would be helpful in testing those. I know way less about machine closure and liveness properties in general. So maybe there are applications there, but in all of the papers I’ve read about prophecy variables this isn’t mentioned.
I like how this post bridges the vocabulary of two communities that are otherwise not overlapping much, the TLA+ and property-based testing (PBT) people. In particular I’m thinking about “prophecy variables” and “refinement mappings”, which are not typically used in the context of PBT.
A scenario that I don’t quite see how prophecy variables at the actions would work is: imagine you got a distributed system, say a key value store. Client issues the action “write x 1”, the client request and response don’t timeout, but internally within the network of database nodes timeouts do happen (causing leader re-election, etc), where do the prophecy variables go in this case? Are they part of the “write” action?
PS. Your link to lobsters at the end is broken.
For the KV store example, it boils down to whether or not the leader election / replication scheme can all be shown to be an implementation detail of a higher-level spec. If so, you’d likely have an abstract spec that looked something like this:
The implementation is likely where the prophecy variables would be added, so that node failures / leader election issues can all be simulated and shown to map to the proper spec states. i.e. a true failure will show up as either a no-op in the spec (stutter state) or some explicit error state, but a failure that recovers looks as though the operation in the spec just succeeded with no issue. The more I’m thinking about it, prophecy variables are just the theoretical concept that’s being implemented with fault injection in deterministic simulations, Jepsen tests, etc.
The implementation would look something like:
This becomes more tricky when the cluster logic ends up breaking the assumed guarantees of the simple model, say if it’s not actually serializable. In that case, the model may need to be modified to be more permissive.
Nice way to look at it!
I’ve been putting off learning prophecy variables; in refinement mappings, are they a way of injecting prescience into an algorithm so it can refine non-machine-closed liveness properties of an abstract spec, or is that something else?
The primary purpose of prophecy variables is to enable showing that a spec implements another one when at least one is nondeterministic. All of the examples where I’ve found them useful are when the implementation is nondeterministic and the abstract spec is deterministic.
The specs in the “Simple Prophecy Variables” section (4.2) of Prophecy Made Simple are a good example. The abstract spec is a process that receives a stream of integers and calculates their cumulative average. The implementation does the same thing, except there’s also an “undo” operation, where an integer can be ignored after being received and the average never gets calculated for it. Since that implementation spec is nondeterministic, you can’t write a refinement mapping because you’ll eventually hit a case where two states in the implementation try to map to a single one in the spec, and they conflict. The prophecy variable solves this by telling you which operation will be taken ahead of time, so you can use that to relate to the correct abstract states. This makes more sense visually, I could send you a diagram if you want.
This undo example is basically the exact same thing as nondeterministic errors, and that’s what made me realize that a prophecy variable would be helpful in testing those. I know way less about machine closure and liveness properties in general. So maybe there are applications there, but in all of the papers I’ve read about prophecy variables this isn’t mentioned.
[Comment removed by author]