Nicholas V. Lewchenko

arXiv2018

Conflict-Aware Replicated Data Types

We introduce Conflict-Aware Replicated Data Types (CARDs). CARDs are significantly more expressive than Conflict-free Replicated Data Types (CRDTs) as they support operations that can conflict with each other. Introducing conflicting operations typically brings the need to block an operation in at least some executions, leading to difficulties in programming and reasoning about correctness, as well as potential inefficiencies in implementation. The salient aspect of CARDs is that they allow ease of programming and reasoning about programs comparable to CRDTs, while enabling algorithmic inference of conflicts so that an operation is blocked only when necessary. The key idea is to have a language that allows associating with each operation a two-state predicate called {\em consistency guard} that relates the state of the replica on which the operation is executing to a global state (which is never computed). The consistency guards bring three advantages. First, a programmer developing an operation needs only to choose a consistency guard that states what the operation will rely on. In particular, they do not need to consider the operation conflicts with other operation. This allows purely {\em modular reasoning}. Second, we show that consistency guard allow reducing the complexity of reasoning needed to prove invariants that hold as CARD operations are executing. The reason is that consistency guard allow reducing the reasoning about concurrency among operations to purely {\em sequential reasoning}. Third, conflicts among operations can be algorithmically inferred by checking whether the effect of one operation preserves the consistency guard of another operation.

cs.DC↗

arXiv2018

DroidStar: Callback Typestates for Android Classes

Event-driven programming frameworks, such as Android, are based on components with asynchronous interfaces. The protocols for interacting with these components can often be described by finite-state machines we dub *callback typestates*. Callback typestates are akin to classical typestates, with the difference that their outputs (callbacks) are produced asynchronously. While useful, these specifications are not commonly available, because writing them is difficult and error-prone. Our goal is to make the task of producing callback typestates significantly easier. We present a callback typestate assistant tool, DroidStar, that requires only limited user interaction to produce a callback typestate. Our approach is based on an active learning algorithm, L*. We improved the scalability of equivalence queries (a key component of L*), thus making active learning tractable on the Android system. We use DroidStar to learn callback typestates for Android classes both for cases where one is already provided by the documentation, and for cases where the documentation is unclear. The results show that DroidStar learns callback typestates accurately and efficiently. Moreover, in several cases, the synthesized callback typestates uncovered surprising and undocumented behaviors.

cs.LO↗