Abstract Information flow guided synthesis is a compositional approach to the automated construction of distributed systems where the assumptions between the components are captured as information-flow requirements. Information-flow requirements are hyperproperties that ensure that if a component needs to act on certain information that is only available in other components, then this information will be passed to the component. We present a new method for the automatic construction of information flow assumptions from specifications given as temporal safety properties. The new method is the first approach to handle situations where the required amount of information is unbounded. For example, we can analyze communication protocols that transmit a stream of messages in a potentially infinite loop. We show that component implementations can then, in principle, be constructed from the information flow requirements using a synthesis tool for hyperproperties. We additionally present a more practical synthesis technique that constructs the components using efficient methods for standard synthesis from trace properties. We have implemented the technique in the prototype tool FlowSy, which outperforms previous approaches to distributed synthesis on several benchmarks.

For common knowledge to arise in dynamic settings, all players must simultaneously come to know it has arisen. Consequently, common knowledge cannot arise in many realistic settings with timing frictions. This counterintuitive observation of Halpern and Moses (1990) was discussed by Arrow et al. (1987) and Aumann (1989), was called a paradox by Morris (2014), and has evaded satisfactory resolution for four decades. We resolve this paradox by proposing a new definition for common knowledge, which coincides with the traditional one in static settings but is more permissive in dynamic settings. Under our definition, common knowledge can arise without simultaneity, particularly in canonical examples of the Haplern-Moses paradox. We demonstrate its usefulness by deriving for it an agreement theorem à la Aumann (1976), showing it arises in the setting of Geanakoplos and Polemarchakis (1982) with timing frictions added, and applying it to characterize equilibrium behavior in a dynamic coordination game.

With the rapid increase in the size and volume of cloud services and data centers, architectures with multiple job dispatchers are quickly becoming the norm. Load balancing is a key element of such systems. Nevertheless, current solutions to load balancing in such systems admit a paradoxical behavior in which more accurate information regarding server queue lengths degrades performance due to herding and detrimental incast effects. Indeed, both in theory and in practice, there is a common doubt regarding the value of information in the context of multi-dispatcher load balancing. As a result, both researchers and system designers resort to more straightforward solutions, such as the power-of-two-choices to avoid worst-case scenarios, potentially sacrificing overall resource utilization and system performance. A principal focus of our investigation concerns the value of information about queue lengths in the multi-dispatcher setting. We argue that, at its core, load balancing with multiple dispatchers is a distributed computing task. In that light, we propose a new job dispatching approach, called Tidal Water Filling, which addresses the distributed nature of the system. Specifically, by incorporating the existence of other dispatchers into the decision-making process, our protocols outperform previous solutions in many scenarios. In particular, when the dispatchers have complete and accurate information regarding the server queues, our policies significantly outperform all existing solutions.

This paper provides a formal framework for reasoning about randomized distributed algorithms. We generalize the notion of indistinguishability, the most useful tool in deterministic lower bounds, to apply to a probabilistic setting. We use the new notion to prove a lower bound on the probability at which it can be guaranteed that honest parties will not decide on a possibly bogus value. Moreover, we show that the bound is tight by providing a protocol that matches the bound. This completely characterizes the quality of decisions that protocols for a randomized multi-valued Consensus problem can guarantee in an asynchronous environment with Byzantine faults.

Abstract Compositional synthesis relies on the discovery of assumptions, i.e., restrictions on the behavior of the remainder of the system that allow a component to realize its specification. In order to avoid losing valid solutions, these assumptions should benecessaryconditions for realizability. However, because there are typically many different behaviors that realize the same specification, necessary behavioral restrictions often do not exist. In this paper, we introduce a new class of assumptions for compositional synthesis, which we callinformation flow assumptions. Such assumptions capture an essential aspect of distributed computing, because components often need to act upon information that is available only in other components. The presence of a certain flow of information is therefore often a necessary requirement, while the actual behavior that establishes the information flow is unconstrained. In contrast to behavioral assumptions, which are properties of individual computation traces, information flow assumptions arehyperproperties, i.e., properties of sets of traces. We present a method for the automatic derivation of information-flow assumptions from a temporal logic specification of the system. We then provide a technique for the automatic synthesis of component implementations based on information flow assumptions. This provides a new compositional approach to the synthesis of distributed systems. We report on encouraging first experiments with the approach, carried out with theBoSyHypersynthesis tool.

