The Tatami Protocol
The Tatami Protocol is a distributed broadcast protocol which mantains the consistency of proofs on users sites. It is highly dependent upon the Tatami Database which, among other things, stores the meessages handled by the protocol.

Some standard daemons are responsible for the low level communication providing the background mechanism on which the Tatami Protocol is based. However, the Tatami Protocol should be viewed as a collection of strategies saying what to do when certain events are encountered, including the following:

The system has an abstract State , which is modified whenever one of the above events appears. Implementation details of the state are hidden from applications that use the protocol, but there are some attributes which allow applications to extract useful information from the state, including: The proofweb of the Tatami Protocol consists of three main parts: the attribute coherence of the specification, some distributed properties of the protocol, and the corectnesss of the protocol. These are included below, although they are not completely self-contained; see the Tatami Protocol Proof homepage for background and full details of the proof.
Explanation Page for the Specification

It is usually convenient to specify data by initial algebras, but in this example, the algebra of data is specified loosely as a theory of dependency sets, DEP-SET. This means that DEP-SET contains properties that must be respected by any concrete algebra we might chose for data. An interesting and immediate consequence of this approacg is that, depending on what algebra is chosen for data, different classes of systems can be obtained.

We first disscuss dependency sets, that is, sets in which elements may depend on each other. The interesting operations on such sets are as follows:

We formally specify the Tatami Protocol as a behavioral specification in which insert, submit, receive and ack are methodes, and database, temp-mem, and not-ack are attributes on a hidden State.

Attribute Coherence of the Tatami Protocol

In order too prove behavioral properties using attribute coinduction, the attribute coherence of the specification must be checked. In other words, we have to show that a state is fully characterized by observations using only attributes. To do this, we have to prove that S1 =A= S2 implies

  1. insert(E, S1) =A= insert(E, S2),
  2. submit(E, S1) =A= submit(E, S2),
  3. receive(E, S1) =A= receive(E, S2),
  4. ack(U, E, S1) =A= ack(U, E, S2),

In the case of ack, this is done by proving the first order formula:

