Search

Runtime verification is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors observing the system, only if each monitor can emit verdicts taken from a large enough finite set. We revisit this impossibility result in the concrete context of linear-time logic (LTL) semantics for runtime verification, that is, when the correctness of the system is specified by an LTL formula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics of LTL (rv-LTL) may result in inconsistent distributed monitoring, even for some simple LTL formulas. More generally, given any LTL formula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called its alternation number. Specifically, we show that, for every k ≥ 0, there is an LTL formula φ with alternation number k that cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller than k + 1. On the positive side, we define a family of logics, called distributed LTL (abbreviated as dLTL), parameterized by k ≥ 0, which refines RV-LTL by incorporating 2k + 4 truth values. Our main contribution is to show that, for every k ≥ 0, every LTL formula φ with alternation number k can be consistently monitored by distributed monitors, each running an automaton based on a (2⌈k/2⌉ + 4)-valued logic taken from the dltl family. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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 = 2n. Several algebraic topology proofs of a lower bound stating that no such protocol exists when K ≥ 2n 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 ≥ 2n. In this article, we show that if n + 1 is not a primer power, then there exists a wait-free renaming protocol for K = 2n - 1. Therefore the renaming lower bound for K ≥ 2n is incorrect. More precisely, our main theorem states that there exists a wait-free renaming protocol for K ≥ 2n if and only if n + 1 is not a prime power. We prove this result using the known equivalence of K-renaming for K = 2n - 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. Categories and Subject Descriptors: D.1.3 [Programming Techniques]: Concurrent Programming; F.1.1 [Computation by Abstract Devices]: Models of Computation -- computability theory; F.1.2 [Computation by Abstract Devices]: Modes of Computation -- parallelism and concurrency General Terms: Algorithms, Theory [ABSTRACT FROM AUTHOR]

We consider a failure-free, asynchronous message passing network with n links, where the processors are arranged on a ring or a chain. The processors are identically programmed but have distinct identities, taken from {0, 1,…, M -1}. We investigate the communication costs of three well studied tasks: Consensus, Leader, and MaxF (finding the maximum identity). We show that in chain and ring topologies, the message complexities of all three tasks are the same. Hence, we study a finer measure of complexity: the number of transmitted bits required to solve a task T, denoted BitC(T ). We prove several new lower bounds (and some simple upper bounds) that imply the following results: For the two processors case, BitC(Consensus) = 2 and BitC(Leader) = BitC(MaxF) = 2 log2 M ± O(1), where the gap between the lower and upper bounds is almost always 1. For a chain, BitC(Consensus) = ϴ(n), BitC(Leader) = ϴ(n + log M), and BitC(MaxF) = ϴ(n log M). For the ring topology, we prove the lower bound of Ω(n log M) for Leader, and (hence) MaxF. We consider also a chain where the intermediate processors have no identities. We prove that BitC(Leader) = ϴ(n log M), which is equal to n times the bit complexity of the problem for two processors. For the specific case when the chain length is even, we prove that BitC(Leader) = ϴ(n), for both above settings. In addition, we show that for any algorithm solving MaxF, there exists an input, for which every execution has the bit complexity Ω(n log M) (this is not the case for Leader). In our proofs, we use both methods of distributed computing and of communication complexity theory, establishing new links between the two areas. [ABSTRACT FROM AUTHOR]

This article introduces and explores the condition-based approach to solve the consensus problem in asynchronous systems. The approach studies conditions that identify sets of input vectors for which it is possible to solve consensus despite the occurrence of up to f process crashes. The first main result defines acceptable conditions and shows that these are exactly the conditions for which a consensus protocol exists. Two examples of realistic acceptable conditions are presented, and proved to be maximal, in the sense mat they cannot be extended and remain acceptable. The second main result is a generic consensus shared-memory protocol for any acceptable condition. The protocol always guarantees agreement and validity, and terminates (at least) when the inputs satisfy the condition with which the protocol has been instantiated, or when there are no crashes. An efficient version of the protocol is then designed for the message passing model that works when f < n/2, and it is shown that no such protocol exists when f ≥ n/2. It is also shown how the protocol's safety can be traded for its liveness. [ABSTRACT FROM AUTHOR]