Combining State- and Event-Based Semantics to Verify Highly Available Programs

Abstract

Replicated databases are attractive for managing the data of distributed applications that require high availability, low latency, and high throughput. However, these benefits entail weak consistency which comes at a price: it becomes harder to reason about application correctness. We address this difficulty with a verification technique for highly available programs. We augment an existing sequential programming language with primitives for interacting concurrently with a highly available database and extend the state-based operational semantics of that language accordingly. To this end we make use of existing event-based database semantics. We then present a reduction of the extended semantics to a simpler one, which is again sequential and therefore easier to handle in verification tools. Our verification tool Repliss uses this technique and demonstrates its feasibility.