PRL Seminars

We present an algorithm that emulates atomic read/write shared objects in a dynamic network setting. To ensure availability and fault-tolerance, the objects are replicated. To ensure atomicity, reads and writes are performed using quorum configurations, each of which consists of a set of members plus sets of read-quorums and write-quorums.

The algorithm is reconfigurable: the quorum configurations may change during computation, and such changes do not cause violations of atomicity. Any quorum configuration may be installed at any time. The algorithm tolerates processor crashes and message loss and guarantees atomicity for arbitrary patterns of asynchrony and failure.

The processing consists of three major concurrent activities: reading and writing objects, introducing new configurations, and removing obsolete configurations. The algorithm is formally specified using Input/Output Automata notation and its correctness (atomicity) is proved using invariants and partial-order-based methods. The algorithm satisfies a variety of conditional performance properties, based on timing and failure assumptions. We implemented this atomic memory system in a LAN by carefully mapping the formal specification to Java/sockets code, and empirical performance studies are in progress. Finally we discuss a variety of algorithmic optimizations.

Joint work with Nancy Lynch.