In this paper, we introduce KDB, a novel persistent key-value data store (a concurrent index) with rich linearizable semantics. In contrast to state-of-the-art systems which offer only lookup and put/remove operations, KDB supports both snapshots (which are used by range scans) and atomic batch updates—put and remove operations that are executed atomically. Despite its rich semantics, our system offers highly scalable performance across varied workloads thanks to its unique multiversioned architecture. It features a hybrid lock-CAS synchronization mechanism that allows lookup operations and scans to proceed in a wait-free fashion. Under the hood, KDB maintains all key-value entries in persistent memory (PM) for failure atomicity, but it heavily relies on an efficient DRAM-backed multiversion index based on skip lists to hide the costs of accessing PM. For better PM utilization, entries are arranged in PM in preallocated arrays that occasionally undergo compaction.

In this paper we introduce Jiffy, the first lock-free, linearizable, ordered key-value index that offers both (1) batch updates, i.e., put and remove operations that are executed atomically, and (2) consistent snapshots used by, e.g., range scan operations. Jiffy is built as a multiversioned lock-free skip list and relies on system-provided timestamps (e.g., on x86_64 obtained through the Time Stamp Counter register) to generate version numbers at minimal cost. For faster skip list traversals and better utilization of CPU caches, key-value entries are grouped into immutable objects called revisions. By (automatically) controlling the size of new revisions, our index can adapt to varying contention levels (e.g., smaller revisions are more suited for write-heavy workloads). Structure modifications to the index, which result in changing the size of revisions, happen through (lock-free) skip list node split and merge operations that are carefully coordinated with the update operations. Despite rich semantics, Jiffy offers highly scalable performance across varied workloads. Compared to Jiffy's lock-based rivals that support batch updates, our index can execute large batch updates up to 7.4 times more efficiently. Moreover, Jiffy often outperforms the state-of-the-art lock-free ordered indices that feature linearizable range scan operations but lack batch updates.

Abstract Transaction Memory (TM) is a concurrency control abstraction that allows the programmer to specify blocks of code to be executed atomically as transactions. However, since transactional code can contain just about any operation attention must be paid to the state of shared variables at any given time. E.g., contrary to a database transaction, if a TM transaction reads a stale value it may execute dangerous operations, like attempt to divide by zero, access an illegal memory address, or enter an infinite loop. Thus serializability is insufficient, and stronger safety properties are required in TM, which regulate what values can be read, even by transactions that abort. Hence, a number of TM safety properties were developed, including opacity, and TMS1 and TMS2. However, such strong properties preclude using prerelease as a technique for optimizing TM, because they virtually forbid reading from live transactions. On the other hand, properties that do allow prerelease are either not strong enough to prevent any of the problems mentioned above (recoverability), or add additional conditions on transactions that prerelease variables that limit their applicability (elastic opacity, live opacity, virtual world consistency). This paper introduces last-use opacity and strong last-use opacity, a pair of new TM safety properties meant to be a compromise between strong properties like opacity and minimal ones like serializability. The properties eliminate all but a small class of benign inconsistent views and pose no stringent conditions on transactions.

In this article we study the properties of distributed systems that mix eventual and strong consistency. We formalize such systems throughacute cloud types(ACTs), abstractions similar to conflict-free replicated data types (CRDTs), which by default work in a highly available, eventually consistent fashion, but which also feature strongly consistent operations for tasks which require global agreement. Unlike other mixed-consistency solutions, ACTs can rely on efficient quorum-based protocols, such as Paxos. Hence, ACTs gracefully tolerate machine and network failures also for the strongly consistent operations. We formally study ACTs and demonstrate phenomena which are neither present in purely eventually consistent nor strongly consistent systems. In particular, we identifytemporary operation reordering, which implies interim disagreement between replicas on the relative order in which the client requests were executed. When not handled carefully, this phenomenon may lead to undesired anomalies, including circular causality. We prove an impossibility result which states that temporary operation reordering is unavoidable in mixed-consistency systems with sufficiently complex semantics. Our result is startling, because it shows that apparentstrengtheningof the semantics of a system (by introducing strongly consistent operations to an eventually consistent system) results in the weakening of the guarantees on the eventually consistent operations.

