We describe the input/output automaton model, a model for concurrent and distributed discrete event systems. We define the model, illustrate the model with several examples concerning vending machines and a leader election algorithm, and survey the ways in which the model has been used. 1 , 2

Emulating a shared atomic , read/write storage system is a fundamental problem in distributed computing. Replicating atomic objects among a set of data hosts was the norm for traditional implementations (e.g., [ 11 ]) in order to guarantee the availability and accessibility of the data despite host failures. As replication is highly storage demanding, recent approaches suggested the use of erasure-codes to offer the same fault-tolerance while optimizing storage usage at the hosts. Initial works focused on a fixed set of data hosts. To guarantee longevity and scalability, a storage service should be able to dynamically mask hosts failures by allowing new hosts to join, and failed host to be removed without service interruptions. This work presents the first erasure-code -based atomic algorithm, called Ares , which allows the set of hosts to be modified in the course of an execution. Ares is composed of three main components: (i) a reconfiguration protocol , (ii) a read/write protocol , and (iii) a set of data access primitives (DAPs) . The design of Ares is modular and is such to accommodate the usage of various erasure-code parameters on a per-configuration basis. We provide bounds on the latency of read/write operations and analyze the storage and communication costs of the Ares algorithm.

READ transactions that read data distributed across servers dominate the workloads of real-world distributed storage systems. The SNOW Theorem [13] stated that ideal READ transactions that have optimal latency and the strongest guarantees-i.e., “SNOW” READ transactions-are impossible in one specific setting that requires three or more clients: at least two readers and one writer. However, it left many open questions. We close all of these open questions with new impossibility results and new algorithms. First, we prove rigorously the result from [13] saying that it is impossible to have a READ transactions system that satisfies SNOW properties with three or more clients. The insight we gained from this proof led to teasing out the implicit assumptions that are required to state the results and also, resolving the open question regarding the possibility of SNOW with two clients. We show that it is possible to design an algorithm, where SNOW is possible in a multi-writer, single-reader (MWSR) setting when a client can send messages to other clients; on the other hand, we prove it is impossible to implement SNOW in a multi-writer, single-reader (MWSR) setting-which is more general than the two-client setting-when client-to-client communication is disallowed. We also correct the previous claim in [13] that incorrectly identified one existing system, Eiger [12], as supporting the strongest guarantees (SW) and whose read-only transactions had bounded latency. Thus, there were no previous algorithms that provided the strongest guarantees and had bounded latency. Finally, we introduce the first two algorithms to provide the strongest guarantees with bounded latency.

We study input compression in a biologically inspired model of neural computation. We demonstrate that a network consisting of a random projection step (implemented via random synaptic connectivity) followed by a sparsification step (implemented via winner-take-all competition) can reduce well-separated high-dimensional input vectors to well-separated low-dimensional vectors. By augmenting our network with a third module, we can efficiently map each input (along with any small perturbations of the input) to a unique representative neuron, solving a neural clustering problem. Both the size of our network and its processing time, i.e., the time it takes the network to compute the compressed output given a presented input, are independent of the (potentially large) dimension of the input patterns and depend only on the number of distinct inputs that the network must encode and the pairwise relative Hamming distance between these inputs. The first two steps of our construction mirror known biological networks, for example, in the fruit fly olfactory system [Caron et al., 2013; Lin et al., 2014; Dasgupta et al., 2017]. Our analysis helps provide a theoretical understanding of these networks and lay a foundation for how random compression and input memorization may be implemented in biological neural networks. Technically, a contribution in our network design is the implementation of a short-term memory. Our network can be given a desired memory time t_m as an input parameter and satisfies the following with high probability: any pattern presented several times within a time window of t_m rounds will be mapped to a single representative output neuron. However, a pattern not presented for c⋅t_m rounds for some constant c>1 will be "forgotten", and its representative output neuron will be released, to accommodate newly introduced patterns.

We study the problem of distributed task allocation by workers in an ant colony in a setting of limited capabilities and noisy environment feedback. We assume that each task has a demand that should be satisfied but not exceeded, i.e., there is an optimal number of ants that should be working on this task at a given time. The goal is to assign a near-optimal number of workers to each task in a distributed manner without explicit access to the value of the demand nor to the number of ants working on the task.

In this paper, we study local and global broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local and global broadcast in the dual graph model. We also precisely characterize how this efficiency degrades as the new constraints are reduced down to non-existent, and prove new lower bounds that establish this degradation as near optimal for a large class of natural algorithms. We conclude with an analysis of a more general model where we propose an enhanced back-off algorithm. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.

Emulating a shared atomic, read/write storage system is a fundamental problem in distributed computing. Replicating atomic objects among a set of data hosts was the norm for traditional implementations (e.g., [6]) in order to guarantee the availability and accessibility of the data despite host failures. As replication is highly storage demanding, recent approaches suggested the use of erasure-codes to offer the same fault-tolerance while optimizing storage usage at the hosts. Initial works focused on a fix set of data hosts. To guarantee longevity and scalability, a storage service should be able to dynamically mask hosts failures by allowing new hosts to join, and failed host to be removed without service interruptions. This work presents the first erasure-code based atomic algorithm, called ARES, which allows the set of hosts to be modified in the course of an execution. ARES is composed of three main components: (i) a reconfiguration protocol, (ii) a read/write protocol, and (iii) a set of data access primitives. The design of ARES is modular and is such to accommodate the usage of various erasure-code parameters on a per-configuration basis. We provide bounds on the latency of read/write operations and analyze the storage and communication costs of the ARES algorithm.

In this work, we propose FLECKS, an algorithm which implements atomic memory objects in a multi-writer multi-reader (MWMR) setting in asynchronous networks and server failures. FLECKS substantially reduces storage and communication costs over its replication-based counterparts by employing erasure-codes. FLECKS outperforms the previously proposed algorithms in terms of the metrics that to deliver good performance such as storage cost per object, communication cost a high fault-tolerance of clients and servers, guaranteed liveness of operation, and a given number of communication rounds per operation, etc. We provide proofs for liveness and atomicity properties of FLECKS and derive worst-case latency bounds for the operations. We implemented and deployed FLECKS in cloud-based clusters and demonstrate that FLECKS has substantially lower storage and bandwidth costs, and significantly lower latency of operations than the replication-based mechanisms.

The winner of the 2019 Principles of Distributed Computing Doctoral Dissertation Award is Dr. Sepehr Assadi for his dissertation Combinatorial Optimization on Massive Datasets: Streaming, Distributed, and Massively Parallel Computation, written under the supervision of Prof. Sanjeev Khanna at the University of Pennsylvania.

In this paper, we consider networks of deterministic spiking neurons, firing synchronously at discrete times. We consider the problem of translating temporal information into spatial information in such networks, an important task that is carried out by actual brains. Specifically, we define two problems: "First Consecutive Spikes Counting" and "Total Spikes Counting", which model temporal-coding and rate-coding aspects of temporal-to-spatial translation respectively. Assuming an upper bound of T on the length of the temporal input signal, we design two networks that solve two problems, each using O(log T) neurons and terminating in time T+1. We also prove that these bounds are tight.

Winner-take-all (WTA) refers to the neural operation that selects a (typically small) group of neurons from a large neuron pool. It is conjectured to underlie many of the brain's fundamental computational abilities. However, not much is known about the robustness of a spike-based WTA network to the inherent randomness of the input spike trains. In this work, we consider a spike-based [Formula: see text]–WTA model wherein [Formula: see text] randomly generated input spike trains compete with each other based on their underlying firing rates and [Formula: see text] winners are supposed to be selected. We slot the time evenly with each time slot of length 1 ms and model the [Formula: see text] input spike trains as [Formula: see text] independent Bernoulli processes. We analytically characterize the minimum waiting time needed so that a target minimax decision accuracy (success probability) can be reached. We first derive an information-theoretic lower bound on the waiting time. We show that to guarantee a (minimax) decision error [Formula: see text] (where [Formula: see text]), the waiting time of any WTA circuit is at least [Formula: see text]where [Formula: see text] is a finite set of rates and [Formula: see text] is a difficulty parameter of a WTA task with respect to set [Formula: see text] for independent input spike trains. Additionally, [Formula: see text] is independent of [Formula: see text], [Formula: see text], and [Formula: see text]. We then design a simple WTA circuit whose waiting time is [Formula: see text]provided that the local memory of each output neuron is sufficiently long. It turns out that for any fixed [Formula: see text], this decision time is order-optimal (i.e., it matches the above lower bound up to a multiplicative constant factor) in terms of its scaling in [Formula: see text], [Formula: see text], and [Formula: see text].

In this paper, we study local broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local broadcast in the dual graph model. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.

We initiate a line of investigation into biological neural networks from an algorithmic perspective. We develop a simplified but biologically plausible model for distributed computation in stochastic spiking neural networks and study tradeoffs between computation time and network complexity in this model. Our aim is to abstract real neural networks in a way that, while not capturing all interesting features, preserves high-level behavior and allows us to make biologically relevant conclusions. In this paper, we focus on the important 'winner-take-all' (WTA) problem, which is analogous to a neural leader election unit: a network consisting of $n$ input neurons and n corresponding output neurons must converge to a state in which a single output corresponding to a firing input (the 'winner') fires, while all other outputs remain silent. Neural circuits for WTA rely on inhibitory neurons, which suppress the activity of competing outputs and drive the network towards a converged state with a single firing winner. We attempt to understand how the number of inhibitors used affects network convergence time. We show that it is possible to significantly outperform naive WTA constructions through a more refined use of inhibition, solving the problem in O(\theta) rounds in expectation with just O(\log^{1/\theta} n) inhibitors for any \theta. An alternative construction gives convergence in O(\log^{1/\theta} n) rounds with O(\theta) inhibitors. We complement these upper bounds with our main technical contribution, a nearly matching lower bound for networks using \ge \log \log n inhibitors. Our lower bound uses familiar indistinguishability and locality arguments from distributed computing theory applied to the neural setting. It lets us derive a number of interesting conclusions about the structure of any network solving WTA with good probability, and the use of randomness and inhibition within such a network.

Motivated by emerging applications to the edge computing paradigm, we introduce a two-layer erasure-coded fault-tolerant distributed storage system offering atomic access for read and write operations. In edge computing, clients interact with an edge-layer of servers that is geographically near; the edge-layer in turn interacts with a back-end layer of servers. The edge-layer provides low latency access and temporary storage for client operations, and uses the back-end layer for persistent storage. Our algorithm, termed Layered Data Storage (LDS) algorithm, offers several features suitable for edge-computing systems, works under asynchronous message-passing environments, supports multiple readers and writers, and can tolerate f1 < n1/2 and f2 < n2/3 crash failures in the two layers having n1 and n2 servers, respectively. We use a class of erasure codes known as regenerating codes for storage of data in the back-end layer. The choice of regenerating codes, instead of popular choices like Reed-Solomon codes, not only optimizes the cost of back-end storage, but also helps in optimizing communication cost of read operations, when the value needs to be recreated all the way from the back-end. The two-layer architecture permits a modular implementation of atomicity and erasure-code protocols; the implementation of erasure-codes is mostly limited to interaction between the two layers. We prove liveness and atomicity of LDS, and also compute performance costs associated with read and write operations. In a system with n1 = Θ(n2), f1 = Θ(n1), f2 = Θ(n2), the write and read costs are respectively given by Θ(n1) and Θ(1) + n1 I(δ > 0). Here δ is a parameter closely related to the number of write operations that are concurrent with the read operation, and I(δ > 0) is 1 if δ > 0, and 0 if δ = 0. The cost of persistent storage in the back-end layer is Θ(1). The impact of temporary storage is minimally felt in a multi-object system running N independent instances of LDS, where only a small fraction of the objects undergo concurrent accesses at any point during the execution. For the multi-object system, we identify a condition on the rate of concurrent writes in the system such that the overall storage cost is dominated by that of persistent storage in the back-end layer, and is given by Θ(N).