This paper investigates how null messages can transfer information in fault-prone synchronous systems. The notion of an f-resilient message block is defined and is shown to capture the fundamental communication pattern for knowledge transfer. In general, this pattern combines both null messages and explicit messages. It thus provides a fault-tolerant extension of the classic notion of a message-chain. Based on the above, we provide tight necessary and sufficient characterizations of the generalized communication patterns that can serve to solve the distributed tasks of (nice-run) Signalling and Ordered Response.

Current-day data centers and high-volume cloud services employ a broad set of heterogeneous servers. In such settings, client requests typically arrive at multiple entry points, and dispatching them to servers is an urgent distributed systems problem. This paper presents an efficient solution to the load balancing problem in such systems that improves on and overcomes problems of previous solutions. The load balancing problem is formulated as a stochastic optimization problem, and an efficient algorithmic solution is obtained based on a subtle mathematical analysis of the problem. Finally, extensive evaluation of the solution on simulated data shows that it outperforms previous solutions. Moreover, the resulting dispatching policy can be computed very efficiently, making the solution practically viable.

Lower bounds and impossibility results in distributed computing are both intellectually challenging and practically important. Hundreds if not thousands of proofs appear in the literature, but surprisingly, the vast majority of them apply to deterministic algorithms only. Probabilistic protocols have been around for at least four decades and are receiving a lot of attention with the emergence of blockchain systems. Nonetheless, we are aware of only a handful of randomized lower bounds. In this work we provide a formal framework for reasoning about randomized distributed algorithms. We generalize the notion of indistinguishability, the most useful tool in deterministic lower bounds, to apply to a probabilistic setting. We apply this framework to prove a result of independent interest. Namely, we completely characterize the quality of decisions that protocols for a randomized multi-valued Consensus problem can guarantee in an asynchronous environment with Byzantine faults. We use the new notion to prove a lower bound on the guaranteed probability that honest parties will not decide on a possibly bogus value proposed by a malicious party. Finally, we show that the bound is tight by providing a protocol that matches it. This brief announcement consists of an introduction to the full paper [Guy Goren et al., 2020] by the same title. The interested reader is advised to consult the full paper for a detailed exposition.

In reliable settings, null messages allow the transfer of information without explicit communication in cases of interest. We investigate the use of null messages in the much more challenging Byzantine model (without signatures). Different ways of using null messages are discussed. One of them, called a silent validation round, can provide processes with global information about all correct sites of the system, without any message exchange. As a case study, we consider optimizing the behavior in failure-free runs of protocols for the classic Byzantine Consensus problem.

Whereas deterministic protocols are typically guaranteed to obtain particular goals of interest, probabilistic protocols typically provide only probabilistic guarantees. This paper initiates an investigation of the interdependence between actions and subjective beliefs of agents in a probabilistic setting. In particular, we study what probabilistic beliefs an agent should have when performing actions, in a protocol that satisfies a probabilistic constraint of the form: Condition ϕ should hold with probability at least p when action α is performed. Our main result is that the expected degree of an agent's belief in ϕ when it performs α equals the probability that ϕ holds when α is performed. Indeed, if the threshold of the probabilistic constraint should hold with probability p = 1 − ε2 for some small value of ε then, with probability 1 − ε, when the agent acts it will assign a probabilistic belief no smaller than 1 − ε to the possibility that ϕ holds. In other words, viewing strong belief as, intuitively, approximate knowledge, the agent must Probably Approximately Know (PAK-know) that ϕ is true when it acts.

