A basic design decision in the Dragon memory system is that multiple copies of read/write data are allowed to exist when data is cached. Without some means for keeping these copies consistent, computations would in general produce unpredictable results. The DynaBus consistency algorithm ensures that this does not happen.

This consistency algorithm is necessarily more complex than the corresponding algorithm for a circuit switched bus because bus transactions are not atomic anymore. Given this added complexity, and the importance of getting the algorithm right before building the hardware, we considered it important to specify the algorithm carefully and to provide a proof of its correctness.

We begin in Section 2 with the definition of consistency. In Sections 3 and 4 we specify the algorithm. And in Section 5 we develop the proof. The reader would find this document considerably easier if he first familiarized himself with the DynaBus Logical Specifications.

One way to define consistency is to say that for each datum A all copies of A have the same value on a cycle by cycle basis—ie. during each cycle of the system clock. This definition is sufficient in the sense that correct programs can be written on a system that satisfies this definition, and is also easy to understand. The problem is that it is fundamentally hard to build an efficient system that embodies this definition when the potential number of caches is large. Fortunately, there is a weaker definition that is still adequate for correctness and is also compatible with the requirement of a large system. It is based on the notion of serializability.

To define serializability, consider the abstract model of a shared memory multiprocessor shown in Figure 5. There are some number of processors connected to a shared memory. Each processor has a private line to shared memory; over this line the processor issues the commands Fetch(A) and Store(A, D), where A is an address and D is data. For Fetch(A) the memory returns the value currently stored at A; for Store(A, D) it writes the value D into A and returns an indication that the write has completed. Let the starting time of an operation be the moment the request is sent over the line and the ending time be the moment either the return value or an indication of completion is received by the processor.

Let S be the state of the shared memory before the start of some computation C, and F be the state after C has completed. The Fetches and Stores of C are said to be serializable if there exists some serial order such that if these operations were performed in this order, without overlap, the same final state F would be reached starting from the initial state S. Two operations are said to overlap if the starting time of one is before the ending time of the other and the starting of the other is before the ending time of the one.

TBD.