Two protocols for implementing n-writer m-reader atomic registers with 1-writer m-reader atomic registers are described. In order to give complete proofs, a theory of interprocess communication is presented first. The correctness of a protocol that implements an atomic register is proved here in two stages: (1) a formulation of higher-level specifications and a proof that the protocol satisfies these specifications. (2) a proof of atomicity assuming that the specifications hold. This division enables a better understanding of the protocols, and the fact that both protocols share the same higher-level specifications reduces the length of the correctness proof. The difference between the two protocols is that in the first the readers do not write at all, while in the second they do. The first protocol is space efficient, while the second is time efficient. [References: 25]
展开▼
