Towards the Synthesis of Coherence/Replication Protocols from Consistency Models via Real-Time Orderings

This work focuses on shared memory systems with a read-write interface (e.g., distributed datastores or multiprocessors). At the heart of such systems resides a protocol responsible for enforcing their consistency guarantees. Designing a protocol that correctly and efficiently enforces consistency is a very challenging task. Our overarching vision is to automate this task. In this work we take a step towards this vision by establishing the theoretical foundation necessary to automatically infer a protocol from a consistency specification. Specifically, we propose a set of mathematical abstractions, called real-time orderings (rt-orderings), that model the protocol. We then create a mapping from consistency guarantees to the minimal rt-orderings that enforce the guarantees. Finally, we informally relate the rt-orderings to protocol implementation techniques. Consequently, rt-orderings serve as an intermediate abstraction between consistency and protocol design, that enables the automatic translation of consistency guarantees into protocol implementations.