Paxos is one of the most popular protocols for state machine replication (a technique used for making services highly available). We are the first to propose a Paxos-based state machine replication framework which is aimed at persistent (non-volatile) memory, pmem in short-a new class of memory offering direct byte-addressable access to memory (e.g., Optane ™ DC Persistent Memory). In the paper, we describe two variants of the framework, called mPaxosSM and mPaxos, which support efficient recovery of processes after crash with the use of pmem. In the latter variant, a part of Paxos's state, and in the former also the entire state machine's state that should survive crashes, are stored in the persistent memory. This allows to achieve low failure recovery time. We used a key-value map to compare our frameworks equipped with different memory backends (pmem, DRAM, and emulated pmem), with the classical Paxos that recovers state from snapshots and logs stored in stable storage, and with Paxos equipped with EpochSS-a state-of-the-art protocol ensuring state recovery from peer replicas. Our results show the advantages of pmem and our approach.

In this article, we propose and evaluate three different state recovery algorithms aimed for Paxos-one of the most popular distributed agreement protocols. Paxos is commonly used to maintain consistency among state machine replicas despite of failures of processes. The first algorithm, that we call FullSS, originates from the original Paxos and requires that the system frequently uses stable storage during regular (non-faulty) execution. The other two state recovery algorithms, ViewSS and EpochSS, scarcely require access to stable storage, and the recovering process must do much less work to restore its lost state, and to catch up on the current state of the system. We thoroughly analyze and compare the behavior of the three algorithms during state recovery and also during regular, non-faulty system execution, under various workloads (e.g., causing the network or CPU saturation). The experimental results show that by using ViewSS and EpochSS, we can significantly improve process recovery with respect to the original Paxos, if only it can be assumed that at any time a majority of replicas are up running (excluding those replicas that are just recovering). Moreover, these algorithms do not impact the performance of Paxos during regular (non-faulty) operation. However, FullSS is the only choice out of the three, if the system must tolerate catastrophic failures.

In this paper we study the properties of eventually consistent distributed systems that feature arbitrarily complex semantics and mix eventual and strong consistency. These systems execute requests in a highly-available, weakly-consistent fashion, but also enable stronger guarantees through additional inter-replica synchronization mechanisms that require the ability to solve distributed consensus. We use the seminal Bayou system as a case study, and then generalize our findings to a whole class of systems. We show dubious and unintuitive behaviour exhibited by those systems and provide a theoretical framework for reasoning about their correctness. We also state an impossibility result that formally proves the inherent limitation of such systems, namely temporary operation reordering, which admits interim disagreement between replicas on the relative order in which the client requests were executed.

Summary Transactional memory (TM) is an approach to concurrency control that aims to make writing parallel programs both effective and simple. The approach has been initially proposed for nondistributed multiprocessor systems, but it is gaining popularity in distributed systems to synchronize tasks at large scales. Efficiency and scalability are often the key issues in TM research; thus, performance benchmarks are an important part of it. However, while standard TM benchmarks like the Stanford Transactional Applications for Multi‐Processing suite and STMBench7 are available and widely accepted, they do not translate well into distributed systems. Hence, the set of benchmarks usable with distributed TM systems is very limited, and must be padded with microbenchmarks, whose simplicity and artificial nature often makes them uninformative or misleading. Therefore, this paper introduces Helenos, a realistic, complex, and comprehensive distributed TM benchmark based on the problem of the Facebook inbox, an application of the Cassandra distributed store.

We propose Hybrid Transactional Replication (HTR), a novel replication scheme for highly dependable services. It combines two schemes: a transaction is executed either optimistically by only one service replica in the deferred update mode (DU), or deterministically by all replicas in the state machine mode (SM); the choice is made by an oracle. The DU mode allows for parallelism and thus takes advantage of multicore hardware. In contrast to DU, the SM mode guarantees abort-free execution, soit is suitable for irrevocable operations and transactions generating high contention. For expressiveness, transactions can be discarded or retried on demand. We prove that the higher flexibility of the scheme does not come at the cost of weaker guarantees for clients: HTR satisfies strong consistency guarantees akin to those provided by other popular transactional replication schemes such as Deferred Update Replication. We developed HTR-enabled Paxos STM, an object-based distributed transactional memory system, and evaluated it thoroughly under various workloads. We show the benefits of using a novel oracle that relies on machine learning techniques for automatic adaptation to changing conditions. The ML-based oracle, based on algorithms for the multi-armed bandit problem, provides up to 50 percent improvement in throughput when compared to the system running with DU-only or SM-only oracles.

