Partially synchronous programming abstractions for replicated state machine
Replication is the standard way to make distributed applications fault-tolerant. Implementing state machine replication is notoriously difficult due to asynchronous communication and the occurrence of faults, such as the network dropping messages or processes crashing.
One fundamental obstacle in having correct fault-tolerant implementations is the lack of abstractions when reasoning about their behaviors. In this talk we focus on partially synchronous programming abstractions that view asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. This view simplifies the proof arguments making systems amendable to automated verification.
Technically, we take a programming language perspective and define a domain specific language which has a partially synchronous semantics and separates the implementation of network constraints from the algorithmic computation done by processes. We validate our technique by defining partially synchronous abstractions for several state machine replication algorithms, enabling automation of the verification procedure.