Relaxing real-time order in opacity and linearizability

In this paper we introduce two families of safety properties: ♢-opacity and ♢-linearizability. The new properties relax (to a various degree) the real-time order requirement on transaction execution in opacity and, analogically, the real-time order requirement on operation execution in linearizabili...

Full description

Saved in:
Bibliographic Details
Published in:Journal of parallel and distributed computing 2017-02, Vol.100, p.57-70
Main Authors: Kobus, Tadeusz, Kokociński, Maciej, Wojciechowski, Paweł T.
Format: Article
Language:English
Subjects:
Computer networks
Concurrency
Correctness
Deferred update replication
Linearizability
Opacity
Real time
Real time operation
Replication
Safety
Semantics
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper we introduce two families of safety properties: ♢-opacity and ♢-linearizability. The new properties relax (to a various degree) the real-time order requirement on transaction execution in opacity and, analogically, the real-time order requirement on operation execution in linearizability. This way we can formalize the guarantees provided by a wide class of strongly consistent replicated systems for which opacity and linearizability are too strong. We show the formal relationship between ♢-opacity and ♢-linearizability which allows us to directly compare semantics of transactional and non-transactional systems and, in particular, opacity and linearizability in their original definitions. We also illustrate how the new properties can be used by proving correctness of Deferred Update Replication, a well known optimistic concurrency control scheme. We show that it satisfies update-real-time opacity, a member of the ♢-opacity family, which allows read-only and aborted transactions to operate on stale (but still consistent) data. •New properties relaxing to various degree opacity and linearizability are proposed.•A formal relationship between opacity and linearizability is provided.•Deferred Update Replication guarantees update-real-time opacity.
ISSN:0743-7315
1096-0848
DOI:10.1016/j.jpdc.2016.10.007