This article presents a theoretical study of the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is impossible to runtime verify linearizability for some common sequential objects, regardless of the consensus power of base objects. Then, it argues that a variant of the problem, which we call predictive verification, can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be predictively verified using only read/write base objects (i.e., without the need of consensus), and (2) any implementation can be transformed to its counterpart in the class using only read/write objects. As far as we know, this is the first runtime verification algorithm for any correctness condition that is fully asynchronous and fault-tolerant. As a by-product, it is obtained a simple and generic methodology for deriving linearizable implementations that runtime verify their responses, and are able to produce a history certifying this, properties that allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. We call such implementations self-enforced linearizable. The results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability.

Linearizability is the standard correctness condition for concurrent data structures. Even when an algorithm has been proved correct theoretically, translating it into code may introduce subtle errors that are difficult to detect. Existing runtime verification tools rely on intrusive instrumentation that introduces false positives and false negatives, as the observed execution may differ from the actual one. This paper presents an open-source verification framework for runtime verification of linearizability. The framework treats the system as a black box, requiring only the class name of the concurrent implementation. It consists of two layers: an instrumentation layer, that provides two algorithms based on non-linearizable objects that obtain the current execution without modifying the system under inspection; and a monitoring layer, which decides whether the observed execution is linearizable. The framework is sound : if the observed execution is not linearizable, the real execution is also not linearizable, and a witness history is produced. False negatives are possible — the framework may report linearizable when the real execution is not — but this is the best achievable given the impossibility result of [1]. The framework is implemented in Java and Clojure, supports queues, deques, sets, and maps, and can be extended to other data structures by providing their sequential specification. It is intended for the testing phase of concurrent software development, helping developers and researchers validate that a concurrent implementation matches its theoretical design before deployment.

Implementing correct distributed systems is an error-prone task. Runtime Verification (RV) offers a lightweight formal method to improve reliability by monitoring system executions against correctness properties. However, applying RV in distributed settings—where no process has global knowledge—poses fundamental challenges, particularly under full asynchrony and fault tolerance. This paper addresses the Distributed Runtime Verification (DRV) problem under such conditions. In our model, each process in a distributed monitor receives a fragment of the input word describing system behavior and must decide whether this word belongs to the language representing the correctness property being verified. Hence, the goal is to decide languages in a distributed fault-tolerant manner. We propose several decidability definitions, study the relations among them, and prove possibility and impossibility results. One of our main results is a characterization of the correctness properties that can be decided asynchronously. Remarkably, it applies to any language decidability definition. Intuitively, the characterization is that only properties with no real-time order constraints can be decided in asynchronous fault-tolerant settings. These results expose the expressive limits of DRV in realistic systems, as several properties of practical interest rely on reasoning about real-time order of events in executions. To overcome these limitations, we introduce a weaker model where the system under inspection is verified indirectly. Under this weaker model we define predictive decidability, a decidability definition that turn some real-time sensitive correctness properties verifiable. Our framework unifies and extends existing DRV theory and sharpens the boundary of runtime monitorability under different assumptions.

Abstract When a concrete concurrent object refines another, more abstract object, the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This approach is sound for trace properties of the program, but not for hyperproperties, including many security properties and probability distributions of events. We define strong observational refinement, a strengthening of refinement that preserves hypersafety properties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability, a restriction of linearizability, the prevalent consistency condition for implementing concurrent objects. Our results imply that strong linearizability is also equivalent to existence of forward simulations, and show that strongly linearizable implementations can be composed both horizontally and vertically. This paper also investigates whether there are wait-free strongly-linearizable implementations from realistic primitives such as test&set or fetch&add, whose consensus number is 2. We show that many objects with consensus number 1 have wait-free strongly-linearizable implementations from fetch&add. We also show that several objects with consensus number 2 have wait-free or lock-free implementations from other objects with consensus number 2. In contrast, we prove that even when fetch&add, swap and test&set primitives are used, some objects with consensus number 2 do not have lock-free strongly-linearizable implementations. This includes queues and stacks, and relaxed variants thereof.

