6
$\begingroup$

The short paper "Computer Science and State Machines" by Leslie Lamport seems quite strange to me.
On the one hand, I am surprised to see that an important hardware protocol called "two-phase handshake" can be derived from a trivial program, simply by mathematical substitution.
On the other hand, I think that this example is (and should be) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples.

My question is straightforward:

Is this derivation a coincidence? Could anyone offer more examples or related references?


The derivation of the "two-phase handshake" protocol from a trivial program:

The trivial program mentioned above is just to alternately perform the $\mathcal{P}$ and $\mathcal{C}$ operations:

$\mathcal{X}: \textrm{ loop } \mathcal{P} \textrm{ } ; \textrm{ } \mathcal{C} \textrm{ endloop}$

By introducing a variable $pc$ to represent the "program counter", $\mathcal{X}$ can be described as the following state machine:

  • $Init_{\mathcal{X}} \triangleq (pc = 0) \land Init_{\mathcal{PC}}$
  • $Next_{\mathcal{X}} \triangleq \big( (pc = 0) \land \mathcal{P} \land (pc' = 1) \big) \lor \big( (pc = 1) \land \mathcal{C} \land (pc' = 0) \big)$

where $Init_{\mathcal{X}}$ denotes the set of initial states; $Next_{\mathcal{X}}$ specifies the next-step transition. $Init_{\mathcal{PC}}$ specifies the initial values of the variables in $var_{\mathcal{PC}}$ involved in $\mathcal{P}$ and $\mathcal{C}$. The primed variable ($pc'$ here) is used to represent the modified version of its unprimed counterpart ($pc$ here).

The two-phase handshake protocol can be described as follows, where $p$ and $c$ are initially equal.

\begin{eqnarray} \mathcal{Y} : & \textrm{ process } & Prod: \textrm{ whenever } p = c \textrm{ do } \mathcal{P} \textrm{ } ; \textrm{ } p = p \oplus 1 \textrm{ end} \\ & \Arrowvert & \\ & \textrm{ process } & Cons: \textrm{ whenever } p \neq c \textrm{ do } \mathcal{C} \textrm{ } ; \textrm{ } c = c \oplus 1 \textrm{ end} \end{eqnarray}

Note that process $Prod$ reads $c$ and writes $p$ while $Cons$ reads $p$ and writes $c$. It is not hard to find out that $\mathcal{Y}$ alternately performs $\mathcal{P}$ and $\mathcal{C}$.

The protocol $\mathcal{Y}$ can also be described as a state machine:

  • $Init_{\mathcal{Y}} \triangleq (p = c) \land Init_{\mathcal{PC}}$
  • $Next_{\mathcal{Y}} \triangleq Prod \lor Cons$
  • $Prod \triangleq (p = c) \land \mathcal{P} \land (p' = p \oplus 1) \land (c' = c)$
  • $Cons \triangleq (p \neq c) \land \mathcal{C} \land (c' = c \oplus 1) \land (p' = p)$

The amazing observation is:

$\mathcal{Y}$ can be obtained from $\mathcal{X}$ by substituting $p \oplus c$ for $pc$ in their state machines.

$\endgroup$
  • $\begingroup$ This is a great question. But I have one small comment on it. You write: "I doubt that this lovely derivation has been chosen deliberately." - I'm not sure what you were getting at here. I have no problem believing that Lamport deliberately chose this example to illustrate his point in the best way he was able. I'm not sure how that relates to your ultimate question anyway. $\endgroup$ – D.W. Jul 25 '14 at 23:20
  • $\begingroup$ @D.W. Thanks for your comment. I also believe that this example is (and should be) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples. (updated the post) $\endgroup$ – hengxin Jul 26 '14 at 1:31
  • $\begingroup$ In order to get some intuition, it might be helpful to see where it gets by considering all 16 boolean functions on two boolean variables p and c. $\endgroup$ – Abel Molina Jul 30 '14 at 6:12
7
$\begingroup$

There is a general theory here, which was introduced into CS by Robin Milner, which Lamport did not go into.

A state machine is generally given as a triple $(Q \in \mathrm{Set}, q \in Q, f \in I \times Q \to \mathcal{P}(O \times Q))$, consisting of a state set $Q$, an initial state $q$, and a transition relation $f$.

Now, suppose we have two automata $(Q, q, f)$ and $(T, t, g)$. Let's ask a question: when are these automata equivalent? If all we are going to do is take the machines and send them inputs and listen to the outputs, we don't want to require the state sets to be the same (for example, if $(T, t, g)$ is the result of running a DFA minimization algorithm on $(Q, q, f)$).

It turns out that the right notion of equivalence is bisimulation. The idea is that we take two state machines to be the same, if we can produce a relation $R \subseteq Q \times T$, such that

  • $(q,t) \in R$
  • for all $(q,t) \in R$ and $i \in I$ and $o \in O$ then:
    • for all $q' \in Q$, if $(o, q') \in f(i, q)$, then there is a $t' \in T$ such that $(o, t') \in g(i, t)$.
    • for all $t' \in T$, if $(o, t') \in g(i, t)$, then there is a $q' \in Q$ such that $(o, q') \in f(i, q)$.