Transactional memory (TM) aims to be a general purpose concurrency mechanism. However, operations which cause side-effects cannot be easily managed by a TM system, in which transactions are executed optimistically. In particular, networking, I/O, and some system calls cannot be executed within a transaction that may abort and restart (e.g., due to conflicts). Thus, many TM systems let transactions become irrevocable, i.e., they are guaranteed to commit. Supporting this in TM is a challenge, but there exist fast and highly parallel TM systems that allow for irrevocable transactions. However, no such system so far provides guarantees that all transactional operations terminate in a finite time. In this paper, we show that support for irrevocable operations does not entail inherent waiting. We present a TM algorithm that guarantees wait-freedom for any transactional operation. The algorithm is based on the weakest synchronization primitive possible (test-and-set), and guarantees opacity and strong progressiveness. To experimentally evaluate the algorithm, we developed a proof-of-concept TM system and tested it using the STMBench7 benchmark.

In the paper, we analyze and experimentally compare two popular replication schemes relying on atomic broadcast: state machine replication (SMR) and deferred update replication (DUR). We estimate the lower bounds on the time of executing requests by the SMR and DUR systems running on multi-core servers. We also consider variants of systems that can process read-only requests with a lower overhead. In the analysis of DUR, we consider conflict patterns. We then formally show the scalability of SMR and DUR, which reflects the capacity of systems to effectively utilize an increasing number of processor cores. Next, we compare SMR and DUR experimentally under different levels of contention, using several benchmarks. We show throughput, abort rate (in DUR), and network congestion. The key results of our work are that neither system is superior in all cases, and that the theoretical and experimental results are heavily influenced by the dominance of either the CPU execution time or atomic broadcast time. We therefore propose to combine both replication schemes and gain the best of both worlds.

Eventually consistent linearizability (ec-linearizability) is a new correctness condition for eventually consistent distributed systems (modeled as shared objects). Unlike the existing definitions of eventual consistency, ec-linearizability is suitable for describing the behaviour of some popular eventually consistent systems, such as Cassandra. It is because ec-linearizability allows for certain types of phenomena, such as lost updates. Similarly to linearizability, ec-linearizability is a safety property and is both local and nonblocking. Thus, ec-linearizability is a property that is both easy to use and reason about.

In this paper we propose executive deferred update replication (EDUR), a novel algorithm for multi-primary replication of transactional memory and databases. EDUR streamlines transaction certification (i.e., checking for conflicts between concurrent transactions) with the broadcast protocol, which improves overall performance and scalability compared to deferred update replication based on total order broadcast (TOB). EDUR uses executive order broadcast (EOB), a novel protocol that can be seen as a generalization of TOB. Compared to TOB, EOB features new primitives and properties that enable the application to delegate some work to a leader -- a process inherently present in many TOB algorithms that is responsible for coordination of message dissemination. The results of experimental evaluation show significant performance gains when using our approach.

We propose a novel algorithm for hybrid transactional replication (HTR) of highly dependable services. It combines two schemes: a transaction is executed either optimistically by only one service replica in the deferred update mode (DU), or deterministically by all replicas in the state machine mode (SM); the choice is made by an oracle. The DU mode allows for parallelism and thus takes advantage of multicore hardware. In contrast to DU, the SM mode guarantees abort-free execution, so it is suitable for irrevocable operations and transactions generating high contention. For expressiveness, transactions can be discarded or retried on demand. We developed HTR-enabled Paxos STM, an object-based distributed transactional memory system, and evaluated it using several benchmarks: Bank, Distributed STMBench7, and Twitter Clone. We tested our system under various workloads and three oracle types: DU and SM, which execute all transactions in one mode, and Hybrid -- tailored specifically for each benchmark -- which selects a mode for each transaction dynamically based on various parameters. In all our tests, the Hybrid oracle is not worse than DU and SM and outperforms them when the number of replicas grows.