With the rapid increase in the size and volume of cloud services and data centers, architectures with multiple job dispatchers are quickly becoming the norm. Load balancing is a key element of such systems. Nevertheless, current solutions to load balancing in such systems admit a paradoxical behavior in which more accurate information regarding server queue lengths degrades performance due to herding and detrimental incast effects. Indeed, both in theory and in practice, there is a common doubt regarding the value of information in the context of multi-dispatcher load balancing. As a result, both researchers and system designers resort to more straightforward solutions, such as the power-of-two-choices to avoid worst-case scenarios, potentially sacrificing overall resource utilization and system performance. A principal focus of our investigation concerns the value of information about queue lengths in the multi-dispatcher setting. We argue that, at its core, load balancing with multiple dispatchers is a distributed computing task. In that light, we propose a new job dispatching approach, called Tidal Water Filling, which addresses the distributed nature of the system. Specifically, by incorporating the existence of other dispatchers into the decision-making process, our protocols outperform previous solutions in many scenarios. In particular, when the dispatchers have complete and accurate information regarding the server queue lengths, our policies significantly outperform all existing solutions.

The cost of communication is a substantial factor affecting the scalability of many distributed applications. Every message sent can incur a cost in storage, computation, energy, and bandwidth. Consequently, reducing the communication costs of distributed applications is highly desirable. The best way to reduce message costs is by communicating without sending any messages whatsoever. This article initiates a rigorous investigation into the use of silence in synchronous settings, in which processes can fail. We formalize sufficient conditions for information transfer using silence, as well as necessary conditions for particular cases of interest. This allows us to identify message patterns that enable communication through silence. In particular, a pattern called a silent choir is identified, and shown to be central to information transfer via silence in failure-prone systems. The power of the new framework is demonstrated on the atomic commitment problem (AC). A complete characterization of the tradeoff between message complexity and round complexity in the synchronous model with crash failures is provided, in terms of lower bounds and matching protocols. In particular, a new message-optimal AC protocol is designed using silence, in which processes decide in three rounds in the common case. This significantly improves on the best previously known message-optimal AC protocol, in which decisions were performed in Θ( n ) rounds. And in the naked light I saw Ten thousand people, maybe more People talking without speaking … People writing songs that voices never share And no one dared Disturb the sound of silence Paul Simon, 1964

Distributed computations in a synchronous system prone to message loss can be modeled as a game between a (deterministic) distributed algorithm versus an omniscient message adversary. The latter determines, for each round, the directed communication graph that specifies which messages can reach their destination. Message adversary definitions range from oblivious ones, which pick the communication graphs arbitrarily from a given set of candidate graphs, to general message adversaries, which are specified by the set of sequences of communication graphs (called admissible communication patterns) that they may generate. This paper provides a complete characterization of consensus solvability for closed message adversaries, where every inadmissible communication pattern has a finite prefix that makes all (infinite) extensions of this prefix inadmissible. Whereas every oblivious message adversary is closed, there are also closed message adversaries that are not oblivious. We provide a tight non-topological, purely combinatorial characterization theorem, which reduces consensus solvability to a simple condition on prefixes of the communication patterns. Our result not only non-trivially generalizes the known combinatorial characterization of the consensus solvability for oblivious message adversaries by Coulouma, Godard, and Peters (Theor. Comput. Sci., 2015), but also provides the first combinatorial characterization for this important class of message adversaries that is formulated directly on the prefixes of the communication patterns.

Even in the absence of clocks, time bounds on the duration of actions enable the use of time for distributed coordination. This paper initiates an investigation of coordination in such a setting. A new communication structure called a zigzag pattern is introduced, and is shown to guarantee bounds on the relative timing of events in this clockless model. Indeed, zigzag patterns are shown to be necessary and sufficient for establishing that events occur in a manner that satisfies prescribed bounds. We capture when a process can know that an appropriate zigzag pattern exists, and use this to provide necessary and sufficient conditions for timed coordination of events using a full-information protocol in the clockless model.

Network configuration and policy updates occur frequently, and must be performed in a way that minimizes transient effects caused by intermediate states of the network. It has been shown that accurate time can be used for coordinating network-wide updates, thereby reducing temporary inconsistencies. However, this approach presents a great challenge; even if network devices have perfectly synchronized clocks, how can we guarantee that updates are performed at the exact time for which they were scheduled? In this paper, we present a practical method for implementing accurate time-based updates, using TimeFlips. A TimeFlip is a time-based update that is implemented using a timestamp field in a ternary content addressable memory (TCAM) entry. TimeFlips can be used to implement atomic bundle updates, and to coordinate network updates with high accuracy. We analyze the amount of TCAM resources required to encode a TimeFlip, and show that if there is enough flexibility in determining the scheduled time, a TimeFlip can be encoded by a single TCAM entry, using a single bit to represent the timestamp, while allowing a very high degree of accuracy.

