[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Invariance under transition order

On 01 Feb 2016, at 22:12, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

Thanks! This is exactly my problem, and I see that you have a good definition of the property I'm looking for: 

    "We will then establish a reduction theorem that shows that for every fine-grained run there exists an equivalent round-based (“coarse-grained”) run in the sense that the two runs exhibit the same sequences of local states of all processes, modulo stuttering"

The question is, then, suppose I have a set of such local state variables, how do I specify in TLA+ "this variable always obtains the same sequence of values modulo stuttering"?

Here's one suggestion on how to do that. Specify the two semantics, say, by formulas CoarseSpec and FineSpec. Then define a mapping that computes the "coarse" state from the "fine" state, by restricting to rounds that all processes have already executed, and prove that for any fine-grained execution the result of the mapping is a coarse-grained execution. To be a little more concrete, let's assume your coarse-grained spec looks something like this.

--- MODULE Coarse ---
CONSTANT Proc  \* the processes of the algorithm
VARIABLE x     \* the local states of each process

Init == x = [p \in Proc |-> init(p)]   \* initialize every process
Next == x' = [p \in Proc |-> f(x,p)]   \* all processes execute in lock-step
Spec == Init /\ [][Next]_x             \* ignoring liveness for simplicity

Fine-grained executions are specified by interleaving the processes. In order to simplify the statement of the relation between the two semantics, let's record for every process the history of its past states. (In practice, you probably want to introduce a history variable separate from the "real" specification.)

--- MODULE Fine ---

Init == y = [p \in Proc |-> << ... >>]  \* singleton sequence containing initial state
Next == \E p \in Proc :
   y' = [y EXCEPT ![p] = Append(@, ...)] \* process p moves and records its new state
Spec == Init /\ [][Next]_y

(* Now recover the abstract state for the last round that all processes executed.
   Note that the state of the fine-grained spec may need to be more detailed: the
   operator g (not defined here) retrieves the abstract state of process p. *)
Min(S) == CHOOSE n \in S : \A m \in S : n <= m
abs == LET n == Min( {Len[y][p] : p \in Proc} )
       IN  [p \in Proc |-> g(y[p][n], p)]

C == INSTANCE Coarse WITH x <- abs

THEOREM Spec => C!Spec

Does this make sense?