A prophecy variable is an auxiliary variable that encodes into a nondeterministic action the spec will take into the starting state. In Auxiliary Variables in TLA+ Leslie and Stephen says that the prophecy variables are mostly used to make refinements work. The other day I realized that we might also be able to use them to distribute model checking on more machines.
Say, as a toy example, we have two workers pulling messages from an N message queue. Here's a quick outline of the spec:
VARIABLE queue, worker_msg
W == {"w1", "w2"}
Init ==
/\ queue = [i \in 1..N |-> i]
/\ worker_msg = [w \in W |-> NoMsg]
ReadMessage(w) ==
/\ queue # <<>>
/\ worker_msg[w] = NoMsg
/\ worker_msg' = [worker_msg EXCEPT ![w] = Head(queue)]
/\ queue' = Tail(queue)
DoWork(w) ==
\* blah blah blah
Next ==
\E w \in W:
\/ ReadMessage(w)
\/ DoWork(w)
With a prophecy variable, we can preserve all of the same
behavior, but "push some nondeterminism" into Init.
We'll prophess which messages are read by each worker, by not
letting the other worker read them.
VARIABLE proph_msg_receiver
W == {"w1", "w2"}
Init ==
/\ proph_msg_receiver \in [1..N -> W]
/\ \* etc
ReadMessage(w) ==
/\ queue # <<>>
/\ proph_msg_receiver[Head(queue)] = w
\* etc
Next ==
/\ \E w \in W:
\/ ReadMessage(w)
\/ DoWork(w)
/\ UNCHANGED proph_msg_receiver
Now we have more initial states, but each initial state has a
smaller state space, so we have the same set of behaviors overall.
What does this give us? In some cases, the state graphs from each initial state will be mostly disjoint from one another, so we can split model-checking across multiple machines by giving them each a different set of initial states. We parameterize the spec in MCSpec.tla:
EXTENDS Spec
CONSTANT W1Msgs, W2Msgs
ASSUME W1Msgs \union W2Msgs = 1..N
ConstFunc(set, val) == [x \in set |-> val]
MCInit ==
/\ Init
/\ proph_message_receiver = ConstFunc(W1Msgs, "w1") @@
ConstFunc(W2Msgs, "w2")
Then we just give each server separate values for the constants
in MCSpec.cfg.
One potential benefit this has over TLC's Distributed Mode is that this approach lets you distribute liveness checking, too. One potential drawback is that you'll be doing redundant computation, as the initial states won't lead to completely disjoint state spaces.
I should be clear this is just an idea I had, I haven't actually tried it on a real spec.
H