With the rise of Software Defined Networks (SDN), there is growing interest in dynamic and centralized traffic engineering, where decisions about forwarding paths are taken dynamically from a network-wide perspective. Frequent path reconfiguration can significantly improve the network performance, but should be handled with care, so as to minimize disruptions that may occur during network updates. In this paper we introduce Time4, an approach that uses accurate time to coordinate network updates. We characterize a set of update scenarios called flow swaps, for which Time4 is the optimal update approach, yielding less packet loss than existing update approaches. We define the lossless flow allocation problem, and formally show that in environments with frequent path allocation, scenarios that require simultaneous changes at multiple network devices are inevitable. We present the design, implementation, and evaluation of a time4-enabled OpenFlow prototype. The prototype is publicly available as open source. Our work includes an extension to the OpenFlow protocol that has been adopted by the Open Networking Foundation (ONF), and is now included in OpenFlow 1.5. Our experimental results demonstrate the significant advantages of Time4 compared to other network update approaches.

This paper introduces OneClock, a generic approach for using time in networked applications. OneClock provides two basic time-triggered primitives: the ability to schedule an operation at a remote host or device, and the ability to receive feedback about the time at which an event occurred or an operation was executed at a remote host or device. We introduce a novel prediction-based scheduling approach that uses timing information collected at runtime to accurately schedule future operations. Our work includes an extension to the Network Configuration protocol (NETCONF), which enables OneClock in real-life systems. This extension has been published as an Internet Engineering Task Force (IETF) RFC, and a prototype of our NETCONF time extension is publicly available as open source. Experimental evaluation shows that our prediction-based approach allows accurate scheduling in diverse and heterogeneous environments, with various hardware capabilities and workloads. OneClock is a generic approach that can be applied to any managed device: sensors, actuators, Internet of Things (IoT) devices, routers, or toasters.

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

With the rise of software defined networks (SDNs), there is a growing interest in dynamic and centralized traffic engineering, where decisions about forwarding paths are taken dynamically from a network-wide perspective. Frequent path reconfiguration can significantly improve the network performance, but should be handled with care soas to minimize disruptions that may occur during network updates. Network updates are especially challenging when the network is heavily utilized; some of the existing approaches suggest that spare capacity should be reserved in the network in order to allow updates in such scenarios, or that the network load should be temporarily reduced prior to a network update. In this paper, we introduce Time4, an approach that uses accurate time to coordinate network updates. Time4 is a powerful tool in softwarized environments that can be used for various network update scenarios, including in heavily utilized networks. Specifically, we characterize a set of update scenarios called flow swaps, for which Time4 is the optimal update approach, yielding less packet loss than existing update approaches without requiring spare capacity, and without temporarily reducing the network's bandwidth. We define the lossless flow allocation problem, and formally show that in environments with frequent path allocation, scenarios that require simultaneous changes at multiple network devices are inevitable. We present the design, implementation, and evaluation of a Time4-enabled OpenFlow prototype. The prototype is publicly available as open source. This paper includes an extension to the OpenFlow protocol that has been adopted by the open networking foundation, and is now included in OpenFlow 1.5. Our experimental results show the significant advantages of Time4 compared to other network update approaches, and demonstrate an SDN use case that is infeasible without Time4. Our experimental results demonstrate the significant advantages of Time4 compared to other network update approaches.

Network updates, such as policy and routing changes, occur frequently in software-defined networks (SDNs). Updates should be performed consistently, preventing temporary disruptions, and should require as little overhead as possible. Scalability is increasingly becoming an essential requirement in SDNs. In this paper, we propose to use time-triggered network updates to achieve consistent updates. Our proposed solution requires lower overhead than the existing update approaches, without compromising the consistency during the update. We demonstrate that accurate time enables far more scalable consistent updates in the SDN than previously available. In addition, it provides the SDN programmer with fine-grained control over the tradeoff between consistency and scalability.