This says that if we can figure out any relation such that (a) the initial states are related, and (b) from related initial states, any I/O action the first machine can take can be mimicked by the second machine in a way that keeps you in the relation, and (c) similarly, the first machine can mimic anything the second can do.

Lamport's notation with primes is a way of concisely describing input-output relations. In this case, the state sets are the program counter of the first program, and the two program counters of the second program. The bisimulation relation is $R(pc, (p, c)) \triangleq pc = p \oplus c$, and then the bisimulation conditions follow trivially (since the relation expressions are equal under the subsitution).

The general theory at work is the theory of coinduction. State machines are representions of corecursively defined sets, and bisimulations tell you when two state machines are representations of the same potentially-infinite object.

Incidentally, this paper is written in a rather polemical style. Equally polemically, I'll point out that the style he advocates in this paper simply fails should you ever need to verify part of a program in isolation -- for example, if you want to prove a library implementation correct, or verifying a program using higher-order functions (or even just dynamic linking).

But both of us will use coinduction, nonetheless.

$\endgroup$
  • $\begingroup$ Thanks for your excellent answer. A quick search shows me that coinduction (which I know little) and bisimulation (which I know just a few) are themselves pretty big topics. Confusion about your polemical comment in the last but one paragraph: Which fails? Is it bisimulation? Isn't it popular in model checking and generally formal methods? I am not a native English speaker and am stumped on the inverted sentence. Would you mind explaining it in more details? Great thanks. $\endgroup$ – hengxin Jul 31 '14 at 2:33
  • $\begingroup$ I have just learnt a little thing about coinduction from this post: Where inductive definitions build a structure from elementary building blocks, coinductive definitions shape structures from how they can be deconstructed. I can get the basic idea. You claim that State machines are representions of corecursively defined sets. Why is it? Could you please make it more clear or provide some references? Thanks. $\endgroup$ – hengxin Jul 31 '14 at 12:53
  • 1
    $\begingroup$ Lamport doesn't mention Milner because he developed his own theory concurrently, starting in 1977. He doesn't need the concept of bisimulation because labeling states rather than events makes bisimulation coincide with the simpler, more convenient notion of trace-equivalence, and makes LTL and FOL sufficient. Lamport's theory handles open specifications (libraries) elegantly, which he covered at length. In fact, any form of composition, including higher order, becomes simple conjunction in his formalism (not surprising as it's similar to ODEs, just discrete and designed for refinements). $\endgroup$ – pron Dec 22 '16 at 12:46
  • $\begingroup$ @pron: No, Lamport's formalism doesn't handle libraries adequately. Try working out what the spec of a memory allocator or thread scheduler should be, bearing in mind it has to run in the same address space as client code. (It's not enough to treat these as primitive abstractions because the same patterns show up at higher levels of the stack -- eg, connection pooling for DB access is morally the same as a malloc implementation, and GUI libraries basically implement threading abstractions.) $\endgroup$ – Neel Krishnaswami Dec 27 '16 at 17:33
  • 1
    $\begingroup$ @NeelKrishnaswami I don't see any problem, but perhaps you could pinpoint the issue. It was Lamport who proved the soundness of assume-guarantee proofs for concurrent systems (w/parallel composition), and those are well-handled by his formalism. See research.microsoft.com/en-us/um/people/lamport/pubs/… and/or research.microsoft.com/en-us/um/people/lamport/pubs/… $\endgroup$ – pron Dec 27 '16 at 18:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.