A powerful tool for designing complex concurrent programs is through composition with object implementations from lower-level primitives. Strongly-linearizable implementations allow to preserve hyper-properties, e.g., probabilistic guarantees of randomized programs. However, the only known wait-free strongly-linearizable implementations for many objects rely on compare&swap, a universal primitive that allows any number of processes to solve consensus. This is despite the fact that these objects have wait-free linearizable implementations from read / write primitives, which do not support consensus. This paper investigates a middle-ground, asking whether there are wait-free strongly-linearizable implementations from realistic primitives such as test&set or fetch&add, whose consensus number is 2.

We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach lies in characterizing memory models by their mergeability properties, identifying restrictions under which independent memory traces can be merged into a single valid memory trace. In turn, we show that the mergeability properties of the underlying memory model entail similar mergeability requirements on the specifications of objects that can be implemented on that memory model. We demonstrate the applicability of our approach to establish the impossibility of implementing standard distributed objects with different restrictions on memory traces on three memory models: strictly consistent memory, total store order, and release-acquire. These impossibility results allow us to identify tight and almost tight bounds for some objects, as well as new separation results between weak memory models, and between well-studied objects based on their implementability on weak memory models.

Abstract We introduce pattern models, a dynamic epistemic logic for analyzing distributed systems. First, we present a version of pattern models where the full-information protocol, widely studied in distributed computability, is static in the product definition of pattern models. Next, we parametrize such a logic so as to add the capability to model dynamics of arbitrary deterministic protocols. We thus give a systematic construction of pattern models for a large variety of distributed-computing models called dynamic-network models. Using pattern models, the epistemic dynamics of a proper subclass of dynamic-network models called oblivious can be described using a static pattern model, hence using constant space. For this case, we present a sufficient unsolvability condition for the consensus task that can be easily verified analyzing the structure of the initial epistemic model and the pattern model for a given oblivious dynamic-network model.

This paper studies the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is impossible to runtime verify linearizability for some common sequential objects, regardless of the consensus power of base objects. Then, it argues that actually a stronger version of the problem can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be strongly verified using only read/write base objects (i.e. without the need of consensus), and (2) any implementation can be transformed to its counterpart in the class (which implements the same object) using only read/write objects too. As far as we know, this is the first runtime verification algorithm for any correctness condition that is fully asynchronous and fault-tolerant. As a by-product, a simple and generic methodology for deriving self-enforced linearizable implementations is obtained. This type implementations produce outputs that are guaranteed linearizable, and are able to produce a certificate of it, which allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. These results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability.

The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.

It is known that any algorithm for work-stealing in the standard asynchronous shared memory model must use expensive Read-After-Write synchronization patterns or atomic Read-Modify-Write instructions. There have been proposed algorithms for relaxations in the standard model and algorithms in restricted models that avoid the impossibility result, but only in some operations. This paper considers work-stealing with multiplicity, a relaxation in which every task is taken by at least one operation, with the requirement that any process can extract a task at most once. Two versions of the relaxation are considered and two fully Read/Write algorithms are presented in the standard asynchronous shared memory model, both devoid of Read-After-Write synchronization patterns in all its operations, the second algorithm additionally being fully fence-free, namely, no specific ordering among the algorithm’s instructions is required, beyond what is implied by data dependence. To our knowledge, these are the first algorithms for work-stealing possessing all these properties. Our algorithms are also wait-free solutions of relaxed versions of single-enqueue multi-dequeuer queues. The algorithms are obtained by reducing work-stealing with multiplicity and weak multiplicity to MaxRegister and RangeMaxRegister, a relaxation of MaxRegister which might be of independent interest. An experimental evaluation shows that our fully fence-free algorithm exhibits better performance than Cilk THE, Chase-Lev and Idempotent Work-Stealing algorithms.