Network configuration and policy updates occur frequently, and must be performed in a way that minimizes transient effects caused by intermediate states of the network. It has been shown that accurate time can be used for coordinating network-wide updates, thereby reducing temporary inconsistencies. However, this approach presents a great challenge; even if network devices have perfectly synchronized clocks, how can we guarantee that updates are performed at the exact time for which they were scheduled? In this paper we present a practical method for implementing accurate time-based updates, using TIMEFLIPs. A TimeFlip is a time-based update that is implemented using a timestamp field in a Ternary Content Addressable Memory (TCAM) entry. TIMEFLIPs can be used to implement Atomic Bundle updates, and to coordinate network updates with high accuracy. We analyze the amount of TCAM resources required to encode a TimeFlip, and show that if there is enough flexibility in determining the scheduled time, a TimeFlip can be encoded by a single TCAM entry, using a single bit to represent the timestamp, and allowing the update to be performed with an accuracy on the order of 1 microsecond.

The coordination of a sequence of actions, to be performed in a linear temporal order in a distributed system, is studied. While in asynchronous message-passing systems such ordering of events requires the construction of message chains based on Lamport's happened-before relation, this is no longer true in the presence of time bounds on message delivery. Given such bounds, the mere passage of time can provide information about the occurrence of events at remote sites, without the need for explicit confirmation. A new causal structure called the centipede is introduced, and it is shown that centipedes must exist in every execution where linear ordering of actions is ensured. Centipedes capture the subtle interplay between the explicit information obtained via message chains, and the indirectly derived information gained by the passage of time, given the time bounds. Centipedes are defined using two relations. One is called syncausality, a slight generalisation of the happened-before relation. The other is a novel bound guarantee relation among events, that is based on the bounds on message transmission. In a precise sense, centipedes play a role in the synchronous setting analogous to that played by message chains in asynchronous systems. Our study is based on a knowledge-based analysis of distributed coordination. Temporally linear coordination is reduced to nested knowledge (knowledge about knowledge). Obtaining nested knowledge of a spontaneous event is, in turn, shown to require the existence of an appropriate centipede.

We show how game-theoretic solution concepts such as Nash equilibrium, correlated equilibrium, rationalizability, and sequential equilibrium can be given a uniform definition in terms of a knowledge-based program with counterfactual semantics. In a precise sense, this program can be viewed as providing a procedural characterization of rationality.

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

Consider a fully connected network where up to t processes may crash and all processes start in an arbitrary memory state. The self-stabilizing firing squad problem consists of eventually guaranteeing simultaneous response to an external input. This is modeled by requiring that the noncrashed processes “fire” simultaneously if some correct process received an external “go” input, and that they only fire as a response to some process receiving such an input. This paper presents FireSquad, the first self-stabilizing firing squad algorithm. A firing squad algorithm facilitates the use of algorithms that need to start in the same round. It allows a smooth transition between algorithms whose executions need to be disjoint. The FireSquad algorithm combines two forms of fault-tolerance properties: self-stabilization to allow recovery from arbitrary transient errors and resilience to crash failures to handle permanent ones. The FireSquad algorithm is optimal in two respects: (a) once the algorithm is in a safe state, it fires in response to a go input as fast as any other algorithm does, and (b) starting from an arbitrary state, it converges to a safe state as fast as any other algorithm does.

Decision tasks require that nonfaulty processes make decisions based on their input values. Simultaneous decision tasks require that nonfaulty processes decide in the same round. Most decision tasks have known worst-case lower bounds. Most also have known worst-case optimal protocols that halt in the number of rounds given by the worst-case lower bound, and some have early-stopping protocols that can halt earlier than the worst-case lower bound (sometimes in as early as two rounds). We consider what might be called earliest-possible protocols for simultaneous decision tasks. We present a new technique that converts worst-case optimal decision protocols into all-case optimal simultaneous decision protocols: For every behavior of the adversary, the all-case optimal protocol decides as soon as any protocol can decide in a run with the same adversarial behavior. Examples to which this can be applied include set consensus, condition-based consensus, renaming and order-preserving renaming. Some of these tasks can be solved significantly faster than the classical simultaneous consensus task. A byproduct of the analysis is a proof that improving on the worst-case bound for any simultaneous task by even a single round is as hard as reaching simultaneous consensus.