In this paper we study the problem of developing efficient distributed algorithms for dense wireless networks. For many problems in this setting, fast solutions must leverage the reality that radio signals fade with distance, which can be exploited to enable concurrent communication among multiple sender/receiver pairs. To simplify the development of these algorithms we describe a new communication abstraction called FadingMAC which exposes the benefits of this concurrent communication, but also hides the details of the underlying low-level radio signal behavior. This approach splits efforts between those who develop useful algorithms that run on the abstraction, and those who implement the abstraction in concrete low-level wireless models, or on real hardware. After defining FadingMAC, we describe and analyze an efficient implementation of the abstraction in a standard low-level SINR-style network model. We then describe solutions to the following problems that run on the abstraction: max, min, sum, and mean computed over input values; process renaming; consensus and leader election; and optimal packet scheduling. Combining our abstraction implementation with these applications that run on the abstraction, we obtain near-optimal solutions to these problems in our low-level SINR model - significantly advancing the known results for distributed algorithms in this setting. Of equal importance to these concrete bounds, however, is the general idea advanced by this paper: as wireless networks become more dense, both theoreticians and practitioners must explore new communication abstractions that can help tame this density.

We study distributed algorithms implemented in a simplified biologically inspired model for stochastic spiking neural networks. We focus on tradeoffs between computation time and network complexity, along with the role of randomness in efficient neural computation. It is widely accepted that neural computation is inherently stochastic. In recent work, we explored how this stochasticity could be leveraged to solve the `winner-take-all' leader election task. Here, we focus on using randomness in neural algorithms for similarity testing and compression. In the most basic setting, given two $n$-length patterns of firing neurons, we wish to distinguish if the patterns are equal or $ε$-far from equal. Randomization allows us to solve this task with a very compact network, using $O \left (\frac{\sqrt{n}\log n}ε\right)$ auxiliary neurons, which is sublinear in the input size. At the heart of our solution is the design of a $t$-round neural random access memory, or indexing network, which we call a neuro-RAM. This module can be implemented with $O(n/t)$ auxiliary neurons and is useful in many applications beyond similarity testing. Using a VC dimension-based argument, we show that the tradeoff between runtime and network size in our neuro-RAM is nearly optimal. Our result has several implications -- since our neuro-RAM can be implemented with deterministic threshold gates, it shows that, in contrast to similarity testing, randomness does not provide significant computational advantages for this problem. It also establishes a separation between feedforward networks whose gates spike with sigmoidal probability functions, and well-studied deterministic sigmoidal networks, whose gates output real number sigmoidal values, and which can implement a neuro-RAM much more efficiently.

Adaptive collective systems are common in biology and beyond. Typically, such systems require a task allocation algorithm: a mechanism or rule-set by which individuals select particular roles. Here we study the performance of such task allocation mechanisms measured in terms of the time for individuals to allocate to tasks. We ask: (1) Is task allocation fundamentally difficult, and thus costly? (2) Does the performance of task allocation mechanisms depend on the number of individuals? And (3) what other parameters may affect their efficiency? We use techniques from distributed computing theory to develop a model of a social insect colony, where workers have to be allocated to a set of tasks; however, our model is generalizable to other systems. We show, first, that the ability of workers to quickly assess demand for work in tasks they are not currently engaged in crucially affects whether task allocation is quickly achieved or not. This indicates that in social insect tasks such as thermoregulation, where temperature may provide a global and near instantaneous stimulus to measure the need for cooling, for example, it should be easy to match the number of workers to the need for work. In other tasks, such as nest repair, it may be impossible for workers not directly at the work site to know that this task needs more workers. We argue that this affects whether task allocation mechanisms are under strong selection. Second, we show that colony size does not affect task allocation performance under our assumptions. This implies that when effects of colony size are found, they are not inherent in the process of task allocation itself, but due to processes not modeled here, such as higher variation in task demand for smaller colonies, benefits of specialized workers, or constant overhead costs. Third, we show that the ratio of the number of available workers to the workload crucially affects performance. Thus, workers in excess of those needed to complete all tasks improve task allocation performance. This provides a potential explanation for the phenomenon that social insect colonies commonly contain inactive workers: these may be a 'surplus' set of workers that improves colony function by speeding up optimal allocation of workers to tasks. Overall our study shows how limitations at the individual level can affect group level outcomes, and suggests new hypotheses that can be explored empirically.

Erasure codes are increasingly being studied in the context of implementing atomic memory objects in large scale asynchronous distributed storage systems. When compared with the traditional replication based schemes, erasure codes have the potential of significantly lowering storage and communication costs while simultaneously guaranteeing the desired resiliency levels. In this work, we propose the Storage-Optimized Data-Atomic (SODA) algorithm for implementing atomic memory objects in the multi-writer multi-reader setting. SODA uses Maximum Distance Separable (MDS) codes, and is specifically designed to optimize the total storage cost for a given fault-tolerance requirement. For tolerating f server crashes in an n-server system, SODA uses an [n, k] MDS code with k = n - f, and incurs a total storage cost of n/n-f. SODA is designed under the assumption of reliable point-to-point communication channels. The communication cost of a write and a read operation are respectively given by O(f2) and n/n-f(δw+1), where δwdenotes the number of writes that are concurrent with the particular read. In comparison with the recent CASGC algorithm [1], which also uses MDS codes, SODA offers lower storage cost while pays more on the communication cost. We also present a modification of SODA, called SODAerr, to handle the case where some of the servers can return erroneous coded elements during a read operation. Specifically, in order to tolerate f server failures and e error-prone coded elements, the SODAerr algorithm uses an [n, k] MDS code such that k = n - 2e - f. SODAerr also guarantees liveness and atomicity, while maintaining an optimized total storage cost of n/n-f-2e.

Erasure codes offer an efficient way to decrease storage and communication costs while implementing atomic memory service in asynchronous distributed storage systems. In this paper, we provide erasure-code-based algorithms having the additional ability to perform background repair of crashed nodes. A repair operation of a node in the crashed state is triggered externally, and is carried out by the concerned node via message exchanges with other active nodes in the system. Upon completion of repair, the node re-enters active state, and resumes participation in ongoing and future read, write, and repair operations. To guarantee liveness and atomicity simultaneously, existing works assume either the presence of nodes with stable storage, or presence of nodes that never crash during the execution. We demand neither of these; instead we consider a natural, yet practical network stability condition N1 that only restricts the number of nodes in the crashed/repair state during broadcast of any message. We present an erasure-code based algorithm RADON_{C} that is always live, and guarantees atomicity as long as condition N1 holds. In situations when the number of concurrent writes is limited, RADON_{C} has significantly improved storage and communication cost over a replication-based algorithm RADON_{R}, which also works under N1. We further show how a slightly stronger network stability condition N2 can be used to construct algorithms that never violate atomicity. The guarantee of atomicity comes at the expense of having an additional phase during the read and write operations.

The focus of this paper is to understand storage costs of emulating an atomic shared memory over an asynchronous, distributed message passing system. Previous literature has developed several shared memory emulation algorithms based on replication and erasure coding techniques, and analyzed the storage costs of the proposed algorithms. In this paper, we present the first known information-theoretic lower bounds on the storage costs incurred by shared memory emulation algorithms. Our storage cost lower bounds are universally applicable, that is, we make no assumption on the structure of the algorithm or the method of encoding the data.

We introduce the study of the ant colony house-hunting problem from a distributed computing perspective. When an ant colony's nest becomes unsuitable due to size constraints or damage, the colony relocates to a new nest. The task of identifying and evaluating the quality of potential new nests is distributed among all ants. They must additionally reach consensus on a final nest choice and transport the full colony to this single new nest. Our goal is to use tools and techniques from distributed computing theory in order to gain insight into the house-hunting process. We develop a formal model for the house-hunting problem inspired by the behavior of the Temnothorax genus of ants. We then show a Omega(log n) lower bound on the time for all n ants to agree on one of k candidate nests. We also present two algorithms that solve the house-hunting problem in our model. The first algorithm solves the problem in optimal O(log n) time but exhibits some features not characteristic of natural ant behavior. The second algorithm runs in O(k log n) time and uses an extremely simple and natural rule for each ant to decide on the new nest.

We present the first algorithm that implements an abstract MAC (absMAC) layer in the Signal-to-Interference-plus-Noise-Ratio (SINR) wireless network model. We first prove that efficient SINR implementations are not possible for the standard absMAC specification. We modify that specification to an "approximate" version that better suits the SINR model. We give an efficient algorithm to implement the modified specification, and use it to derive efficient algorithms for higher-level problems of global broadcast and consensus.

In this paper, we implement an efficient local broadcast service for the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Our local broadcast service offers probabilistic latency guarantees for: (1) message delivery to all reliable neighbors (i.e., neighbors connected by reliable links), and (2) receiving some message when one or more reliable neighbors are broadcasting. This service significantly simplifies the design and analysis of algorithms for the otherwise challenging dual graph model. To this end, we also note that our solution can be interpreted as an implementation of the abstract MAC layer specification---therefore translating the growing corpus of algorithmic results studied on top of this layer to the dual graph model. At the core of our service is a seed agreement routine which enables nodes in the network to achieve "good enough" coordination to overcome the difficulties of unpredictable link behavior. Because this routine has potential application to other problems in this setting, we capture it with a formal specification---simplifying its reuse in other algorithms. Finally, we note that in a break from much work on distributed radio network algorithms, our problem definitions (including error bounds), implementation, and analysis do not depend on global network parameters such as the network size, a goal which required new analysis techniques. We argue that breaking the dependence of these algorithms on global parameters makes more sense and aligns better with the rise of ubiquitous computing, where devices will be increasingly working locally in an otherwise massive network. Our push for locality, in other words, is a contribution independent of the specific radio network model and problem studied here.

This paper considers the communication and storage costs of emulating atomic (linearizable) multi-writer multi-reader shared memory in distributed message-passing systems. The paper contains two main contributions: 1) We present an atomic shared-memory emulation algorithm that we call Coded Atomic Storage (CAS). This algorithm uses erasure coding methods. In a storage system with 'N' servers that is resilient to 'f' server failures, we show that the communication cost of CAS is N/(N-2f). The storage cost of CAS is unbounded. 2) We present a variant of CAS known as CAS with Garbage Collection (CASGC). The CASGC algorithm is parametrized by an integer 'd' and has a bounded storage cost. We show that in every execution where the number of write operations that are concurrent with a read operation is no bigger than d, the CASGC algorithm with parameter d satisfies atomicity and liveness. We explicitly characterize the storage cost of CASGC, and show that it has the same communication cost as CAS.

We study the multi-message broadcast problem using abstract MAC layer models of wireless networks. These models capture the key guarantees of existing MAC layers while abstracting away low-level details such as signal propagation and contention.We begin by studying upper and lower bounds for this problem in a standard abstract MAC layer model---identifying an interesting dependence between the structure of unreliable links and achievable time complexity. In more detail, given a restriction that devices connected directly by an unreliable link are not too far from each other in the reliable link topology, we can (almost) match the efficiency of the reliable case. For the related restriction, however, that two devices connected by an unreliable link are not too far from each other in geographic distance, we prove a new lower bound that shows that this efficiency is impossible. We then investigate how much extra power must be added to the model to enable a new order of magnitude of efficiency. In more detail, we consider an enhanced abstract MAC layer model and present a new multi-message broadcast algorithm that (under certain natural assumptions) solves the problem in this model faster than any known solutions in an abstract MAC layer setting.

We argue that in the context of biology-inspired problems in computer science, in addition to studying the time complexity of solutions it is also important to study the selection complexity, a measure of how likely a given algorithmic strategy is to arise in nature. In this spirit, we propose a selection complexity metric χ for the ANTS problem [Feinerman et al.]. For algorithm A, we define χ(A) = b + log l, where b is the number of memory bits used by each agent and l bounds the fineness of available probabilities (agents use probabilities of at least 1/2l). We consider n agents searching for a target in the plane, within an (unknown) distance D from the origin. We identify log log D as a crucial threshold for our selection complexity metric. We prove a new upper bound that achieves near-optimal speed-up of (D2/n +D) ⋅ 2O(l) for χ(A) ≤ 3 log log D + O(1), which is asymptotically optimal if l∈ O(1). By comparison, previous algorithms achieving similar speed-up require χ(A) = Ω(log D). We show that this threshold is tight by proving that if χ(A) < log log D - ω(1), then with high probability the target is not found if each agent performs D2-o(1) moves. This constitutes a sizable gap to the straightforward Ω(D2/n + D) lower bound.

In much of the theoretical literature on global broadcast algorithms for wireless networks, issues of message dissemination are considered together with issues of contention management. This combination leads to complicated algorithms and analysis, and makes it difficult to extend the work to more difficult communication problems. In this paper, we present results aimed at simplifying such algorithms and analysis by decomposing the treatment into two levels, using abstract “MAC layer” specifications to encapsulate contention management. We use two different abstract MAC layers: the basic layer of [1], [2] and a new probabilistic layer. We first present a typical randomized contention-management algorithm for a standard graph-based radio network model and show that it implements both abstract MAC layers. Then we combine this algorithm with greedy algorithms for single-message and multi-message global broadcast and analyze the combinations, using both abstract MAC layers as intermediate layers. Using the basic MAC layer, we prove a bound of ODlogn∊log(Δ) for the time to deliver a single message everywhere with probability 1 − ∊, where D is the network diameter, n is the number of nodes, and Δ is the maximum node degree. Using the probabilistic layer, we prove a bound of OD+logn∊log(Δ), which matches the best previously-known bound for single-message broadcast over the physical network model. For multi-message broadcast, we obtain bounds of O(D+kΔ)logn∊log(Δ) using the basic layer and OD+kΔlogn∊log(Δ) using the probabilistic layer, for the time to deliver a message everywhere in the presence of at most k concurrent messages.

Summary form only given. The Timed I/O Automata (TIOA) modeling framework has been used for describing and analyzing many distributed algorithms, ranging from data-management algorithms to clock-synchronization algorithms to robot-coordination algorithms. These algorithms include timing aspects, and both discrete and continuous behavior. In this talk, I will describe the TIOA framework in some detail, and summarize many of the examples to which it has been applied. Then, I will discuss the extensions that are needed to enable it to handle more kinds of algorithms. These extensions will mainly involve adding and integrating features for handling probabilistic choices. I will review the state of the art for Probabilistic Timed I/O Automata models, and describe the work that I think is still needed.

We study upper and lower bounds for the global and local broadcast problems in the dual graph model combined with different strength adversaries. The dual graph model is a generalization of the standard graph-based radio network model that includes unreliable links controlled by an adversary. It is motivated by the ubiquity of unreliable links in real wireless networks. Existing results in this model [11, 12, 3, 8] assume an offline adaptive adversary - the strongest type of adversary considered in standard randomized analysis. In this paper, we study the two other standard types of adversaries: online adaptive and oblivious. Our goal is to find a model that captures the unpredictable behavior of real networks while still allowing for efficient broadcast solutions.

Modern distributed computer systems are based on platforms that change dynamically. Many of these platforms utilize wireless communication, and many involve mobile nodes. These systems must handle complications like changing sets of participants, changing connectivity, and message collisions with resulting losses. Consequently, designing and analyzing algorithms for these systems is very hard.

Failure detectors - oracles that provide information about process crashes - are an important abstraction for crash tolerance in distributed systems. Although current failure-detector theory provides great generality and expressiveness, it also poses significant challenges in developing a robust hierarchy of failure detectors. We address some of these challenges by proposing a variant of failure detectors called asynchronous failure detectors and an associated modeling framework. Unlike the traditional failure-detector framework, our framework eschews real time completely. We show that asynchronous failure detectors are sufficiently expressive to include several popular failure detectors. Additionally, we show that asynchronous failure detectors satisfy many desirable properties: they are self-implementable, guarantee that stronger asynchronous failure detectors solve more problems, and ensure that their outputs encode no information other than process crashes. We introduce the notion of a failure detector being representative of a problem to capture the idea that some problems encode the same information about process crashes as their weakest failure detectors do. We show that a large class of problems, called finite problems, do not have representative failure detectors.

The VNLayer approach simplifies software development for MANET by providing the developers an abstraction of a network divided into fixed geographical regions, each containing a virtual server for network services. In this paper, we present our study on reactive MANET routing over the VNLayer. During this research, we identified in our initial VNLayer implementation three major limitations that lead to heavy control traffic, long forwarding paths and frequent message collisions in MANET routing. To address the problems, we changed the assumptions made by the VNLayer on the link layer and extended the operations allowed by VNLayer. This results in a VNLayer implementation that can be tuned to optimize the performance of traffic intensive applications (such as routing) while maintaining their simplicity and robustness. Simulation results showed that VNAODV, a VNLayer based routing protocol adapted from AODV, delivers more packets, generates less routing traffic and creates more stable routes than AODV in a dense MANET with high node motion rates. This research validated that the VNLayer approach makes software development for MANET easier and improves the performance of MANET protocols.

In this paper we study the problem of building a connected dominating set with constant degree (CCDS) in the dual graph radio network model [4,9,10]. This model includes two types of links: reliable, which always deliver messages, and unreliable, which sometimes fail to deliver messages. Real networks compensate for this differing quality by deploying low-layer detection protocols to filter unreliable from reliable links. With this in mind, we begin by presenting an algorithm that solves the CCDS problem in the dual graph model under the assumption that every process u is provided a local link detector set consisting of every neighbor connected to u by a reliable link. The algorithm solves the CCDS problem in O(Δ\log2 n/b + log3 n) rounds, with high probability, where Δ is the maximum degree in the reliable link graph, n is the network size, and b is an upper bound in bits on the message size. The algorithm works by first building a Maximal Independent Set (MIS) in log3 n time, and then leveraging the local topology knowledge to efficiently connect nearby MIS processes. A natural follow up question is whether the link detector must be perfectly reliable to solve the CCDS problem. With this in mind, we first describe an algorithm that builds a CCDS in O(Δpolylog(n)) time under the assumption of O(1) unreliable links included in each link detector set. We then prove this algorithm to be (almost) tight by showing that the possible inclusion of only a single unreliable link in each process's local link detector set is sufficient to require Ω(Δ) rounds to solve the CCDS problem, regardless of message size. We conclude by discussing how to apply our algorithm in the setting where the topology of reliable and unreliable links can change over time.

Partial Reversal (PR) is a link reversal algorithm which ensures that the underlying graph structure is destination-oriented and acyclic. These properties of PR make it useful in routing protocols and algorithms for solving leader election and mutual exclusion. While proofs exist to establish the acyclicity property of PR, they rely on assigning labels to either the nodes or the edges in the graph. In this work we present simpler direct proof of the acyclicity property of partial reversal without using any external or dynamic labeling mechanism. First, we provide a simple variant of the PR algorithm, and show that it maintains acyclicity. Next, we present a binary relation which maps the original PR algorithm to the new algorithm, and finally, we conclude that the acyclicity proof applies to the original PR algorithm as well. 1

In this paper, we present automated formal verification of the DHCP Failover protocol. We conduct bounded model-checking for the protocol using Timeout Order Abstraction (TO-Abstraction), a technique to abstract a given timed model in a certain sub-class of loosely synchronized real-time distributed systems into an untimed model. A resulting untimed model from TO-abstraction is a finite state machine, and therefore one can verify the model using a conventional model-checker. We have verified the protocol by bounded model-checking up to depth 20. We also experimented with "mutating" the original code to examine the efficiency of bug-finding using TO-Abstraction. We used two mutated pieces of the original code. The first one represents a model that uses a stronger failure assumption. The second one represents a model that the protocol implementer has forgot to add a certain check of a received message. We found one counterexample for each of two pieces of mutated code. In particular, the counterexample that was found for the second mutated code had a complex scenario, and we believe that it is considerably difficult to find the counterexample by human or simulations.

Practitioners agree that unreliable links, which sometimes deliver messages and sometime do not, are an important characteristic of wireless networks. In contrast, most theoretical models of radio networks fix a static set of links and assume that these links are reliable. This gap between theory and practice motivates us to investigate how unreliable links affect theoretical bounds on broadcast in radio networks.

In this paper we investigate distributed computation in dynamic networks in which the network topology changes from round to round. We consider a worst-case model in which the communication links for each round are chosen by an adversary, and nodes do not know who their neighbors for the current round are before they broadcast their messages. The model captures mobile networks and wireless networks, in which mobility and interference render communication unpredictable. In contrast to much of the existing work on dynamic networks, we do not assume that the network eventually stops changing; we require correctness and termination even in networks that change continually. We introduce a stability property called T -interval connectivity (for T >= 1), which stipulates that for every T consecutive rounds there exists a stable connected spanning subgraph. For T = 1 this means that the graph is connected in every round, but changes arbitrarily between rounds.

The virtual node layer (VNLayer) is a programming abstraction for mobile ad hoc networks (MANETs). It defines simple virtual servers at fixed locations in a network, addressing a central problem for MANETs, which is the absence of fixed infrastructure. Advantages of this abstraction are that persistent state is maintained in each region, even when mobile nodes move or fail, and that simple wireline protocols can be deployed on the infrastructure, thereby taming the difficulties inherent in MANET setting. The major disadvantage is the messaging overhead for maintaining the persistent state. In this paper, we use simulation to determine the magnitude of the messaging overhead and the impact on the performance of the protocol. The overhead of maintaining the servers and the persistent state is small in bytes, but the number of messages required is relatively large. In spite of this, the latency of address allocation is relatively small and almost all mobile nodes have an address for 99 percent of their lifetime. Our ns-2 based simulation package (VNSim) implements the VNLayer using a leader-based state replication strategy to emulate the virtual nodes. VNSim efficiently simulates a virtual node system with up to a few hundred mobile nodes. VNSim can be used to simulate any VNLayer-based application.

Consider a setting where nodes can vary their transmission power thereby changing the network topology, the goal of topology control is to reduce the transmission power while ensuring the communication graph remains connected. Wattenhofer et al. [6] introduced the distributed cone-based topology control algorithm with parameter α (CBTC(α)) and proved it correct if α ≤ 2π/3. Li et al. [4] proposed performing asymmetric edge removal or increasing α to 5π/6, and proved that when applied separately these minimizations preserve connectivity. Bahramgiri et al. [1] proved that when α ≤ 2π/3 it was possible to extend the algorithm to work in three dimensions and described a variation to preserve k-connectivity.

We prove two broadcast lower bounds for a wireless network model that includes unreliable links. For deterministic algorithms, we show n − 1 rounds are required, where n is the number of processes. For randomized algorithms, ε(n − 1) rounds are required for success probability ε. In both cases, the bounds are proved for a network in which constant-time broadcast is possible.

We describe how a set of mobile robots can arrange themselves on any specified curve on the plane in the presence of dynamic changes both in the underlying ad hoc network and in the set of participating robots. Our strategy is for the mobile robots to implement a self-stabilizing virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs), and local broadcast communication. The VNs are associated with predetermined regions in the plane and coordinate among themselves to distribute the client nodes relatively uniformly among the VNs' regions. Each VN directs its local client nodes to align themselves on the local portion of the target curve. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired target formation.

Wireless ad hoc networks pose several significant challenges: devices are unreliable; deployments are unpredictable; and communication is erratic. One proposed solution is Virtual Infrastructure, an abstraction in which unpredictable and unreliable devices are used to emulate reliable and predictable infrastructure. In this paper, we present a new protocol for emulating virtual infrastructure in collision-prone wireless networks. At the heart of our emulation is a convergent history agreement protocol that tolerates lost messages and crash failures. It is designed specifically for ad hoc deployments, for example, the set of participants a priori unknown. The convergent history agreement protocol is quite efficient, as each agreement instance completes in a constant number of communication rounds, and the size of the messages is constant, independent of the length of the execution. Building on the convergent history agreement protocol, our virtual infrastructure emulation introduces only constant overhead per virtual round emulated. We believe that the techniques developed in this paper help to bring virtual infrastructure one step closer to a reality.

An indulgent algorithm is a distributed algorithm that, besides tolerating process failures, also tolerates unreliable information about the interleaving of the processes. This article presents a general characterization of indulgence in an abstract computing model that encompasses various communication and resilience schemes. We use our characterization to establish several results about the inherent power and limitations of indulgent algorithms.

Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A. We introduce a new type of simulation relation for hybrid automata— switching simulation —for establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT τ a can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. A solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton.

Task-PIOA is a modeling framework for distributed systems with both probabilistic and nondeterministic behaviors. It is suitable for cryptographic applications because its task-based scheduling mechanism is less powerful than the traditional perfect-information scheduler. Moreover, one can speak of two types of complexity restrictions: time bounds on description of task-PIOAs and time bounds on length of schedules. This distinction, along with the flexibility of nondeterministic specifications, are interesting departures from existing formal frameworks for computational security. The current paper presents a new approximate implementation relation for task-PIOAs. This relation is transitive and is preserved under hiding of external actions. Also, it is shown to be preserved under concurrent composition, with any polynomial number of substitutions. Building upon this foundation, we present the notion of structures, which classifies communications into two categories: those with a distinguisher environment and those with an adversary. We then formulate secure emulation in the spirit of traditional simulation-based security, and a composition theorem follows as a corollary of the composition theorem for the new approximate implementation relation.

We introduce a virtual-node based mobile object tracking algorithm for mobile sensor networks, VINESTALK. The algorithm uses the virtual stationary automata programming layer, consisting of mobile clients, virtual timed machines distributed at known locations in the plane, called virtual stationary automata (VSAs), and a communication service connecting VSAs and mobile clients. VINESTALK maintains a data structure on top of an underlying hierarchical partitioning of the network. In a grid partitioning, operations to find a mobile object distance d away take O(d) time and communication to complete. Updates to the tracking structure after the object has moved a total of d distance take O{d*log network diameter) amortized time and communication to complete. The tracked object may relocate without waiting for VINESTALK to complete updates for prior moves, and while a find is in progress.

Many problems in distributed computing are impossible when no information about process failures is available. It is common to ask what information about failures is necessary and sufficient to circumvent some specific impossibility, e.g., consensus, atomic commit, mutual exclusion, etc. This paper asks what information about failures is needed to circumvent any impossibility and sufficient to circumvent some impossibility. In other words, what is the minimal yet non-trivial failure informatio.

No abstract available.

Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAME-based theorem proving support provided in the toolkit, for proving system properties, including timing properties. Several examples are provided by way of illustration.

We prove an Ω(n log n) lower bound on the number of non-busywaiting memory accesses by any deterministic algorithm solving n process mutual exclusion that communicates via shared registers. The cost of the algorithm is measured in the state change cost model, a variation of the cache coherent model. Our bound is tight in this model. We introduce a novel information theoretic proof technique. We first establish a lower bound on the information needed by processes to solve mutual exclusion. Then we relate the amount of information processes can acquire through shared memory accesses to the cost they incur. We believe our proof technique is flexible and intuitive, and may be applied to a variety of other problems and system models.

We prove two theorems saying that no distributed system in which processes coordinate using reliable registers and f-resilient services can solve the consensus problem in the presence of f + 1 undetectable process stopping failures. (A service is f-resilient if it is guaranteed to operate as long as no more than f of the processes connected to it fail.) Our first theorem assumes that the given services are atomic objects, and allows any connection pattern between processes and services. In contrast, we show that it is possible to boost the resilience of systems solving problems easier than consensus: the k-set consensus problem is solvable for 2k - 1 failures using 1-resilient consensus services. The first theorem and its proof generalize to the larger class of failure-oblivious services. Our second theorem allows the system to contain failure-aware services, such as failure detectors, in addition to failure-oblivious services; however, it requires that each failure-aware service be connected to all processes. Thus, f + 1 process failures overall can disable all the failure-aware services. In contrast, it is possible to boost the resilience of a system solving consensus if arbitrary patterns of connectivity are allowed between processes and failure-aware services: consensus is solvable for any number of failures using only 1-resilient 2-process perfect failure detectors

The task of designing algorithms for constantly changing networks is difficult. We focus on mobile ad-hoc networks, where mobile processors attempt to coordinate despite minimal infrastructure support. We develop new techniques to cope with this dynamic, heterogeneous, and chaotic environment. We mask the unpredictable behavior of mobile networks by defining and emulating a virtual infrastructure, consisting of timing-aware and location-aware machines at fixed locations, that mobile nodes can interact with. The static virtual infrastructure allows appplication developers to use simpler algorithms — including many previously developed for fixed networks. Virtual Stationary Automata programming layer. Our programming abstraction consists of a static infrastructure of fixed, timed virtual machines with an explicit notion of real time, called Virtual Stationary Automata (VSAs), distributed at known locations over the plane, and emulated by the real mobile nodes in the system. Each VSA represents a predetermined geographic area and has broadcast capabilities similar to those of the mobile nodes, allowing nearby VSAs and mobile nodes to communicate with one another. This programming layer provides mobile nodes with a virtual infrastructure with which to coordinate their actions. Many practical algorithms depend significantly on timing, and it is reasonable to assume that many mobile nodes have access to reasonably synchronized clocks. In the VSA programming layer, the virtual automata also have access to virtual clocks, guaranteed to not drift too far from real time. Our virtual infrastructure differs in key ways from others that have previously been proposed for mobile ad-hoc networks. The GeoQuorums algorithm [2] was the first to use virtual nodes; the virtual nodes in that work are atomic objects at fixed geographical locations. More general virtual mobile automata were suggested in [1]; our automata are more powerful than those in [1] in that ours include timing capabilities, which are important for many applications. Also, our automata are stationary, and are arranged in a connected pattern that is similar to a traditional wired ne-

This work presents a strategy for compiling distributed systems specified in IOA, a formal language for describing such systems as I/O automata, into Java programs running on a group of networked workstations. The translation works node-by-node, translating IOA programs into Java classes that communicate using the message passing interface. The resulting system runs without any global synchronization. We prove that, subject to certain restrictions on the program to be compiled, assumptions on the correctness of hand-coded datatype implementations, and basic assumptions about the behavior of the network, the compilation method preserves safety properties of the IOA program in the generated Java code. We model the generated Java code itself as a threaded, low-level I/O automaton and use a refinement mapping to show that the external behavior of the system is preserved by the translation. The IOA compiler is part of the IOA toolkit which supports algorithm design, development, testing, and formal verification using automated tools.

No abstract available.

No abstract available.

We introduce the distributed gradient clock synchronization problem. As in traditional distributed clock synchronization, we consider a network of nodes equipped with hardware clocks with bounded drift. Nodes compute logical clock values based on their hardware clocks and message exchanges, and the goal is to synchronize the nodes' logical clocks as closely as possible, while satisfying certain validity conditions. The new feature of gradient clock synchronization (GCS for short) is to require that the skew between any two nodes' logical clocks be bounded by a nondecreasing function of the uncertainty in message delay (call this the distance) between the two nodes. That is, we require nearby nodes to be closely synchronized, and allow faraway nodes to be more loosely synchronized. We contrast GCS with traditional clock synchronization, and discuss several practical motivations for GCS, mostly arising in sensor and ad hoc networks. Our main result is that the worst case clock skew between two nodes at distance d from each other is Ω(d + log D log log D), where D is the diameter1 of the network. This means that clock synchronization is not a local property, in the sense that the clock skew between two nodes depends not only on the distance between the nodes, but also on the size of the network. Our lower bound implies, for example, that the TDMA protocol with a fixed slot granularity will fail as the network grows, even if the maximum degree of each node stays constant.

Future civilian rescue and military operations will depend on a complex system of communicating devices that can operate in highly dynamic environments. In order to present a consistent view of a complex world, these devices will need to maintain data objects with atomic (linearizable) read/write semantics.

I have had the honor of working with Mike Fischer on no fewer than 15 projects in the area of distributed computing theory, plus a few others in other areas. The results of some of these projects, like the one with Mike Paterson on impossibility of consensus, are very well known in the PODC community and elsewhere. Others are less well known, but I think are interesting anyway.I will take the opportunity of Mike's birthday celebration to review the many papers we have written together and describe their contributions. I will put the ideas of these papers in the context of earlier and later distributed computing theory research.These papers cover a wide range of topics within distributed computing theory. The papers include algorithms and/or impossibility results for mutual exclusion, k-exclusion, optimal resource placement in networks, consensus (synchronous and asynchronous), global snapshots, and implementing reliable communication over unreliable channels. One paper establishes a quantitative difference between the capabilities of synchronous and asynchronous systems. Another, dated 1980, presents an early levels-of-abstraction proof for a complex mutual exclusion algorithm. Yet another, dated 1979, presents a very early compositional model for fair asynchronous systems.

We describe the timed input/output automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new hybrid I/O automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and to express the important ideas of previous timed automata frameworks.

This paper presents a formal technique for incremental construction of system specifications, algorithm descriptions, and simulation proofs showing that algorithms meet their specifications.The technique for building specifications and algorithms incrementally allows a child specification or algorithm to inherit from its parent by two forms of incremental modification: (a) signature extension , where new actions are added to the parent, and (b) specialization (subtyping), where the child's behavior is a specialization (restriction) of the parent's behavior. The combination of signature extension and specialization provides a powerful and expressive incremental modification mechanism for introducing new types of behavior without overriding behavior of the parent; this mechanism corresponds to the subclassing for extension form of inheritance.In the case when incremental modifications are applied to both a parent specification S and a parent algorithm A, the technique allows a simulation proof showing that the child algorithm A′ implements the child specification S′ to be constructed incrementally by extending a simulation proof that algorithm A implements specification S. The new proof involves reasoning about the modifications only, without repeating the reasoning done in the original simulation proof.The paper presents the technique mathematically, in terms of automata. The technique has been used to model and verify a complex middleware system; the methodology and results of that experiment are summarized in this paper.

We present a mathematical state-machine model, the Dynamic I/O Automaton (DIOA) model, for defining and analyzing dynamic systems of interacting components. The systems we consider are dynamic in two senses: (1) components can be created and destroyed as computation proceeds, and (2) the set of events in which a component may participate can change as computation proceeds. The new model admits a notion of external system behavior, based on sets of traces. It also features a parallel composition operator for dynamic systems, which satisfies standard execution projection and pasting results, and a notion of simulation from one dynamic system to another, which can be used to prove that one system implements the other.

This talk will describe a new algorithm for implementing atomic objects in distributed settings where processes may fail (by stopping), and may also join and leave voluntarily. This strategy builds on Lamport's Paxos algorithm, and also on work by [Yeger-Lotem, Keidar, Dolev] and [De Prisco, Fekete, Lynch, Shvartsman] on view-oriented group communication.

Group communication services are becoming accepted as effective building blocks for the construction of fault-tolerant distributed applications. Many specifications for group communication services have been proposed. However, there is still no agreement about what these specifications should say, especially in cases where the services are partitionable , i.e., where communication failures may lead to simultaneous creation of groups with disjoint memberships, such that each group is unware of the existence of any other group. In this paper, we present a new, succinct specification for a view-oriented partitionable group communication service. The service associates each message with a particular view of the group membership. All send and receive events for a message occur within the associated view. The service provides a total order on the messages within each view, and each processor receives a prefix of this order. Our specification separates safety requirements from performance and fault-tolerance requirements. The safety requirements are expressed by an abstract, global state machine . To present the performance and fault-tolerance requirements, we include failure-status input actions in the specification; we then give properties saying that consensus on the view and timely message delivery are guaranteed in an execution provided that the execution stabilizes to a situation in which the failure-status stops changing and corresponds to consistently partioned system. Because consensus is not required in every execution, the specification is not subject to the existing impossibility results for partionable systems. Our specification has a simple implementation, based on the membership algorithm of Christian and Schmuck. We show the utility of the specification by constructing an ordered-broadcast application, using an algorithm (based on algorithms of Amir, Dolev, Keidar, and others) that reconciles information derived from different instantiations of the group. The application manages the view-change activity to build a shared sequence of messages, i.e., the per-view total orders of the group service are combined to give a universal total order. We prove the correctness and analyze the performance and fault-tolerance of the resulting application.

This paper presents a technique for incrementally constructing safety specifications, abstract algorithm descriptions, and simulation proofs showing that algorithms meet their specifications.

We prove tight bounds on the time needed to solve k-set agreement . In this problem, each processor starts with an arbitrary input value taken from a fixed set, and halts after choosing an output value. In every execution, at most k distinct output values may be chosen, and every processor's output value must be some processor's input value. We analyze this problem in a synchronous, message-passing model where processors fail by crashing. We prove a lower bound of ⌊f/k⌋+1 degree of coordination required, and the number of faults tolerated, even in idealized models like the synchronous model. The proof of this result is interesting because it is the first to apply topological techniques to the synchronous model.

We demonstrate a high-level approach to modeling, analyzing, and verifying complex safety-critical systems through a case study on the traffic alert and collision avoidance system (TCAS); an avionics system that detects and resolves aircraft collision threats. Due to the complexity of the TCAS software and the hybrid nature of the closed-loop system, the traditional testing technique of exhaustive simulation does not constitute a viable verification approach. Moreover, the detailed specification of the system software employed to date as a means toward analysis and verification neither helps in intuitively understanding the behavior of the system nor enables the analysis of the closed-loop system behavior. We advocate defining high-level hybrid system models that capture the behavior not only of the software but also of the airplanes, sensors, pilots, etc. In particular, we show how the core components of TCAS can be captured by relatively simple hybrid I/O automata, which are amenable to format analysis. We then outline a methodology for establishing conditions under which TCAS guarantees sufficient separation in altitude for aircraft involved in collision threats. The contributions of the paper are the high-level models of the closed-loop TCAS system and the demonstration of the usefulness of high-level modeling, analysis, and verification techniques.

The combination of two security protocols, a simple shared-key communication protocol and the Diffie-Hellman key distribution protocol, is modeled formally and proved correct. The modeling is based on the I/O automaton model for distributed algorithms, and the proofs are based on invariant assertions, simulation relations, and compositional reasoning. Arguments about the cryptosystems are handled separately from arguments about the protocols.

In this paper we demonstrate a high-level approach to modeling and analyzing complex safety-critical systems through a case study in the area of air traffic management. In particular, we focus our attention on the Traffic Alert and Collision Avoidance System (TCAS); an on-board conflict detection and resolution system which alerts pilots to the presence of nearby aircraft that pose a mid-air collision threat and issues conflict resolution advisories. Due to the complexity of the TCAS software and the hybrid nature of the closed-loop system, the traditional testing techniques through simulation do not constitute a viable verification approach. To aid people in analyzing and designing such systems, we advocate defining high-level mathematical system models that capture the behavior not only of the software, but also of the airplanes, sensors, and pilots-that is, high-level hybrid system models. In particular we show how the core components of this complex system can be captured by relatively simple Hybrid I/O Automata (HIOA) which are amenable to formal analysis. We then outline a methodology for establishing conditions under which the conflict resolution advisories issued by TCAS guarantee sufficient separation in altitude for aircraft involved in mid-air collision threats. Although our results are intended only as illustrations of high-level modeling and analysis techniques, the TCAS system models provide a foundation for study of a wide range of properties of the system's behavior.

View-oriented group communication services are widely used for fault-tolerant distributed computing.For applications involving coherent data, it is importaut to know when a process has a primary view of the current group membership, usually defined as a view containing a majority out of a static universe of processes.For high availability in a system where processes can join and leave routinely, some researchers have suggested def?.ning primary views dynamically, depending on having enough members in common with recent views.We present a new formal automaton specification, DVS, for the safety guarantees made by a practical group communication service providing a dynamic notion of primary view.We demonstrate the value of DVS by showing both how it can be implemented and how it can be used in an application.First, we present a distributed algorithm based on a group membership algorithm of Lotem, Keidar and Dolev; our version integrates communication with the membership service, uses iuformation from the application processes saying when a view has been prepared for computation by the application, and uses a static view-oriented service internally.We prove that this algorithm implements DVS.Second, we present an application algorithm that is a variant of an algorithm of Amir, Dolev, Keidar, Melliar-Smith and Moser, modified to use DVS instead of a static service.We prove that it implements a (non-group-oriented) totally-orderedbroadcast service.

This paper presents and proves correct a distributed algorithm that implements a sequentially consistent collection of shared read/update objects. This algorithm is a generalization of one used in the Orca shared object system. The algorithm caches objects in the local memory of processors according to application needs; each read operation accesses a single copy of the object, while each update accesses all copies. The algorithm uses broadcast communication when it sends messages to replicated copies of an object, and it uses point-to-point communication when a message is sent to a single copy, and when a reply is returned. Copies of all objects are kept consistent using a strategy based on sequence numbers for broadcasts. The algorithm is presented in two layers. The lower layer uses the given broadcast and point-to-point communication services, plus sequence numbers, to provide a new communication service called acontext multicast channel. The higher layer uses a context multicast channel to manage the object replication in a consistent fashion. Both layers and their combination are described and verified formally, using the I/O automation model for asynchronous concurrent systems.

Group communication services are becoming accepted as effective building blocks for the construction of fault-tolerant distributed applications. Many specifications for group communication services have been proposed. However, there is still no agreement about what these specifications should say, especially in cases where the services are partitionable, i.e., where communication failures may lead to simultaneous creation of groups with disjoint memberships, such that each group is unware of the existence of any other group. In this paper, we present a new, succinct specification for a view-oriented partitionable group communication service. The service associates each message with a particular view of the group membership. All send and receive events for a message occur within the associated view. The service provides a total order on the messages within each view, and each processor receives a prefix of this order. Our specification separates safety requirements from performance and fault-tolerance requirements. The safety requirements are expressed by an abstract, global state machine. To present the performance and fault-tolerance requirements, we include failure-status input actions in the specification; we then give properties saying that consensus on the view and timely message delivery are guaranteed in an execution provided that the execution stabilizes to a situation in which the failure-status stops changing and corresponds to consistently partioned system. Because consensus is not required in every execution, the specification is not subject to the existing impossibility results for partionable systems. Our specification has a simple implementation, based on the membership algorithm of Christian and Schmuck. We show the utility of the specification by constructing an ordered-broadcast application, using an algorithm (based on algorithms of Amir, Dolev, Keidar, and others) that reconciles information derived from different instantiations of the group. The application manages the view-change activity to build a shared sequence of messages, i.e., the per-view total orders of the group service are combined to give a universal total order. We prove the correctness and analyze the performance and fault-tolerance of the resulting application.

We present a new specification for distributed data services that trade-off immediate consistency guarantees for improved system availability and efficiency, while ensuring the long-term consistency of the data.An eventually-serializable data service maintains the operations requested in a partial order that gravitates over time towards a total order.It provides clear and unambiguous guarantees about the immediate and long-term behavior of the system.To demonstrate its utility, we present an algorithm, based on one of Ladin, Liskov, Shrira, and Ghemawat [12], that implements this specification.Our algorithm provides the interface of the abstract service, and generalizes their algorithm by allowing general operations and greater flexibility in specifying consistency requirements.We also describe how to use this specification as a building block for applications such as directory services.1

No abstract available.

Counting networks are a class of concurrent structures that allow the design of highly scalable concurrent data structures in a way that eliminates sequential bottlenecks and contention.Linearizable counting networks assure that the order of the values returned by the network reflects the real-time order in which they were requested.We argue that in many concurrent systems the worst case scenarios that violate linearizability require a form of timing anomaly that is uncommon in practice.The linear time cost of designing networks that achieve linearizability under all circumstances may thus prove an unnecessary burden on applications that are willing to trade-off occasional non-linearizability for speed and parallelism.This paper presents a very simple measure that is iocal to the individual links and nodes of the network, and that quantifies the extent to which a network can suffer from timing anomalies and still remain linearizable.Perhaps counter-intuitively, this measure is independent of network depth.We use our measure to mathematically support our experiment al results: that in a variety of normal situations tested on a simulated shared memory multiprocessor, the Monic counting networks of Aspnes, Herlihy, and Shavit are "for all practical purposes" Iinearizable.

Several example vehicle deceleration manoeuvres arising in automated transportation systems are specified, and their correctness verified, using the hybrid I/O automaton model of (Lynch et al., 1995). All system components are formalized using hybrid I/O automata, and their combination described using automaton composition. The proofs use invariant assertions, simulation mappings, and differential calculus.

Abstract The timed automaton model of [LyV92, LyV93] is a general model for timing-based systems. A notion of timed action transducer is here defined as an automata-theoretic way of representing operations on timed automata. It is shown that two timed trace inclusion relations are substitutive with respect to operations that can be described by timed action transducers. Examples are given of operations that can be described in this way, and a preliminary proposal is given for an appropriate language of operators for describing timing-based systems.

A distributed algorithm that implements a sequentially consistent collection of shared read/update objects using a combination of broadcast and point-to-point communication is presented and proved correct. This algorithm is a generalization of one used in the Orca shared object system. The algorithm caches objects in the local memory of processors according to application needs; each read operation accesses a single copy of the object, while each update accesses all copies. Copies of all the objects are kept consistent using a strategy based on sequence numbers for broadcasts. The algorithm is presented in two layers. The lower layer uses the given broadcast and point-to-point communication services, plus sequence numbers, to provide a new communication service called a context multicast channel. The higher layer uses a context multicast channel to manage the object replication in a consistent fashion. Both layers and their combination are described and verified formally, using the I/O automaton model for asynchronous concurrent systems.

Abstract Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output automata; both safety and liveness properties are considered. A small but typical circuit is verified in both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I/O automata. An extended evaluation and comparison of the two methods is given.

Article Free Access Share on Proving time bounds for randomized distributed algorithms Authors: Nancy Lynch Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile , Isaac Saias Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile , Roberto Segala Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile Authors Info & Claims PODC '94: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computingAugust 1994 Pages 314–323https://doi.org/10.1145/197917.198117Published:14 August 1994Publication History 45citation508DownloadsMetricsTotal Citations45Total Downloads508Last 12 Months10Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

A new solution to the generalized railroad crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model.>

Layered communicationprotocols frequently implement a FIFO message fiacility cm top of an unrehable non-FIFO serwce such as that provided hy a packet-swltchmg network.This paper investigates the possibdity of Implementing a reliable message layer on top of an underlying layer that can low packets and deliver them out of order, with the addltlonzd restriction that the implementatmn uses only a fixed fimte number of different packets.A new formalism is presented to spcclfy communication layers and their properties, the notion of their implementation by 1/0 automata.and the properties of such implementations.An 1/0 automaton that Implements a rellable layer over an unreliable layer is presented In this implementation, tbe number ot packets needed to deliver each succeeding message increases permanently as additional packet-loss and reordering faults occur.A proof is gwen that no protocol can avoid such performance degradatmn.

Upper and lower bounds are proved for the time complexity of the problem of reaching agreement m a distributed network m the presence of process fwlures and inexact information about time.It is assumed that the amount of (real) time between any two consecutwe steps of any ncmfatrhy process is at least c1 and at most C2; thus, C = cz/cl is a measure of the timing uncertainty.It E also assumed that the time for message dehvery ]s at most d.Processes are assumed to fail by stopping, so that process fdures can be detected by timeouts.A straightforward adaptation of an (~+ 1)-round round-based agreement algorithm takes time (f + l)Cd If there are f potential faults, while a straightforward mochflcation of the proof that f'+ 1 rounds are required yields a lower bound of time (~+ 1)d.The frost result of this paper is m agreement algorlthm in which the uncerttimty factor C is only incurred for one round, yielding A preliminary version of this work appeared in Proceedings of the 23rd ACM SvrnposamZ on Theon of Corrrputmg (New Orleans, La., May 6-8).ACM, New York, 1991, pp.359-369.

The time complexity of wait-free algorithms in “normal” executions, where no failures occur and processes operate at approximately the same speed, is considered. A lower bound of log n on the time complexity of any wait-free algorithm that achieves approximate agreement among n processes is proved. In contrast, there exists a non-wait-free algorithm that solves this problem in constant time. This implies an Ω(log n ) time separation between the wait-free and non-wait-free computation models. On the positive side, we present an O(log n ) time wait-free approximate agreement algorithm; the complexity of this algorithm is within a small constant of the lower bound.

Gifford's Quorum Consensus algorithm for data replication is studied in the context of nested transactions and transaction failures (aborts), and a fully developed reconfiguration strategy is presented. A formal description of the algorithm is presented using the Input/Output automaton model for nested-transaction systems due to Lynch and Merritt. In this description, the algorithm itself is described in terms of nested transactions. The formal description is used to construct a complete proof of correctness that uses standard assertional techniques, is based on a natural correctness condition, and takes advantage of modularity that arises from describing the algorithm as nested transactions. The proof is accomplished hierarchically, showing that a fully replicated reconfigurable system “simulates” an intermediate replicated system, and that the intermediate system simulates an unreplicated system. The presentation and proof treat issues of data replication entirely separately from issues of concurrency control and recovery.

We prove tight bounds on the time needed to solve k-set agreement, a natural generalization of consensus. We analyze this problem in a synchronous, message-passing model where processors fail by crashing. We prove a lower bound of [f/k]+1 rounds of communication for solutions to k-set agreement that tolerate f failures. This bound is tight, and shows that there is an inherent tradeoff between the running time, the degree of coordination required, and the number of faults tolerated, even in idealized models like the synchronous model. The proof of this result is interesting because it is a geometric combination of other well-known proof techniques.>

Much of modernsystems programming involves designing algorithms for distributed systems in which the nodes have access to information about time.Time information can be used to estimate the time at which system or environment events occur, to detect process failures, to schedule the use of

An important function of communication networks is to implement reliable data transfer over an unreliable underlying network.Formal specifications are given for reliable and unreliable communication layers, in terms of 1/0 automata.Based on these specifications, it is proved that no reliable communication protocol can tolerate crashes of the processors on which the protocol runs.

We study randomized, synchronous protocols for coordinated attack.Such protocols trade offthe number of rounds (N), the worst case probability of disagreement (U), and the probability that all generals attack (Z).We prove a nearly tight bound on the tradeoff between L and U (L/U ~N) for a strong adversary that destroys any subset of messages.Our techniques may be useful for other problems that allow a nonzero probability of disagreement.

The benefits that can be obtained by using timing information in mutual exclusion algorithms are examined. A simple and efficient timing-based mutual exclusion algorithm is given. This algorithm always guarantees mutual exclusion (i.e. even when run asynchronously) and also avoids deadlock in case certain (realistic) inexact timing constraints are met. The algorithm uses only two shared read/write registers (a total of log n+1 bits), thus overcoming the n register lower bound for asynchronous algorithms. It is proved that the problem cannot be solved with only one shared register, so that this algorithm is optimal in terms of the number of registers. A lower bound is proved for the time complexity of any deadlock-free mutual exclusion protocol, as a function of the number of shared registers it employs. This bound shows that the algorithm described is near optimal, in terms of time complexity. It is shown that two natural ways of weakening the timing assumptions lead (unfortunately) to an n register lower bound.>

The problem of placing a number t of identical resources at nodes of a tree so as to minimize the total expected cost of servicing a set of t requests arriving randomly at nodes is considered. The cost of servicing a particular set of requests is the total distance in the tree between each request and its assigned resource. Distance is measured by the number of edges along the unique path from the request to the resource. Optimal placements can be found in time O(mt), where m is the number of edges in the tree. Allowing resources to be split into fractional-sized pieces which can be placed separately neither reduces the cost of an optimal placement nor provides an obvious way to find optimal placements significantly faster. Simple, natural “fair” placements whose cost differs from optimality by at most the number of edges in the tree are described. For any fixed tree T, the cost of these placements grows as O(t), where the constant implicit in the “O” notation depends on the size and shape of T. In the case of balanced trees with k leaves, that constant is at most 2kφ. The placement problem becomes somewhat simpler for a complete (rooted) d-ary tree with a symmetric probability density function for request arrivals, and in that case slightly stronger results are possible. For example, an optimal placement can be found in time O(min{ℓ, logdt} + t), where ℓ is the height of the tree, and the placement is symmetric and fair.

In a distributed system, node failures, network delays, and other unpredictable occurences can result in orphan computations—subcomputations that continue to run but whose results are no longer needed. Several algorithms have been proposed to prevent such computations from seeing inconsistent states of the shared data. In this paper, two such orphan management algorithms are analyzed. The first is an algorithm implemented in the Argus distributed-computing system at MIT, and the second is an algorithm proposed at Carnegie-Mellon. The algorithms are described formally, and complete proofs of their correctness are given. The proofs show that the fundamental concepts underlying the two algorithms are very similar in that each can be regarded as an implementation of the same high-level algorithm. By exploiting properties of information flow within transaction management systems, the algorithms ensure that orphans only see states of the shared data that they could also see if they were not orphans. When the algorithms are used in combination with any correct concurrency control algorithm, they guarantee that all computations, orphan as well as nonorphan, see consistent states of the shared data.

. Upper and lower bounds are proved for the time complexity of the problem of reaching agreement in a distributed network in the presence of process failures and inexact information about time. It is assumed that the amount of (real) time between any two consecutive steps of any nonfaulty process is at least c 1 and at most c 2 ; thus, C = c 2 =c 1 is a measure of the timing uncertainty. It is also assumed that the time for message delivery is at most d. Processes are assumed to fail by stopping, so that process failures can be detected by timeouts. A straightforward adaptation of an (f + 1)-round round-based agreement algorithm takes time (f + 1)Cd if there are f potential faults, while a straightforward modification of the proof that f + 1 rounds are required yields a lower bound of time (f + 1)d. The first result of this paper is an agreement algorithm in which the uncertainty factor C is only incurred for one round, yielding a running time of approximately 2fd + Cd in the worst ca...

The time complexity of wait-free algorithms in so-called normal executions, where no failures occur and processes operate at approximately the same speed, is considered. A lower bound of log n on the time complexity of any wait-free algorithm that achieves approximate agreement among n processes is proved. In contrast, there exists a non-wait-free algorithm that solves this problem in constant time. This implies an Omega (log n)-time separation between the wait-free and non-wait-free computation models. An O(log n)-time wait-free approximate agreement algorithm is presented. Its complexity is within a small constant of the lower bound.>

The I/O automation model of N.A. Lynch and M.R. Tuttle (1987) is extended to allow modeling of shared memory systems, as well as systems that include both shared memory and shared action communication. A full range of types of atomic accesses to shared memory is allowed, from basic reads and writes to read-modify-write. The extended model supports system description, verification, and analysis. As an example, E.W. Dijkstra's (1965) classical shared memory mutual exclusion algorithm is presented and proven correct.>

A new technique for proving timing properties for timing-based algorithms is described; it is an extension of the mapping techniques previously used in proofs of safety properties for asynchronous concurrent systems.The key to the method is a way of representing a system with timing constraints as an automaton whose state includes predictive timing information.Timing assumptions and timing requirements for the system are both represented in this way.A multivalued mapping from the "assumptions automaton"to the "requirements automaton" is then used to show that the given system satisfies the requirements.The technique is illustrated with two simple examples, a resource manager and a signal relay system, and a third, more complex example of a two-process race system.The technique is shown to be complete, that is, if some automaton with certain timing assumptions has certain timing behavior, than there exists a mapping from the "assumptions automaton"to the "requirements automaton".

This paper makes three contributions. First, we present a proof technique that offers system designers the same ease of reasoning about nested transaction systems as is given by the classical theory for systems without nesting, and yet can be used to verify that a system satisfies the robust “user view” definition of correctness of [10]. Second, as applications of the technique, we verify the correctness of Moss' read/write locking algorithm for nested transactions, and of an undo logging algorithm that has not previously been presented or proved for nested transaction systems. Third, we make explicit the assumptions used for this proof technique, assumptions that are usually made implicitly in the classical theory, and therefore we clarify the type of system for which the classical theory itself can reliably be used.

this technical assumption is necessary.) The arguments are basically similar to those of based on the pigeonhole principle applied to values of shared memory, only in place of case analysis there is a more systematic examination of executions

A timing-based variant of the mutual-exclusion problem is considered. In this variant, only an upper bound on the time it takes to release the resource is known, and no explicit signal is sent when the resource is released; furthermore, the only mechanism to measure real time is an inaccurate clock, whose tick intervals take time between two constants. A new technique involving shifting and shrinking executions is combined with a careful analysis of the best allocation policy to prove a corresponding lower bound when control is distributed among processes connected by communication lines with an upper bound for message delivery time. These combinatorial results shed some light on modeling and verification issues related to real-time systems.>

We present a simple and efficient algorithm for the FIFO allocation of k identical resources among asynchronous processes that communicate via shared memory. The algorithm simulates a shared queue but uses exponentially fewer shared memory values, resulting in practical savings of time and space as well as program complexity. The algorithm is robust against process failure through unannounced stopping, making it attractive also for use in an environment of processes of widely differing speeds. In addition to its practical advantages, we show that for fixed k , the shared space complexity of the algorithm as a function of the number N of processes is optimal to within a constant factor.

The problem of implementing reliable broadcast in ARPA-like computer networks is studied. The environment is characterized by the absence of any multicast facility on the communication by the absence of any multicast facility on the communications subnetwork level. Thus, broadcast has to be implemented directly on hosts. A reliable broadcast protocol is presented and evaluated with respect to several important performance criteria.>

Article Free Access Share on Data link layer: two impossibility results Authors: Nancy A. Lynch Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile , Yishay Mansour Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile , Alan Fekete Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile Authors Info & Claims PODC '88: Proceedings of the seventh annual ACM Symposium on Principles of distributed computingJanuary 1988 Pages 149–170https://doi.org/10.1145/62546.62572Published:01 January 1988Publication History 21citation530DownloadsMetricsTotal Citations21Total Downloads530Last 12 Months95Last 6 weeks8 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Article Free Access Share on A lattice-structured proof of a minimum spanning Authors: Jennifer L. Welch Laboratory for Computer Science, Massachusetts Institute of Technology Laboratory for Computer Science, Massachusetts Institute of TechnologyView Profile , Leslie Lamport Digital Equipment Corporation, Systems Research Center Digital Equipment Corporation, Systems Research CenterView Profile , Nancy Lynch Laboratory for Computer Science, Massachusetts Institute of Technology Laboratory for Computer Science, Massachusetts Institute of TechnologyView Profile Authors Info & Claims PODC '88: Proceedings of the seventh annual ACM Symposium on Principles of distributed computingJanuary 1988 Pages 28–43https://doi.org/10.1145/62546.62552Published:01 January 1988Publication History 12citation368DownloadsMetricsTotal Citations12Total Downloads368Last 12 Months13Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

The concept of partial synchrony in a distributed system is introduced. Partial synchrony lies between the cases of a synchronous system and an asynchronous system. In a synchronous system, there is a known fixed upper bound Δ on the time required for a message to be sent from one processor to another and a known fixed upper bound Φ on the relative speeds of different processors. In an asynchronous system no fixed upper bounds Δ and Φ exist. In one version of partial synchrony, fixed bounds Δ and Φ exist, but they are not known a priori. The problem is to design protocols that work correctly in the partially synchronous system regardless of the actual values of the bounds Δ and Φ. In another version of partial synchrony, the bounds are known, but are only guaranteed to hold starting at some unknown time T , and protocols must be designed to work correctly regardless of when time T occurs. Fault-tolerant consensus protocols are given for various cases of partial synchrony and various fault models. Lower bounds that show in most cases that our protocols are optimal with respect to the number of faults tolerated are also given. Our consensus protocols for partially synchronous processors use new protocols for fault-tolerant “distributed clocks” that allow partially synchronous processors to reach some approximately common notion of time.

Gifford's basic Quorum Consensus algorithm for data replication is generalized to accommodate nested transactions and transaction failures (aborts), A formal description of the generalized algorithm is presented using the new Lynch-Merritt inputoutput automaton model for nested transaction systems.This formal description is used to construct a complete (yet simple) proof of correctness that uses standard assertional techniques and is based on a natural correctness condition.The presentation and proof treat issues of data replication entirely separately from issues of concurrency control and recovery-

Abstract: We introduce the input-output automaton, a simple but powerful model of computation in asynchronous distributed networks. With this model we are able to construct modular, hierarchical correctness proofs for distributed algorithms. We de ne this model, and give aninteresting example of how itcan be used to construct such proofs. 1

We give a clear yet rigorous correctness proof for Moss's algorithm for managing data in a nested transaction system. The algorithm, which is the basis of concurrency control and recovery in the Argus system, uses read- and write-locks and a stack of versions of each object to ensure the serializability and recoverability of transactions accessing the data. Our proof extends earlier work on exclusive locking to prove that Moss's algorithm generates serially correct executions in the presence of concurrency and transaction aborts. The key contribution is the identification of a simple property of cead operations, called transparency, that permits shared locks to be used for read operations.

The problem of electing a leader in a synchronous ring of n processors is considered. Both positive and negative results are obtained. On the one hand, if processor IDS are chosen from some countable set, then there is an algorithm that uses only O ( n ) messages in the worst case. On the other hand, any algorithm that is restricted to use only comparisons of IDs requires Ω( n log n ) messages in the worst case. Alternatively, if the number of rounds is required to be bounded by some t in the worst case, and IDs are chosen from any set having at least ƒ( n, t ) elements, for a certain very fast-growing function ƒ, then any algorithm requires Ω( n log n ) messages in the worst case.

A replicated database architecture is described in which updates processed at a site must be saved to allow reconcilliation of newly arriving updates in a way that preserves mutual consistency. The storage space occupied by the saved updates increases indefinitely, and periodic discarding of old updates is needed to avoid running out of storage. A protocol is described which allows sites in the system to agree that updates older than a given timestamp are no longer needed and can be discarded. This protocol uses a "distributed snapshot" algorithm of Chandy and Lamport and represents a practical application of that algorithm. A protocol for permanent removal of sites is also described, which will allow the discarding of updates to continue when one or more sites crash and are expected not to recover.

C<,retoness conditicms arc given which describe some nf tile pt'tq~crlie~ c×hibiLed by Ilighly aw~itable distributed database systems sttch a:; the 511,'x.RI) (Systcnl I~n' l lighly Available Replicated Data) ,¢.ystem cuurcntlv be~hg developed at Comptller Corporation of /~l]lOi'iC;i.This svslcm allows a da~d~ase application to contilme OpClatlt:~l ill tile lace o1" communicatiun faih.llCS,incheding fietwork pa0"tidons.A penalty is paid tbr thir; c×tz'a availability: the usual corrc,:tncss conditi,n,~; serializability of tr:msactions and preservation of iritcgrily c,n.~traims, ,:re not guaranteed.I Iowevcr, it is still possihle to make intcrestin~g claims about the beh,vior e,f the system.The kinds of claims whicli can be 9roved include bom~ds on tile costs oF violatior, of integrity cofistraints, and Ihirness guma,tces.In comrast to serializ~bility:s all-or-m~thing character, this work has a "continuous" flavor:small changes in available inform~itiou lead a) small perturbations in corrcctuess conditk)ns."['l:.iswork is novel, because there has been very little previous success in'stating .inlcresti'ngproperties whk:h are guaranteed by nonscrializable systems.

This paper considers a variant of the Byzantine Generals problem, in which processes start with arbitrary real values rather than Boolean values or values from some bounded range, and in which approximate, rather than exact, agreement is the desired goal. Algorithms are presented to reach approximate agreement in asynchronous, as well as synchronous systems. The asynchronous agreement algorithm is an interesting contrast to a result of Fischer et al, who show that exact agreement with guaranteed termination is not attainable in an asynchronous system with as few as one faulty process. The algorithms work by successive approximation, with a provable convergence rate that depends on the ratio between the number of faulty processes and the total number of processes. Lower bounds on the convergence rate for algorithms of this form are proved, and the algorithms presented are shown to be optimal.

Article Free Access Share on Easy impossibility proofs for distributed consensus problems Authors: Michael J. Fischer Yale University, New Haven, CT Yale University, New Haven, CTView Profile , Nancy A. Lynch Mass. Inst. of Tech., Cambridge, MA Mass. Inst. of Tech., Cambridge, MAView Profile , Michael Merritt AT&T Bell Labs., Murray Hill, NJ and Mass. Inst. of Tech., Cambridge, MA AT&T Bell Labs., Murray Hill, NJ and Mass. Inst. of Tech., Cambridge, MAView Profile Authors Info & Claims PODC '85: Proceedings of the fourth annual ACM symposium on Principles of distributed computingAugust 1985 Pages 59–70https://doi.org/10.1145/323596.323602Online:01 August 1985Publication History 47citation743DownloadsMetricsTotal Citations47Total Downloads743Last 12 Months26Last 6 weeks7 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

The consensus problem involves an asynchronous system of processes, some of which may be unreliable. The problem is for the reliable processes to agree on a binary value. In this paper, it is shown that every protocol for this problem has the possibility of nontermination, even with only one faulty process. By way of contrast, solutions are known for the synchronous case, the “Byzantine Generals” problem.

We describe a new fault-tolerant algorithm for solving a variant of Lamport's clock synchronization problem. The algorithm is designed for a system of distributed processes that communicate by sending messages. Each process has its own read-only physical clock whose drift rate from real time is very small. By adding a value to its physical clock time, the process obtains its local time. The algorithm solves the problem of maintaining closely synchronized local times, assuming that processes' local times are closely synchronized initially. The algorithm is able to tolerate the failure of just under a third of the participating processes. It maintains synchronization to within a small constant, whose magnitude depends upon the rate of clock drift, the message delivery time, and the inital closeness of synchronization. We also give a characterization of how far the clocks drift from real time. Reintegration of a repaired process can be accomplished using a slight modification of the basic algorithm. A similar style algorithm can also be used to achieve synchronization initially.

We consider the problem of electing a leader in a synchronous ring of n processors. We obtain both positive and negative results.

The consensus problem involves an asynchronous system of processes, some of which may be unreliable. The problem is for the reliable processes to agree on a binary value. We show that every protocol for this problem has the possibility of nontermination, even with only one faulty process. By way of contrast, solutions are known for the synchronous case, the "Byzantine Generals" problem.

Article Free Access Share on Concurrency control for resilient nested transactions Author: Nancy A. Lynch Massachusetts Institute of Technology, Cambridge, Massachusetts Massachusetts Institute of Technology, Cambridge, MassachusettsView Profile Authors Info & Claims PODS '83: Proceedings of the 2nd ACM SIGACT-SIGMOD symposium on Principles of database systemsMarch 1983 Pages 166–181https://doi.org/10.1145/588058.588080Online:21 March 1983Publication History 18citation206DownloadsMetricsTotal Citations18Total Downloads206Last 12 Months1Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

article Free Access Share on Efficiency of Synchronous Versus Asynchronous Distributed Systems Authors: Eshrat Arjomandi Department of Computer Science, York University, Downsview, Ontario, Canada M3J 1P3 Department of Computer Science, York University, Downsview, Ontario, Canada M3J 1P3View Profile , Michael J. Fischer Department of Computer Science, Yale University, P.O. Box 2158, New Haven, CT and University of Washington, Seattle, Washington Department of Computer Science, Yale University, P.O. Box 2158, New Haven, CT and University of Washington, Seattle, WashingtonView Profile , Nancy A. Lynch Laboratory for Computer Science, M.I.T., Cambridge, MA Laboratory for Computer Science, M.I.T., Cambridge, MAView Profile Authors Info & Claims Journal of the ACMVolume 30Issue 3July 1983 pp 449–456https://doi.org/10.1145/2402.322387Published:01 July 1983Publication History 46citation865DownloadsMetricsTotal Citations46Total Downloads865Last 12 Months51Last 6 weeks9 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Multilevel atomicity , a new correctness criteria for database concurrency control, is defined. It weakens the usual notion of serializability by permitting controlled interleaving among transactions. It appears to be especially suitable for applications in which the set of transactions has a natural hierarchical structure based on the hierarchical structure of an organization. A characterization for multilevel atomicity, in terms of the absence of cycles in a dependency relation among transaction steps, is given. Some remarks are made concerning implementation.

Article Free Access Share on Multilevel atomicity Author: Nancy A. Lynch Massachusetts Institute of Technology, Cambridge, Massachusetts and Georgia Institute of Technology, Atlanta, Georgia Massachusetts Institute of Technology, Cambridge, Massachusetts and Georgia Institute of Technology, Atlanta, GeorgiaView Profile Authors Info & Claims PODS '82: Proceedings of the 1st ACM SIGACT-SIGMOD symposium on Principles of database systemsMarch 1982 Pages 63–69https://doi.org/10.1145/588111.588123Online:29 March 1982Publication History 0citation162DownloadsMetricsTotal Citations0Total Downloads162Last 12 Months1Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

A cryptographic transformation is a mapping f from a set of cleartext messages, M, to a set of ciphertext messages. Since for m e M, f(m) should hide the contents of m from an enemy, f-1 should, in a certain technical sense, be difficult to infer from f(m) and public knowledge about f.

An analysis is made of the shared memory requirements for implementing mutual excluslon of N asynchronous parallel processes m a model where the only primitive communication mechamsm is a general test-and-set operation on a single shared variable.While two variable values suffice to tmplement simple mutual exclusion without deadlock, it is shown that any solution whJch avoids possJble lockout of processes requires at least 2~ + ½ values A technical restnctmn on the model increases this requtrement to N/2 values, while achieving a fixed bound on wamng further increases the reqmrement to N + 1 values.These bounds are shown to be nearly optimal, for algorithms are exhibited for the last two cases which use [N/2J + 9 and N + 3 values, respectively All of the lower bounds apply afortiori to the space requirements for weaker primitives, such as P and V, using busy waiting Categones and Subject Descnptors D 4 1 [Operating Systems]" Process Management--mutual exclusion; D 4 2 [Operating Systems]' Storage Management F ! ![Computation by Abstract Devices]: Models of Computation, F !.2 [Computation by Abstract Devices]" Modes ofComputaUon--parallehsm, F 2 [Theory of Computation] Analysis of Algorithms and Problem Complexity General Terms Algonthms, Performance, Theory

A global state of a distributed transaction system is consistent if no transactions are in progress. A global checkpoint is a transaction which must view a globally consistent system state for correct operation. We present an algorithm for adding global checkpoint transactions to an arbitrary distributed transaction system. The algorithm is nonintrusive in the sense that checkpoint transactions do not interfere with ordinary transactions in progress; however, the checkpoint transactions still produce meaningful results.

A system of parallel processes is said to be synchronous if all processes run using the same clock, and it is asynchronous if each process has its own independent clock. For any s, n, a particular distributed problem is defined involving system behavior at n “ports”. This problem can be solved in time s by a synchronous system but requires time at least (s-1) log n on any asynchronous system.

this paper, the problem is generalized to a distributed system resource allocation problem which is local in two senses. First, although the system and number of users can be very large, there is a limit to the overlap in resource demands of different users. The second condition can be thought of as a property of the geography of the network - the resources are (or can be) located in the network in such a way that connunication between a user and any of its required resources is fast. Both types of locality conditions are satisfied by the Dining Philosophers problem. Under these two conditions, one would hope that waiting chains could be avoided, so that the worst-case time to grant a user's requests is independent of the total size of the network and the total number of users

A model of computation is introduced which permits the analysis of both the time and space requirements of non-oblivious programs. Using this model, it is demonstrated that any algorithm for sorting n inputs which is based on comparisons of individual inputs requires time-space product proportional to n2. Uniform and non-uniform sorting algorithms are presented which show that this lower bound is nearly tight.

Upper and lower bounds are proved for the shared space requirements for solution of several problems involving resource allocation among asynchronous processes. Controlling the degradation of performance when a limited number of processes fail is of particular interest.

A definition is proposed for a size measure to be used as a parameter for algorithm analysis in any algebra. The parameter is simply the straight-line program length in the associated free algebra. This parameter generalizes the usual measures in basic arithmetic and string algebras, as well as some apparently different measures used for data structure algorithms. Another use is illustrated with an introduction to complexity-bounded group theory. I. INT~00ucT10N This paper continues the work in [9-l 21 directed toward the development of a unified, relative framework for complexity theory. Those papers establish a natural model for situations in which each data element is regarded as “atomic”; for example, it can be copied in one computation step. The attractiveness of the model is demonstrated by its use in stating and proving a variety of technical results, prin-cipally involving data types whose elements are bit strings or natural numbers. It would be useful to extend those ideas to.data types whose elements are not usually regarded as atomic (such as matrices, graphs, or, storage-retrieval structures of various kinds). This paper treats a problem that permeates the other work: How

The concept of reduction between problems is strengthened. Certain standard problems are shown to be complete in the new and stronger sense. Applications to the number of solutions of particular problems are presented.

Much of the research on semantic theories has concentrated on qualitative properties such as definability (of such programming concepts as recursive procedures), equivalence (of different language constructs), and verifiability (of the correctness, or consistency, of one expression relative to another). Current qualitative theories are in a tentative state and much remains to be done. However, there is also a quantitative side to semantics. Indeed, many of the questions which any semantic theory must answer are at once qualitative and quantitative. We would like to draw upon complexity-theoretic techniques to answer such questions. We are currently working on the development of new algebraic constructs to provide a mathematical framework for both qualitative and quantitative analysis of semantic problems.

It ~S shown how to determine membership in any parenthesis context-free language in log space As an apphcatton, the evaluation of Boolean sentences ~s shown to be log space computable Log space translatton of parenthesis languages ~s slmdarly shown to be possible, thus log space translators among various representations of Boolean formulas may be constructed

Let F be an arbitrary context-free grammar form and $\mathcal{G}(F)$ the family of grammars defined by F. For each grammar G in $\mathcal{G}(F)$, the derivation complexity function $\Phi _G$, on the language of G, is defined for each word x as the number of steps in a minimal G-derivation of x. It is shown that derivations may always be speeded up by any constant factor n, in the sense that for each positive integer n, an equivalent grammar $G'$ in $\mathcal{G}(F)$ can be found so that $\Phi _{G'} (x) \leqq | x | / n$ for all large words $x,| x |$ denoting the length of x.

Grammar forms are compared for their efficiency in representing languages, as measured by the sizes (i.e. total number of symbols, number of variable occurrences, number of productions, and number of distinct variables) of interpretation grammars. For every regular set, right- and left-linear forms are essentially equal in efficiency. Any form for the regular sets provides, at most, polynomial improvement over right-linear form. Moreover, any polynomial improvement is attained by some such form, at least on certain languages. Greater improvement for some languages is possible using forms expressing larger classes of languages than the regular sets. However, there are some languages for which no improvement over right-linear form is possible. While a similar set of results holds for forms expressing exactly the linear languages, only linear improvement can occur for forms expressing all the context-free languages.

The definition of “grammar form” introduced in [CG] makes it possible to state and prove results about various types of grammars in a uniform way. Among questions naturally formalizable in this framework are many about the complexity or efficiency of grammars of different kinds. Grammar forms provide a reasonable way of considering the totality of other forms we might use, and so answering the question with both upper and lower bound results.

Sets which are efficiently reducible (in Karp's sense) to arbitrarily complex sets are shown to be polynomial computable.Analogously, sets efficiently reducible to arbitrarily sparse sets are polynomial computable.A key lemma for both proofs shows that any set which is not polynomial computable has an infinite recursive subset of its domain, on which every algorithm runs slowly on almost all arguments.

Much recent work in the theory of computational complexity ([Me], [FR]. [SI]) is concerned with establishing “the complexity” of various recursive functions, as measured by the time or space requirements of Turing machines which compute them. In the above work, we also observe another phenomenon: knowing the values of certain functions makes certain other functions easier to compute than they would be without this knowledge. We could say that the auxiliary functions “help” the computation of the other functions. For example, we may conjecture that the “polynomial-complete” problems of Cook [C] and Karp [K] and Stockmeyer [S2], such as satisfiability of propositional formulas or 3-colorability of planar graphs, in fact require time proportional to nlog2n to be computed on a deterministic Turing machine. Then since the time required to decide if a planar graph with n nodes is 3-colorable can be lowered to a polynomial in n if we have a precomputed table of the satisfiable formulas in the propositional calculus, it is natural to say that the satisfiability problem “helps” the computation of the answers to the 3-coloring problem. Similar remarks may be made for any pair of polynomial-complete problems. As a further illustration, Meyer and Stockmeyer [MS] have shown that, for a certain alphabet Σ, recognition of the set of regular expressions with squaring which are equivalent to Σ* requires Turing machine space cn for some constant c, on an infinite set of arguments. We also know that this set of regular expressions, which we call RSQ, may actually be recognized in space dn for some other constant d. Theorem 6.2 in [LMF] implies that there is some problem (not necessarily an interesting one) of complexity approximately equal to that of RSQ, which does not reduce the complexity of RSQ below cn. It does not “help” the computation of RSQ.

Comparison of the polynomial-time-bounded reducibilities introduced by Cook [1] and Karp [4] leads naturally to the definition of several intermediate truth-table reducibilities. We give definitions and comparisons for these reducibilities; we note, in particular, that all reducibilities of this type which do not have obvious implication relationships are in fact distinct in a strong sense. Proofs are by simultaneous diagonalization and encoding constructions.Work of Meyer and Stockmeyer [7] and Gill [2] then leads us to define nondeterministic versions of all of our reducibilities. Although many of the definitions degenerate, comparison of the remaining nondeterministic reducibilities among themselves and with the corresponding deterministic reducibilities yields some interesting relationships.

This paper contains several results yielding pairs of problems which don't help each other's solution, and therefore which may be said to be complex for “different reasons.” Statements are formalized and results proved within Blum complexity theory, generalized to relative algorithms. The approach is fairly intuitive; all details appear in [1] and [2].