An elegant strategy for proving impossibility results in distributed computing was introduced in the celebrated FLP consensus impossibility proof. This strategy is local in nature as at each stage, one configuration of a hypothetical protocol for consensus is considered, together with future valencies of possible extensions. This proof strategy has been used in numerous situations related to consensus, leading one to wonder why it has not been used in impossibility results of two other well-known tasks: set agreement and renaming. This paper provides an explanation of why impossibility proofs of these tasks have been of a global nature. It shows that a protocol can always solve such tasks locally, in the following sense. Given a configuration and all its future valencies, if a single successor configuration is selected, then the protocol can reveal all decisions in this branch of executions, satisfying the task specification. This result is shown for both set agreement and renaming, implying that there are no local impossibility proofs for these tasks.

Considering asynchronous shared memory systems in which any number of processes may crash, this work identifies and formally defines relaxations of queues and stacks that can be non-blocking or wait-free while being implemented using only read/write operations. Set-linearizability and Interval-linearizability are used to specify the relaxations formally, and precisely identify the subset of executions which preserve the original sequential behavior. The relaxations allow for an item to be returned more than once by different operations, but only in case of concurrency; we call such a property multiplicity. The stack implementation is wait-free, while the queue implementation is non-blocking. Interval-linearizability is used to describe a queue with multiplicity, with the additional relaxation that a dequeue operation can return weak-empty, which means that the queue might be empty. We present a read/write wait-free interval-linearizable algorithm of a concurrent queue. As far as we know, this work is the first that provides formalizations of the notions of multiplicity and weak-emptiness, which can be implemented on top of read/write registers only.

Round-based models are very common message-passing models; combinatorial topology applied to distributed computing provides sweeping results like general lower bounds. We combine both to study the computability of k-set agreement.

More than two decades ago, combinatorial topology was shown to be useful for analyzing distributed fault-tolerant algorithms in shared memory systems and in message passing systems. In this work, we show that combinatorial topology can also be useful for analyzing distributed algorithms in networks of arbitrary structure. To illustrate this, we analyze consensus, set-agreement, and approximate agreement in networks, and derive lower bounds for these problems under classical computational settings, such as the LOCAL model and dynamic networks.

The $M(n)$-renaming task requires $n+1$ processes, each starting with a unique input name (from an arbitrary large range), to coordinate the choice of new output names from a range of size $M(n)$. It is known that $2n$-renaming can be solved if and only if $n+1$ is not a prime power. However, the previous proof of solvability was not constructive, involving a complex approximation theorem, and so it did not yield a concrete upper bound on the complexity of the resulting protocol. Here, we present the first upper bound on the step complexity of $2n$-renaming, whenever it is solvable, i.e., when $n+1$ is not a prime power. The paper also presents the first lower bound on the output namespace, showing that if $n+1$ is not a prime power and $n$ is a prime power, then $2n$ is a tight bound on the output namespace for $n+1$ processes.

A long-standing open question has been whether lock-freedom and wait-freedom are fundamentally different progress conditions, namely, can the former be provided in situations where the latter cannot? This paper answers the question in the affirmative, by proving that there are objects with lock-free implementations, but without wait-free implementations-using objects of any finite power. We precisely define an object called n-process long-lived approximate agreement (n-LLAA), in which two sets of processes associated with two sides, 0 or 1, need to decide on a sequence of increasingly closer outputs. We prove that 2-LLAA has a lock-free implementation using reads and writes only, while n-LLAA has a lock-free implementation using reads, writes and (n - 1)-process consensus objects. In contrast, we prove that there is no wait-free implementation of the n-LLAA object using reads, writes and specific (n - 1)-process consensus objects, called (n - 1)-window registers.

