Littschwager, N. (CSE) – A Proposal for Characterizing Replicated Systems and Emulators
Simulation is a coinductive proof technique to assert the behavioral equivalence of computing systems that has seen fruitful application in distributed systems, concurrent process calculi, and programming languages, since the 1970’s. We have also utilized simulation in our prior work, where we formalized and proved a folklore claim that the state-based and operation-based approaches to Conflict-free Replicated Data Types (CRDTs) are ‘equivalent’ since they can ‘emulate each other’. More specifically, a CRDT system consists of a collection of nodes called replicas. Clients interact with individual replicas by querying or updating their state, and replicas interact by message passing over a network to eventually reach a convergent state. There are two main approaches to implementing a CRDT: operation-based, and state-based. We showed that the main state-based and operation-based approaches to CRDTs do indeed ‘emulate each other’ since one can exhibit a pair of weak simulations between the original type of CRDT, and its corresponding translation into the other type. We then leveraged the existence of these weak simulations to formally prove a ‘representation independence’ result, in the sense that when access to the CRDTs is mediated by an imperative programming language, the programmer cannot discern the underlying CRDT implementation by producing a program that terminates when run using one type of CRDT implementation, but not when run with the other.
Unfortunately, our results are impractical for the purpose of being reapplied to asserting the equivalence of other replicated systems, since the simulation relations (that one needs to exhibit in order to prove the necessary representation-independence) are non-modular, requiring the user to reason about the potential executions of their entire replicated system. Additionally, we observed that behavioral equivalence of state-based and operation-based CRDTs is a specific instance of the more general paradigm of ‘emulation’, which is the process by which an ‘emulator’ translates the behavior of one system into the behavior of a different system.
We propose to generalize the techniques of our prior work to be applicable for any pair of replicated systems, and correct the ‘non-modularity’ issue by decomposing the overall proof structure into compositional simulation proofs about the local behavior of a replica, and the behavior of the communication medium. Our second proposal comes from the observation that, to our knowledge, ‘emulation’ has not been given a formal and general mathematical semantic model that adequately captures the practical nuances faced by researchers and practitioners working on emulators. With that in mind, we propose a notion of a faithful emulator, inspired by the concept of a faithful functor 𝐹 ∶ C → D which lets us regard objects in C as ‘the same as’ the objects in D, but with additional structure.
Host: Nathan Littschwager, Ph.D. Student, Computer Science and Engineering
Advisor: Lindsey Kuper
