Cloud Types for Eventual Consistency
Intervenant(s) : Sebastian Burckhardt, Microsoft Research Redmond
When writing applications for mobile devices sharing data in the cloud, it is often desirable to support seamless offline operation. This can be achieved by using local replicas that support queries and updates even if disconnected. However, implementation of such systems can be challenging, and it is often not clear how to separate system details (transport, storage) from application-specific logic (conflict resolution).
To raise the abstraction level of such programs, we propose the use of cloud types that seamlessly integrate into the programming language. Cloud types empower programmers to simultaneously express the structure of the shared data, and its semantics under concurrent updates. The consistency model is based on revision diagrams, a type of graph reminiscent of source control systems, and guarantees causally and eventually consistent transactions. We show how our prototype enables programmers to write simple apps using cloud types, and to reason about their executions using revision diagrams.