Tasks and objects are two predominant ways of specifying distributed problems where processes should compute outputs based on their inputs. Roughly speaking, a task specifies, for each set of processes and each possible assignment of input values, their valid outputs. In contrast, an object is defined by a sequential specification. Also, an object can be invoked multiple times by each process, while a task is a one-shot problem. Each one requires its own implementation notion, stating when an execution satisfies the specification. For objects, linearizability is commonly used, while tasks implementation notions are less explored. The article introduces the notion of interval-sequential object, and the corresponding implementation notion of interval-linearizability , to encompass many problems that have no sequential specification as objects. It is shown that interval-sequential specifications are local , namely, one can consider interval-linearizable object implementations in isolation and compose them for free, without sacrificing interval-linearizability of the whole system. The article also introduces the notion of refined tasks and its corresponding satisfiability notion. In contrast to a task, a refined task can be invoked multiple times by each process. Also, objects that cannot be defined using tasks can be defined using refined tasks. In fact, a main result of the article is that interval-sequential objects and refined tasks have the same expressive power and both are complete in the sense that they are able to specify any prefix-closed set of well-formed executions. Interval-linearizability and refined tasks go beyond unifying objects and tasks; they shed new light on both of them. On the one hand, interval-linearizability brings to task the following benefits: an explicit operational semantics, a more precise implementation notion, a notion of state, and a locality property. On the other hand, refined tasks open new possibilities of applying topological techniques to objects.

The LOOK-COMPUTE-MOVE model for a set of autonomous robots has been thoroughly studied for over two decades. Each robot repeatedly LOOKS at its surroundings and obtains a snapshot containing the positions of all robots; based on this information, the robot COMPUTES a destination and then MOVES to it. Previous work assumed all robots are present at the beginning of the computation. What would be the effect of robots appearing asynchronously? This paper studies thisquestion, for problems of bringing the robots close together, andexposes an intimate connection with combinatorial topology. A central problem in the mobile robots area is the gathering problem. In its discrete version, the robots start at vertices in some graph G known to them, move towards the same vertex and stop. The paper shows that if robots are asynchronous and may crash, then gathering is impossible for any graph G with at least two vertices, even if robots can have unique IDs, remember the past, know the same names for the vertices of G and use an arbitrary number of lights to communicate witheach other. Next, the paper studies two weaker variants of gathering: edge gathering and 1-gathering. For both problems we present possibility and impossibility results. The solvability of edge gathering is fully characterized: it is solvable for three or more robots on a given graph if and only if the graph is acyclic. Finally, general robot tasks in a graph are considered. A combinatorial topology characterization for the solvable tasks is presented, by a reduction of the asynchronous fault-tolerant LOOK-COMPUTE-MOVE model to a wait-free read/write shared-memory computing model, bringing together two areas that have been independently studied for a long time into a common theoretical foundation.

Adaptive renaming can be viewed as a coordination task involving a set of asynchronous agents, each aiming at grabbing a single resource out of a set of resources totally ordered by their desirability. We consider a generalization of adaptive renaming to take into account scenarios in which resources are not independent.

The set consensus problem has played an important role in the study of distributed systems for over two decades. Indeed, the search for lower bounds and impossibility results for this problem spawned the topological approach to distributed computing, which has given rise to new techniques in the design and analysis of protocols. The design of efficient solutions to set consensus has also proven to be challenging. In the synchronous crash failure model, the literature contains a sequence of solutions to set consensus, each improving upon the previous ones. This paper presents an unbeatable protocol for nonuniform k-set consensus in the synchronous crash failure model. This is an efficient protocol whose decision times cannot be improved upon. Moreover, the description of our protocol is extremely succinct. Proving unbeatability of this protocol is a nontrivial challenge. We provide two proofs for its unbeatability: one is a subtle constructive combinatorial proof, and the other is a topological proof of a new style. These two proofs provide new insight into the connection between topological reasoning and combinatorial reasoning about protocols, which has long been a subject of interest. In particular, our topological proof reasons in a novel way about subcomplexes of the protocol complex, and sheds light on an open question posed by Guerraoui and Pochon (2009). Finally, using the machinery developed in the design of this unbeatable protocol, we propose a protocol for uniform k-set consensus that beats all known solutions by a large margin.

