Stabilization-preserving atomicity refinement

Program refinements from an abstract to a concrete model empower designers to reason effectively in the abstract and architects to implement effectively in the concrete. For refinements to be useful, they must not only preserve functionality properties but also dependability properties. In this paper, we focus our attention on refinements that preserve the dependability property of stabilization. Specifically, we present a stabilization-preserving refinement of atomicity from an abstract model where a process can atomically access the state of all its neighbors and update its own state, to a concrete model where a process can only atomically access the state of any one of its neighbors or atomically update its own state. Our refinement is sound and complete with respect to the computations admitted by the abstract model, and induces linear step complexity and constant synchronization delay in the computations admitted by the concrete model. It is based on a bounded-space, stabilizing dining philosophers program in the concrete model. The program is readily extended to: (a) solve stabilization-preserving semantics refinement, (b) solve the stabilizing drinking philosophers problem, and (c) allow further refinement into a message-passing model. (C) 2002 Elsevier Science (USA).