We study several variants of coordinated consensus in dynamic networks. We assume a synchronous model, where the communication graph for each round is chosen by a worst-case adversary. The network topology is always connected, but can change completely from one round to the next. The model captures mobile and wireless networks, where communication can be unpredictable.

This paper studies the role that known bounds on message transmission times in a computer network play on the evolution of the epistemic state over time. A connection to cones of causal influence analogous to, and more general than, light cones is presented. Focusing on lower bounds on message transmission times, an analysis is presented of how knowledge about when others are guaranteed to be ignorant about an event of interest ("knowing that they don't know") can arise. This has implications in competitive settings, in which knowing about another's ignorance can provide an advantage.

This paper introduces a simple notion of layering as a tool for analyzing well-behaved runs of a given model of distributed computation. Using layering, a model-independent analysis of the consensus problem is performed and then applied to proving lower bounds and impossibility results for consensus in a number of familiar and less familiar models. The proofs are simpler and more direct than existing ones, and they expose a unified structure to the difficulty of reaching consensus. In particular, the proofs for the classical synchronous and asynchronous models now follow the same outline. A new notion of connectivity among states in runs of a consensus protocol, called potence connectivity, is introduced. This notion is more general than previous notions of connectivity used for this purpose and plays a keyrole in the uniform analysis of consensus.

We investigate eventual Byzantine agreement (EBA) in the crash and omission failure modes. The emphasis is on characterizing optimal EBA protocols in terms of the states of knowledge required by the processors in order to attain EBA. It is well known that common knowledge among the nonfaulty processors is a necessary and sufficient condition for attaining simultaneous Byzantine agreement (SBA). We define a new variant that we call continual common knowledge and use it to provide necessary and sufficient conditions for attaining EBA. Using this characterization, we provide a technique that allows us to start with any EBA protocol and convert it to an optimal EBA protocol using a two-step process.

We introduce a simple notion of layering that provides a tool for defining submodels of a given model of distributed computation.We describe two layerings, the synchronic and the permutation layering, and show that they induce appropriate submodels of several asynchronous models of computation.The synchronic layering applies to the synchronous model too.We perform a model-independent analysis of the consensus problem in terms of abstract connectivity properties of layering functions.By defining particular layerings in specific models, we derive several popular (and some new) lower bounds and impossibility results for consensus in various classical models.These results are often stronger in the sense that they apply to the subrnodel induced by the layering.The proofs obtained in this way are also simpler and more direct than existing ones.Moreover, the analysis is done in a uniform fashion and demonstrates the fundamental common structure of the consensus problem in the presence of failures.The analysis is then extended to general decision problems (l-resilient in the asynchronous models, t-rounds in the t-resilient synchronous model), providing a characterization of solvability of decision problems in the style of [8] which, for some of the models, is given for the first time.1 introduction For almost two decades now, the consensus problem has played a central role in the study of fault-tolerant distributed computing, e.g.123, 13, 12, 10, 14, 20, 16, 8, 91.It has clearly received the greatest amount of attention in the theoretical literature on distributed computing, and has been studied in a large variety of models and under many types of failure assumptions.Work on different variants often in-*This work has been supported by a Helen and Milton A. Kimmelman career development chair.

This paper presents a polynomial-time protocol for reaching Byzantine agreement in t + 1 rounds whenever n > 3t, where n is the number of processors and t is an a priori upper bound on the number of failures. This resolves an open problem presented by Pease, Shostak, and Lamport in 1980. An early-stopping variant of this protocol is also presented, reaching agreement in a number of rounds that is proportional to the number of processors that actually fail.