Processes in a concurrent system need to coordinate using an underlying shared memory or a message-passing system in order to solve agreement tasks such as, for example, consensus or set agreement. However, coordination is often needed to break the symmetry of processes that are initially in the same state---for example, to get exclusive access to a shared resource, to get distinct names, or to elect a leader. This paper introduces and studies the family of generalized symmetry breaking (GSB) tasks, which includes election, renaming, and many other symmetry breaking tasks, and studies how nondeterminism properties of objects solving tasks affects the computability power of GSB tasks. The aim is to develop the understanding of symmetry breaking tasks and their relation with agreement tasks and to study nondeterminism properties of objects solving tasks and how these properties affect the computability power of symmetry breaking tasks. Among various results characterizing the family of GSB tasks, it is shown that perfect renaming, i.e., $(n,n)$-renaming, is universal for all GSB tasks. The paper also shows that there is a large family of GSB tasks, which includes perfect renaming, that is strictly more powerful than $(n,n-1)$-set agreement. Some of these tasks are equivalent to perfect renaming, while others lie strictly between perfect renaming and $(n,n+1)$-renaming. Results comparing renaming and set agreement are proved, and the results in this paper complement known results. This paper sheds new light on the relations linking set agreement and symmetry breaking. The proofs are based on combinatorial topology techniques and new ideas about different notions of nondeterminism that can be associated with shared objects.

A well-known generalization of the consensus problem, namely, set agreement (SA), limits the number of distinct decision values that processes decide. In some settings, it may be more important to limit the number of "disagreers". Thus, we introduce another natural generalization of the consensus problem, namely, bounded disagreement (BD), which limits the number of processes that decide differently from the plurality. More precisely, in a system with n processes, the (n, l)-BD task has the following requirement: there is a value v such that at most l processes (the disagreers) decide a value other than v. Despite their apparent similarities, the results described below show that bounded disagreement, consensus, and set agreement are in fact fundamentally different problems. We investigate the relationship between bounded disagreement, consensus, and set agreement. In particular, we determine the consensus number for every instance of the BD task. We also determine values of n, l, m, and k such that the (n, l)-BD task can solve the (m, k)-SA task (where m processes can decide at most k distinct values). Using our results and a previously known impossibility result for set agreement, we prove that for all n >= 2, there is a BD task (and a corresponding BD object) that has consensus number n but can not be solved using n-consensus and registers. Prior to our paper, the only objects known to have this unusual characteristic for n >= 2 (which shows that the consensus number of an object is not sufficient to fully capture its power) were artificial objects crafted solely for the purpose of exhibiting this behaviour.

This paper is on the relative power and the relations linking two important synchronization problems in n-process wait-free shared memory models, namely, set agreement and renaming, which are two of the most studied subconsensus tasks. Since the 2006 seminal paper of Gafni, Rajsbaum and Herlihy, it is known that some renaming instances are strictly weaker than set agreement. Indeed, it was later on shown that not even (n + 1)-renaming (the strongest task in the renaming family, after perfect n-renaming) can implement (n - 1)-set agreement (the weakest non-trivial task in the set agreement family). These and other results seem to imply that renaming and, more generally, the tasks called generalized symmetry breaking tasks (GSB) are weaker than agreement tasks. This paper shows that this is not the case, namely, it shows that there is a large family of GSB tasks that are more powerful than (n - 1)-set agreement. Some of these tasks are equivalent to n-renaming, while others lie strictly between n-renaming and (n+1)-renaming. Moreover, none of these GSB tasks can solve (n - 2)-set agreement. Hence, these subconsensus tasks have a rich structure and are interesting in their own. The proofs of these results are based on algebraic topology techniques and new ideas about different notions of nondeterminism that can be associated with shared objects. Interestingly, this paper sheds a new light on the relations linking set agreement and renaming.