Transactional memory, an approach aiming to replace cumbersome locking mechanisms in concurrent systems, has become a popular research topic. But due to problems posed by irrevocable operations (e.g., system calls), the viability of pessimistic concurrency control for transactional memory systems is being explored, in lieu of the more typical optimistic approach. However, in a distributed setting, where partial transaction failures may happen, the inability of pessimistic transactional memories to roll back is a major shortcoming. Therefore, this paper presents a novel transactional memory concurrency control algorithm that is both fully pessimistic and rollback-capable.

In this paper, we analyze and experimentally compare state-machine-based and deferred-update (or transactional) replication, both relying on atomic broadcast. We define a model that describes the upper and lower bounds on the execution of concurrent requests by a service replicated using either scheme. The model is parametrized by the degree of parallelism in either scheme, the number of processor cores, and the type of requests. We analytically compared both schemes and a non-replicated service, considering a bcast- and request-execution-dominant workloads. To evaluate transactional replication experimentally, we developed Paxos STM---a novel fault-tolerant distributed software transactional memory with programming constructs for transaction creation, abort, and retry. For state-machine-based replication, we used JPaxos. Both systems share the same implementat ion of atomic broadcast based on the Paxos algorithm. We present the results of performance evaluation of both replication schemes, and a non-replicated (thus prone to failures) service, considering various workloads. The key result of our theoretical and experimental work is that neither system is superior in all cases. We discuss these results in the paper.

Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, implementation, and verification of overlay networks to support reliable communication between migrating computations, in the Nomadic Pict project. We define two levels of abstraction as calculi with precise semantics: a low-level Nomadic π calculus with migration and location-dependent communication, and a high-level calculus that adds location-independent communication. Implementations of location-independent communication, as overlay networks that track migrations and forward messages, can be expressed as translations of the high-level calculus into the low. We discuss the design space of such overlay network algorithms and define three precisely, as such translations. Based on the calculi, we design and implement the Nomadic Pict distributed programming language, to let such algorithms (and simple applications above them) to be quickly prototyped. We go on to develop the semantic theory of the Nomadic π calculi, proving correctness of one example overlay network. This requires novel equivalences and congruence results that take migration into account, and reasoning principles for agents that are temporarily immobile (e.g., waiting on a lock elsewhere in the system). The whole stands as a demonstration of the use of principled semantics to address challenging system design problems.

In this paper, we study dynamic protocol update (DPU). Contrary to local code updates on-the-fly, DPU requires global coordination of local code replacements. We propose a novel solution to DPU. The key idea is to add a level of indirection between the service callers and the service provider. This indirection level facilitates an implementation of simple and efficient algorithms for DPU. For example, we describe an experimental implementation of adaptive group communication middleware. It can switch between different atomic broadcast protocols on-the-fly. All middleware protocols, including those that depend on the updated protocols, provide service correctly and with negligible delay while the global update takes places. The switching algorithm introduces very low overhead that we illustrate by showing example measurement results.

In this paper we design a language and runtime support for isolation-only, multithreaded transactions (called tasks). Tasks allow isolation to be declared instead of having to be encoded using the low-level synchronization constructs. The key concept of our design is the use of a type system to support rollback-free and safe runtime execution of tasks.We present a first-order type system which can verify information for the concurrency controller. We use an operational semantics to formalize and prove the type soundness result and an isolation property of tasks. The semantics uses a specialized concurrency control algorithm, that is based on access versioning.

Summary form only given. We address programming abstractions for building protocols from smaller, reusable microprotocols. The existing protocol frameworks, such as Appia and Cactus, either restrict the amount of concurrency between microprotocols, or depend on the programmer, who should implement all the necessary synchronisation using standard language facilities. We develop J-SAMOA: a framework for a synchronisation augmented microprotocol approach in Java. It has been designed to allow concurrent protocols to be expressed without explicit low-level synchronisation, thus making programming easier and less error-prone. We describe versioning concurrency control algorithms. They are used by the runtime system of our framework to guarantee that the concurrent execution of a protocol is equivalent to a serial execution of its microprotocols. This guarantee, called the isolation property, ensures consistency of session or message-specific data maintained by microprotocols.