Inspired by the success of the distributed computing community in apply logics of knowledge and time to reasoning about distributed protocols, we aim for a similarly powerful and high-level abstraction when reasoning about control problems involving uncertainty. This paper concentrates on robot motion planning with uncertainty in both control and sensing, a problem that has already been well studied within the robotics community. First, a new and natural problem in this domain is defined: does there exists a sound and complete termination condition for a motion, given initial and goal locations? If yes, how to construct it? Then we define a high-level language, a logic of time and knowledge, which we use to reason about termination conditions and to state general conditions for the existence of sound and complete termination conditions in a broad domain. Finally, we show that sound termination conditions that are optimal in a precise sense provide a natural example of knowledge-based programs with multiple implementations.

Reasoning about activities in a distributed computer system at the level of the knowledge of individuals and groups allows us to abstract away from many concrete details of the system we are considering. In this paper, we make use of two notions introduced in our recent book to facilitate designing and reasoning about systems in terms of knowledge. The first notion is that of a knowledge-based program. A knowledge-based program is a syntactic object: a program with tests for knowledge. The second notion is that of a context, which captures the setting in which a program is to be executed. In a given context, a standard program (one without tests for knowledge) is represented by (i.e., corresponds in a precise sense to) a unique system. A knowledge-based program, on the other hand, may be represented by no system, one system, or many systems. In this paper, we provide a sufficient condition for a knowledge-based program to be represented in a unique way in a given context. This condit...

This paper introduces a framework for knowledgebased analysis of issues of timing and clocks in sys-

This paper presents knowledge-oriented programming, a framework for giving high-level knowledgebased descriptions of distributed protocols.We extend the notion of knowledge-based programs of [FHMV93] by allowing high-level actions that are defined in terms of changing the state of knowledge of processes in the system.As a result, both the choice of which actions to perform and the actions themselves are defined explicitly in terms of the processes' knowledge.We concentrate on a class of high-level notify actions that can be used to abstract away details of communication.Examples are considered, including solutions to the atomic commitment problem and to the sequence transmission problem.

This paper presents a polynomial protocol for reaching Byzantine agreement in t + 1 rounds whenever n > 3t, where n is the number of processors and t is an a priori upper bound on the number of failures.This resolves an open problem presented by Pease, Shostak and Lamport ir 1980.

We investigate eventual Byzantine agreement (EBA) in the crash and omission failure models.The emphasis is on characterizing optimal EBA protocols in terms of the states of knowledge required by the processors in order to attain EBA.It is well known that common knowledge among the nonfaulty processors is a necessary and sufficient condition for attaining simultaneous Byzantine agreement (SBA).We define a new variant of common knowledge, which we call continual common knowledge, in terms of which we can characterize necessary and sufficient conditions for attaining EBA.Using our characterization, we provide a technique that allows us to start with any EBA protocol, apply a certain construction twice, and arrive at an optimal EBA protocol.

Processes in concurrent logic programs communicate and synchronize using shared singleassignment variables.Communication is performed via unification operations, while synchronization is performed through input matching.The more expressive concurrent logic languages employ atomic unification as the basic communication primitive.Atomic unification can be thought of as an atomic transaction that either fails with no trace or succeeds in writing on all of the necessary writable variables occurring in the unification instance.This pa- per presents a distributed variable server algorithm that can be used as the key component in a distributed implementation of concurrent logic languages with atomic unification.The variable server provides an abstraction in which processes can act as if all of the shared variables are local.It thus allows programs to be written for a shared memory model and executed in a system in which memory is distributed.We rigorously specify the requirements the variable server must fulfill, present an algorithm satisfying the specification, and prove its correctness with respect to the specification.The algorithm has been implemented for the language Flat Concurrent Prolog (FCP) and is incorporated in the distributed version of the Logix system.

Reasoning about knowledge seems to play a fundamental role in distributed systems. Indeed, such reasoning is a central part of the informal intuitive arguments used in the design of distributed protocols. Communication in a distributed system can be viewed as the act of transforming the system's state of knowledge. This paper presents a general framework for formalizing and reasoning about knowledge in distributed systems. It is shown that states of knowledge of groups of processors are useful concepts for the design and analysis of distributed protocols. In particular, distributed knowledge corresponds to knowledge that is “distributed” among the members of the group, while common knowledge corresponds to a fact being “publicly known.” The relationship between common knowledge and a variety of desirable actions in a distributed system is illustrated. Furthermore, it is shown that, formally speaking, in practical systems common knowledge cannot be attained. A number of weaker variants of common knowledge that are attainable in many cases of interest are introduced and investigated.

