Sequential programming for replicated data stores
Abstract
We introduce Carol, a refinement-typed programming language for replicated data stores. The salient feature of Carol is that it allows programming and verifying replicated store operations modularly , without consideration of other operations that might interleave, and sequentially , without requiring reference to or knowledge of the concurrent execution model. This is in stark contrast with existing systems, which require understanding the concurrent interactions of all pairs of operations when developing or verifying them.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jul 26, 2019
- Source ID
- 10.1145/3341710
Entities
People
- Akash Gaonkar
- Arjun Radhakrishna
- Nicholas V. Lewchenko
- Pavol Černý
Organizations
- Defense Advanced Research Projects Agency
- Microsoft
- University of Colorado Boulder