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:
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.
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
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))
implies
(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.
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:
The first two subgoals follow immediately by reduction, but the third one needs quantifier elimination first and then reduction.
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.
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: