Checking robustness between weak transactional consistency models
From MaRDI portal
Publication:2233450
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Database theory (68P15) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: Concurrent accesses to databases are typically encapsulated in transactions in order to enable isolation from other concurrent computations and resilience to failures. Modern databases provide transactions with various semantics corresponding to different trade-offs between consistency and availability. Since a weaker consistency model provides better performance, an important issue is investigating the weakest level of consistency needed by a given program (to satisfy its specification). As a way of dealing with this issue, we investigate the problem of checking whether a given program has the same set of behaviors when replacing a consistency model with a weaker one. This property known as robustness generally implies that any specification of the program is preserved when weakening the consistency. We focus on the robustness problem for consistency models which are weaker than standard serializability, namely, causal consistency, prefix consistency, and snapshot isolation. We show that checking robustness between these models is polynomial time reducible to a state reachability problem under serializability. We use this reduction to also derive a pragmatic proof technique based on Lipton's reduction theory that allows to prove programs robust. We have applied our techniques to several challenging applications drawn from the literature of distributed systems and databases.
Recommendations
- Robustness Against Transactional Causal Consistency.
- scientific article; zbMATH DE number 7327945
- Verifying visibility-based weak consistency
- scientific article; zbMATH DE number 2001224
- Robustness against consistency models with atomic visibility
- Transactions for software model checking
- scientific article; zbMATH DE number 4049031
- Model checking transactional memories
- Consistent checkpointing for transaction systems
- Characterizing Transactional Memory Consistency Conditions Using Observational Refinement
Cites work
- 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
- A framework for transactional consistency models with atomic visibility
- Algebraic laws for weak consistency
- Analysing snapshot isolation
- Automated detection of serializability violations under weak consistency
- Checking and enforcing robustness against TSO
- Checking robustness between weak transactional consistency models
- Deciding Robustness against Total Store Ordering
- Effective abstractions for verification under relaxed memory models
- scientific article; zbMATH DE number 7327945 (Why is no real title available?)
- Ogre and Pythia: an invariance proof method for weak consistency models
- On the semantics of snapshot isolation
- On the verification problem for weak memory models
- On verifying causal consistency
- Owicki-Gries reasoning for weak memory models
- Reduction
- Replicated data types, specification, verification, optimality
- Robustness against consistency models with atomic visibility
- Robustness against Power is PSpace-complete
- Serializability for eventual consistency: criterion, analysis, and applications
- The covering and boundedness problems for vector addition systems
- The serializability of concurrent database updates
- Time, clocks, and the ordering of events in a distributed system
- Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017. Proceedings.
- What's decidable about weak memory models?
Cited in
(14)- Checking robustness between weak transactional consistency models
- ROLA: a new distributed transaction protocol and its formal analysis
- Checking causal consistency of distributed databases
- Robustness against consistency models with atomic visibility
- Automated detection of serializability violations under weak consistency
- Algebraic laws for weak consistency
- A framework for transactional consistency models with atomic visibility
- scientific article; zbMATH DE number 7327945 (Why is no real title available?)
- Robustness Against Transactional Causal Consistency.
- Monitoring weak consistency
- Robustness against Read Committed for Transaction Templates with Functional Constraints
- Checking robustness against snapshot isolation
- Optimal stateless model checking for causal consistency
- Formalizing and checking multilevel consistency
This page was built for publication: Checking robustness between weak transactional consistency models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233450)
