Read atomic transactions with prevention of lost updates: ROLA and its formal analysis

DOI10.1007/S00165-019-00489-WzbMATH Open1425.68096OpenAlexW2901599465MaRDI QIDQ2335948FDOQ2335948

Authors: Si Liu, Peter Csaba Ölveczky, Qi Wang, José Meseguer, Indranil Gupta 

Publication date: 18 November 2019

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2142/101836

Recommendations

• ROLA: a new distributed transaction protocol and its formal analysis
• scientific article; zbMATH DE number 97098
• A framework for transactional consistency models with atomic visibility
• Relaxing consistency requirement for read-only transactions
• Robustness against consistency models with atomic visibility

zbMATH Keywords

performance evaluationstatistical model checkingrewriting logicMaudedistributed database systemstransaction protocolsconsistency models

Mathematics Subject Classification ID

Database theory (68P15) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Statistical probabilistic model checking with a focus on time-bounded properties
• Conditional rewriting logic as a unified model of concurrency
• Title not available (Why is that?)
• Semantics and pragmatics of real-time maude
• Computer Aided Verification
• Statistical model checking for composite actor systems
• A framework for transactional consistency models with atomic visibility
• ROLA: a new distributed transaction protocol and its formal analysis
• Scalable atomic visibility with RAMP transactions
• Formalizing and validating the \(P\)-Store replicated data store in Maude
• Pascal's prism

Cited In (4)

• ROLA: a new distributed transaction protocol and its formal analysis
• Scalable atomic visibility with RAMP transactions
• Building correct-by-construction systems with formal patterns
• Automatic analysis of consistency properties of distributed transaction systems in Maude

Uses Software

• PRISM
• Maude
• PMaude
• PVeStA
• VESTA
• MODIST
• SAMC
• IronFleet

This page was built for publication: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2335948)