Synchronizing events in replicated systems

The application of N-Modular Redundancy (NMR) in the construction of software permits redundant systems to be robust with respect to failures in replicated processors. In order to exhibit consistent behavior, all processors in an NMR node must process input requests in the same order. This paper investigates the introduction of synchronization points among replicated computations in a nondeterministic model for concurrent programming. A formal specification is given of a distributed synchronization mechanism that does not introduce any additional deadlock in the replication of a basic single system. We propose this synchronization mechanism as a means of preventing the occurrence of the so-called sequencing failures. The properties of the proposed solution are specified and proved using the COSY path-expression formalism. Finally, some implementation schemes are proposed which satisfy the given specification.