The CISE tool: Proving weakly-consistent applications correct

Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, Marc Shapiro

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)

Abstract

Designers of a replicated database face a vexing choice between strong consistency, which ensures certain application invariants but is slow and fragile, and asynchronous replication, which is highly available and responsive, but exposes the programmer to unfamiliar behaviours. To bypass this conundrum, recent research has studied hybrid consistency models, in which updates are asynchronous by default, but synchronisation is available upon request. To help programmers exploit hybrid consistency, we propose the first static analysis tool for proving integrity invariants of applications using databases with hybrid consistency models. This allows a programmer to find minimal consistency guarantees sufficient for application correctness.
Original languageEnglish
Title of host publicationProceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC 2016
PublisherAssociation for Computing Machinery
ISBN (Electronic)978-1-4503-3537-9
DOIs
Publication statusPublished - 2016
Event2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC) - London
Duration: 18 Apr 2016 → …

Conference

Conference2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC)
CityLondon
Period18/04/16 → …

Keywords

  • Consistency
  • Invariant
  • Program analysis

Fingerprint Dive into the research topics of 'The CISE tool: Proving weakly-consistent applications correct'. Together they form a unique fingerprint.

  • Cite this

    Najafzadeh, M., Gotsman, A., Yang, H., Ferreira, C., & Shapiro, M. (2016). The CISE tool: Proving weakly-consistent applications correct. In Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC 2016 Association for Computing Machinery. https://doi.org/10.1145/2911151.2911160