The CISE tool: Proving weakly-consistent applications correct

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

doi:10.1145/2911151.2911160

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 proceeding › Conference contribution › peer-review

25 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 language	English
Title of host publication	Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC 2016
Publisher	ACM - Association for Computing Machinery
ISBN (Electronic)	978-1-4503-3537-9
DOIs	https://doi.org/10.1145/2911151.2911160
Publication status	Published - 2016
Event	2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC) - London Duration: 18 Apr 2016 → …

Conference

Conference	2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC)
City	London
Period	18/04/16 → …

Keywords

Consistency
Invariant
Program analysis

Access to Document

10.1145/2911151.2911160Licence: Unspecified

Cite this

@inproceedings{221c83dffe764749b1fb6b36e54614d5,

title = "The CISE tool: Proving weakly-consistent applications correct",

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.",

keywords = "Consistency, Invariant, Program analysis",

author = "Mahsa Najafzadeh and Alexey Gotsman and Hongseok Yang and Carla Ferreira and Marc Shapiro",

note = "Sem PDF conforme despacho; 2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC) ; Conference date: 18-04-2016",

year = "2016",

doi = "10.1145/2911151.2911160",

language = "English",

booktitle = "Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC 2016",

publisher = "ACM - Association for Computing Machinery",

address = "United States",

}

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. ACM - Association for Computing Machinery, 2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC), London, 18/04/16. https://doi.org/10.1145/2911151.2911160

The CISE tool: Proving weakly-consistent applications correct. / Najafzadeh, Mahsa; Gotsman, Alexey; Yang, Hongseok et al.
Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC 2016. ACM - Association for Computing Machinery, 2016.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - The CISE tool: Proving weakly-consistent applications correct

AU - Najafzadeh, Mahsa

AU - Gotsman, Alexey

AU - Yang, Hongseok

AU - Ferreira, Carla

AU - Shapiro, Marc

N1 - Sem PDF conforme despacho

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Consistency

KW - Invariant

KW - Program analysis

UR - http://www.scopus.com/inward/record.url?scp=84969941337&partnerID=8YFLogxK

U2 - 10.1145/2911151.2911160

DO - 10.1145/2911151.2911160

M3 - Conference contribution

AN - SCOPUS:84969941337

BT - Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC 2016

PB - ACM - Association for Computing Machinery

T2 - 2nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC)

Y2 - 18 April 2016

ER -

The CISE tool: Proving weakly-consistent applications correct

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this