Properties of the Tatami Protocol

Tatami Protocol

The Tatami Protocol is a proof distributed broadcatsing protocol which mentains the consistency of proofs on users sites. It is highly deppendent upon the Tatami Database which, among other features, is used to store the meessages handled by the protocol. There are some standard daemons responsible for the low level communication working in the background which provide the mechanism on which the Tatami Protocol is based. However, the Tatami Protocol should be viewed as a colection of strategies saying what to do when some events are encountered. The events we are considering are:

insert an element in the database. An element can be a specification, a proof task, an inference rule, a part of a proof, etc.,
submit an element to all members of the project,
receive an element from another member of the project; it is left to the daemons to send acknowledgements for the received elements,
acknowledgement received from another user.

There is an abstract State of the system which is modified every time an event as above appears. The implementation details of the state are hidden for the applications using the protocol. However, there are some attributes which allow the applications to extract useful information from the state:

database gives all elements which put together give a consistent proof. Notice that because of the unpredictable way in which messages are carried over the internet, there could be the case that some already received elements deppends on other elements which have not been received yet; such elements are not provided by the database attribute,
temp-mem gives all those elements which cannot be provided by the database attribute. We do not have any good reason not to allow the applications to access these elements, but if they do it then, of course, no consistency is guaranteed.
not-ack gives the communication status of every user. In other words, it gives for every user U the already submitted messages which have not been acknowledged by U .

The proofweb of the Tatami Protocol consists in three main parts: the attribute coherence of the specification, some distributed properties of the protocol, and the corectnesss of the protocol.

This websites has 14 goals:

First proof page for goal 1 .
First proof page for goals 2 to 5 .
First proof page for goals 6 to 9 .
First proof page for goal 10 .
First proof page for goals 11 to 14 .

Here is the duck code that generated this website.

To the Tatami demos homepage.
To the Links Project homepage.
To the UCSD Meaning and Computation Group homepage.

The prose on this page was written by Grigore Rosu, and the proof was generated from code written by Grigore Rosu, using Kumo on Fri Jun 12 12:39:51 PDT 1998. Kumo is implemented by Kai Lin .