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