Article On reliable message diffusion Share on Authors: Y. Moses Department of Computer Science, The Weiemann Institute, Rehovot, 76100 Israel Department of Computer Science, The Weiemann Institute, Rehovot, 76100 IsraelView Profile , G. Roth Department of Computer Science, The Weiemann Institute, Rehovot, 76100 Israel Department of Computer Science, The Weiemann Institute, Rehovot, 76100 IsraelView Profile Authors Info & Claims PODC '89: Proceedings of the eighth annual ACM Symposium on Principles of distributed computingJune 1989 Pages 119–127https://doi.org/10.1145/72981.72989Online:01 June 1989Publication History 9citation199DownloadsMetricsTotal Citations9Total Downloads199Last 12 Months6Last 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 SiteGet Access

The problem of efficiently performing Byzantine agreement in t+1 rounds in the face of arbitrarily malicious failures is treated. A communication-efficient polynomial-time protocol is presented for n>8t. The protocol is an early stopping protocol, halting in min(t+1, f+2) rounds in the worst case, where f is the number of processors that fail during the run. This is provably optimal. The protocol is based on a careful combination of early stopping, fault masking, and a technique called coordinated traversal. The combination of the three provides a powerful method for restricting the damage that a faulty processor, however malicious, can do. One of the byproducts of this protocol is a polynomial-time (t+1)-round protocol for the Byzantine firing squad problem.>

While the intuition underlying a zero knowledge proof system [GMR85] is that no “knowledge” is leaked by the prover to the verifier, researchers are just beginning to analyze such proof systems in terms of formal notions of knowledge. In this paper, we show how interactive proof systems motivate a new notion of practical knowledge, and we capture the definition of an interactive proof system in terms of practical knowledge. Using this notion of knowledge, we formally capture and prove the intuition that the prover does not leak any knowledge of any fact (other than the fact being proven) during a zero knowledge proof. We extend this result to show that the prover does not leak any knowledge of how to compute any information (such as the factorization of a number) during a zero knowledge proof. Finally, we define the notion of a weak interactive proof in which the prover is limited to probabilistic, polynomial-time computations, and we prove analogous security results for such proof systems. We show that, in a precise sense, any nontrivial weak interactive proof must be a proof about the prover's knowledge, and show that, under natural conditions, the notions of interactive proofs of knowledge defined in [TW87] and [FFS87] are instances of weak interactive proofs.

This work applies the theory of knowledge in distributed systems to the design of faulttolerant protocols for problems involving coordinated simultaneous actions in synchronous systems. We give a simple method for transforming specifications of such problems into high-level protocols programmed using explicit tests of whether certain facts are common knowledge. The resulting protocols are optimal in all runs: for every possible input to system and pattern of processor failures, they are guaranteed to perform the simultaneous actions as soon as any other protocol can possibly perform them. A careful analysis of when facts become common knowledge shows how to efficiently implement these protocols in many variants of the omissions failure model. In the generalized omissions model, however, it is shown that any protocol that is optimal in this sense must require co-NP hard computations. The analysis in this paper exposes subtle differences between the failure models, including the precise point at which this gap in complexity occurs.

By looking at a number of variants of the clteatir~g Itusbcads puzzle, we illustrate the subtle relationship between knowledge, communication, and action in a distributed environment.

We argue that the right way to understand distributed protocols is by considering how messages change the state of knowledge of a system. We present a hierarchy of knowledge states that a system may be in, and discuss how communication can move the system's state of knowledge of a fact up the hierarchy. Of special interest is the notion of common knowledge. Common knowledge is an essential state of knowledge for reaching agreements and coordinating action. We show that in practical distributed systems, common knowledge is not attainable. We introduce various relaxations of common knowledge that are attainable in many cases of interest. We describe in what sense these notions are appropriate, and discuss their relationship to each other. We conclude with a discussion of the role of knowledge in distributed systems.