The M-renaming task requires n+1 processes, each starting with a unique input name (from an arbitrary large range), to coordinate the choice of new output names from a range of size M. This paper presents the first upper bound on the complexity of hard renaming, i.e., 2n-renaming, when n+1 is not a prime power. It is known that 2n-renaming can be solved if and only if n+1 is not a prime power; however, the previous proof of the "if" part was non-constructive, involving an approximation theorem; in particular, it did not yield a concrete upper bound on the complexity of the resulting protocol.

A protocol P is Pareto-optimal if no protocol Q can decide as fast as P for all adversaries, while allowing at least one process to decide strictly earlier, in at least one instance. Pareto optimal protocols cannot be improved upon. We present the first Pareto-optimal solutions to consensus and k-set consensus for synchronous message-passing with crashes failures. Our k-set consensus protocol strictly dominates all known solutions, and our results expose errors in [1, 7, 8, 12]. Our proofs of Pareto optimality are completely constructive, and are devoid of any topological arguments or reductions.

In the asynchronous wait-free shared memory model, two families of tasks play a central role because of their implications in theory and in practice: k-set agreement and M-renaming. Let n denote the number of processes in the system. Previous research shows that (n-1)-set agreement can solve (2n-2)-renaming, for any value of n, while (2n-2)-renaming cannot solve (n-1)-set agreement, when n is odd. It is also known that, for every n ≥ 3, n-renaming, also called perfect renaming, is strictly stronger than (n-1)-set agreement. This paper shows that when n ≥ 4, there is a family of tasks that are strictly stronger than (n-1)-set agreement and strictly weaker than perfect renaming. This enlarges our view of both the nature and the structure of what are distributed computing tasks.

In the renaming task, n +1 processes start with unique input names from a large space and must choose unique output names taken from a smaller name space, 0,1,…, K . To rule out trivial solutions, a protocol must be anonymous : the value chosen by a process can depend on its input name and on the execution, but not on the specific process ID. Attiya et al. [1990] showed that renaming has a wait-free solution when K ≥ 2 n . Several algebraic topology proofs of a lower bound stating that no such protocol exists when K < 2 n have been published. In a companion article, we present the first completely combinatorial renaming lower bound proof stating if n + 1 is a primer power, then renaming is not wait-free solvable when K < 2 n . In this article, we show that if n + 1 is not a primer power, then there exists a wait-free renaming protocol for K = 2 n −1. Therefore the renaming lower bound for K < 2 n is incorrect. More precisely, our main theorem states that there exists a wait-free renaming protocol for K < 2 n if and only if n + 1 is not a prime power. We prove this result using the known equivalence of K -renaming for K = 2 n − 1 and the weak symmetry breaking task: processes have no input values and the output values are 0 or 1, and it is required that in every execution in which all processes participate, at least one process decides 1 and at least one process decides 0.

In the renaming task n+1 processes start with unique input names from a large space and must choose unique output names taken from a smaller name space, namely 0,1,...,K. To rule out trivial solutions, a protocol must be anonymous: the value chosen by a process can depend on its input name and on the execution, but not on the specific process id. Attiya et al. showed in 1990 that renaming has a wait-free solution when K<=2n. Several proofs of a lower bound stating that no such protocol exists when K<2n have been published. In this paper we prove that, for certain values of n, this lower bound is incorrect, exhibiting a wait-free renaming protocol for K=2n-1. For the other values of n, we present the first completely combinatorial lower bound proof stating that no such protocol exists when K<2n. More precisely, our main theorem states that there exists a wait-free renaming protocol for K<2n if and only if the set of integers (n+1 choose i+1) | 0 <= i <= floor((n-1)/2)} are relatively prime. Thus, such protocol exists for six processes, and not for less. The proof of the theorem uses combinatorial topology techniques, both for the lower bound and to derive the renaming protocol.