S1,S2:State U':User E:Elt (
       (database(S1) = database(S2) and
        temp-mem(S1) = temp-mem(S2) and
       U:User (not-ack(U,S1) = not-ack(U,S2))


       (database(ack(U',E,S1)) = database(ack(U',E,S2))     and
        temp-mem(ack(U',E,S1)) = temp-mem(ack(U',E,S2))     and
       U:User (not-ack(U,ack(U',E,S1)) = not-ack(U,ack(U',E,S2))) )

By quatifier elimination, the constants s1, s2 : State , u' : User and e : Elt are generated. By implication elimination and conjunction elimination, three new equations are introduced in the specification, namely database(s1) = database(s2) , temp-mem(s1) = temp-mem(s2) and U:User (not-ack(U,s1) = not-ack(U,s2)) . Now, there are three subgoals left to prove. The first two, database(ack(u',e,s1)) = database(ack(u',e,s2)) and temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2)) are immediate, but the third, U:User (not-ack(U,ack(u',e,s1)) = not-ack(U,ack(u',e,s2))), requires quantifier elimination. So, a new constant u : User is introduced and the new goal becomes not-ack(u,ack(u',e,s1)) = not-ack(u,ack(u',e,s2)). Because of the operational semantics of the OBJ's _==_ , we need to treat two cases, u == u' or u =\= u' . The rest of the proof is easy now.

Idempotency of Methods

A first set of easy behavioral properties which can be proved right now is the idempotency of methodes, i.e., of insert , submit , receive and ack. Why should we be interested in idempotency? This is because the low level daemons use bare IP, so the sender daemon just keep sending messages until acknowledgements are received and the acknowledger daemon just send acknowledges whenever messages are received. So it is very possible to receive or acknowledge many times the same message. On the other way, a user can reinsert or resubmit the same proof either by purpose or by mistake (similar situations appear when the email is used).

All of the following properties are proved relatively similarly, so we discuss only the idempotency of receive in the explanation page. Formally, we need to prove the following (behavioral) first order formula:

F:Elt (S:State (receive(F,receive(F,S)) = receive(F,S)))

Since we have already proved the behavioral coherence of the specification, the simplest way to prove the behavioral property above is to use attribute coinduction. This yields another first order formula, namely:

F:Elt S:State (
        database(receive(F,receive(F,S))) = database(receive(F,S))   and
        temp-mem(receive(F,receive(F,S))) = temp-mem(receive(F,S))   and
        U:User (not-ack(U,receive(F,receive(F,S))) = not-ack(U,receive(F,S))) )

As usual, we prove it by firstly eliminating the quantifiers, i.e., by introducing two constants f :Elt and s :State , and then by eliminating the conjunction, so generating three subgoals:

  1. database(receive(f,receive(f,s))) = database(receive(f,s)) ,
  2. temp-mem(receive(f,receive(f,s))) = temp-mem(receive(f,s)) , and
  3. U:User (not-ack(U,receive(f,receive(f,s))) = not-ack(U,receive(f,s))) .

The first two subgoals follow immediately by reduction, but the third one needs quantifier elimination first and then reduction.

Commutativity of Methods

All methods involved are commutative in a special sense, namely, that the order in which the same method is applied (as a consequence of unpredictable external events) in a given state is not important, that is, behavioral equivalent states are obtained. In the case of receive , for example, the following behavioral equality should be proved:

F1,F2:Elt S:State (receive(F1,receive(F2,S)) = receive(F2, receive(F1,S))).

The generated proof is very simple (relatively), but it is highly based on two properties of the left and right closures, namely:

L,R:Set E:Elt (l< l< L, R >, add(E, r< L, R >) > = l< L, add(E,R) >), and
L,R:Set E:Elt (r< l< L, R >, add(E, r< L, R >) > = r< L, add(E,R) >).

We refer the reader to the explanation page of the specification for more information about the closure operations. In principle, these two properties say that it is not necessary to make closures after each added element; it is enough to make only one closure after more elements are added.

Perhaps the most interesting proof on this page is the commutativity of ack. The first order formula which should be proved is:

F1,F2:Elt U1,U2:User S:State (ack(U1,F1,ack(U2,F2,S)) = ack(U2,F2,ack(U1,F1,S))).

What makes this example different from the others is that a case analysis is required. This is because three constants u,u1,u2:User are involved at some point in the proof (these constants are generated by the quantifier elimination rule), and because the special predicate _==_ is used for the sort User in the PROTOCOL specification.

Correctness of the Tatami Protocol

We saw some properties emphisizing the distributed aspect of the tatami protocol in the previous pages. The goal of those properties was to show that receiving or submiting a message twice, or the order in which messages are received from the internet did not affect the state of the system. But all these properties do not say anything about the corectness of the protocol.

But actually, what is the corectness of the protocol? Since all applications can access the state of the protocol using only the three atributes database , temp-mem , and not-ack, we must define the corectness in terms of these attributes. But temp-mem is only an extra facility offered by our system (in the same way in which "mailq" is an extra facility offered to the email users), so the consistency of the elements found there is not guaranteed, and not-ack shows only the communication status with the other users. Therefore, we formulate the correctness of the Tatami Protocol as follows:

For every reachable state S, database(S) is consistent.
In other words we should show that ok?(database(init)) = true and that ok?(database(_)) is an invariant for methods.

Putting all these together, we have to prove the following three first order formulas:

  1. ok?(database(init)) = true,
  2. S:State F:Elt (ok?(database(S)) = true and ok?(parents(F),database(S)) = true) implies
            (ok?(database(insert(F,S))) = true and ok?(database(insert(F,S))) = true))
    , and
  3. S:State (ok?(database(S)) = true) implies
            F:Elt (ok?(database(receive(F,S))) = true) and
            F:Elt U:User (ok?(database(ack(U,F,S))) = true))
As can be seen in 2., we assume that the applications (for example KUMO) do not let the users introduce or submit inconsistent messages, i.e., messages whose parents are not in the binary relation ok? with the database. We remind the reader that there could be many different ways to implement (and to define) the relation ok?.
25 April 1998