Searcharxiv⌕ Search

arXiv subjects

Yoram Moses

Publications and source records attributed to Yoram Moses.

35 records · Page 2Linked to original sources
arXiv2016

Unbeatable Set Consensus via Topological and Combinatorial Reasoning

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.

cs.DC↗
arXiv2016

The Case for Data Plane Timestamping in SDN

This paper presents the case for Data Plane Timestamping (DPT). We argue that in the unique environment of Software-Defined Networks (SDN), attaching a timestamp to the header of all packets is a powerful feature that can be leveraged by various diverse SDN applications. We analyze three key use cases that demonstrate the advantages of using DPT, and show that SDN applications can benefit even from using as little as one bit for the timestamp field.

cs.NI↗
arXiv2016

Time4: Time for SDN

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. Time4 is a powerful tool in softwarized environments, that can be used for various network update scenarios. 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. 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 show the significant advantages of Time4 compared to other network update approaches, and demonstrate an SDN use case that is infeasible without Time4.

cs.NI↗
arXiv2016

OneClock to Rule Them All: Using Time in Networked Applications

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.

cs.NI↗
arXiv2015

Timed Consistent Network Updates

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

cs.NI↗
arXiv2014

Unbeatable Consensus

The unbeatability of a consensus protocol, introduced by Halpern, Moses and Waarts in 2001, is a stronger notion of optimality than the accepted notion of early stopping protocols. Using a novel knowledge-based analysis, this paper derives the first practical unbeatable consensus protocols in the literature, for the standard synchronous message-passing model with crash failures. These protocols strictly dominate the best known protocols for uniform and for non-uniform consensus, in some case beating them by a large margin. The analysis provides a new understanding of the logical structure of consensus, and of the distinction between uniform and nonuniform consensus. Finally, the first (early stopping and) unbeatable protocol that treats decision values "fairly" is presented. All of these protocols have very concise descriptions, and are shown to be efficiently implementable.

cs.DC↗
arXiv2013

Good, Better, Best! - Unbeatable Protocols for Consensus and Set Consensus

While the very first consensus protocols for the synchronous model were designed to match the worst-case lower bound, deciding in exactly t+1 rounds in all runs, it was soon realized that they could be strictly improved upon by early stopping protocols. These dominate the first ones, by always deciding in at most t+1 rounds, but often much faster. A protocol is unbeatable if it can't be strictly dominated. Unbeatability is often a much more suitable notion of optimality for distributed protocols than worst-case performance. Using a knowledge-based analysis, this paper studies unbeatability for both consensus and k-set consensus. We present unbeatable solutions to non-uniform consensus and k-set consensus, and uniform consensus in synchronous message-passing contexts with crash failures. The k-set consensus problem is much more technically challenging than consensus, and its analysis has triggered the development of the topological approach to distributed computing. Worst-case lower bounds for this problem have required either techniques based on algebraic topology, or reduction-based proofs. Our proof of unbeatability is purely combinatorial, and is a direct, albeit nontrivial, generalization of the one for consensus. We also present an alternative topological unbeatability proof that allows to understand the connection between the connectivity of protocol complexes and the decision time of processes. For the synchronous model, only solutions to the uniform variant of k-set consensus have been offered. Based on our unbeatable protocols for uniform consensus and for non-uniform k-set consensus, we present a uniform k-set consensus protocol that strictly dominates all known solutions to this problem in the synchronous model.

cs.DC↗
arXiv2013

The Shape of Reactive Coordination Tasks

This paper studies the interaction between knowledge, time and coordination in systems in which timing information is available. Necessary conditions are given for the causal structure in coordination problems consisting of orchestrating a set of actions in a manner that satisfies a variety of temporal ordering assumptions. Results are obtained in two main steps: A specification of coordination is shown to require epistemic properties, and the causal structure required to obtain these properties is characterised via "knowledge gain" theorems. A new causal structure called a centibroom structure is presented, generalising previous causal structures for this model. It is shown to capture coordination tasks in which a sequence of clusters of events is performed in linear order, while within each cluster all actions must take place simultaneously. This form of coordination is shown to require the agents to gain a nested common knowledge of particular facts, which in turn requires a centibroom. Altogether, the results presented provide a broad view of the causal shape underlying partially ordered coordinated actions. This, in turn, provides insight into and can enable the design of efficient solutions to the coordination tasks in question.

cs.LO↗
arXiv2013

Timely Common Knowledge

Coordinating activities at different sites of a multi-agent system typically imposes epistemic constraints on the participants. Specifying explicit bounds on the relative times at which actions are performed induces combined temporal and epistemic constraints on when agents can perform their actions. This paper characterises the interactive epistemic state that arises when actions must meet particular temporal constraints. The new state, called timely common knowledge, generalizes common knowledge, as well as other variants of common knowledge. While known variants of common knowledge are defined in terms of a fixed point of an epistemic formula, timely common knowledge is defined in terms of a vectorial fixed point of temporal-epistemic formulae. A general class of coordination tasks with timing constraints is defined, and timely common knowledge is used to characterise both solvability and optimal solutions of such tasks. Moreover, it is shown that under natural conditions, timely common knowledge is equivalent to an infinite conjunction of temporal-epistemic formulae, in analogy to the popular definition of common knowledge.

cs.LO↗
arXiv2013

A Knowledge-based Treatment of Human-Automation Systems

In a supervisory control system the human agent knowledge of past, current, and future system behavior is critical for system performance. Being able to reason about that knowledge in a precise and structured manner is central to effective system design. In this paper we introduce the application of a well-established formal approach to reasoning about knowledge to the modeling and analysis of complex human-automation systems. An intuitive notion of knowledge in human-automation systems is sketched and then cast as a formal model. We present a case study in which the approach is used to model and reason about a classic problem from the human-automation systems literature; the results of our analysis provide evidence for the validity and value of reasoning about complex systems in terms of the knowledge of the system agents. To conclude, we discuss research directions that will extend this approach, and note several systems in the aviation and human-robot team domains that are of particular interest.

cs.HC↗
arXiv2012

Agent-time Epistemics and Coordination

A minor change to the standard epistemic logical language, replacing $K_{i}$ with $K_{\node{i,t}}$ where $t$ is a time instance, gives rise to a generalized and more expressive form of knowledge and common knowledge operators. We investigate the communication structures that are necessary for such generalized epistemic states to arise, and the inter-agent coordination tasks that require such knowledge. Previous work has established a relation between linear event ordering and nested knowledge, and between simultaneous event occurrences and common knowledge. In the new, extended, formalism, epistemic necessity is decoupled from temporal necessity. Nested knowledge and event ordering are shown to be related even when the nesting order does not match the temporal order of occurrence. The generalized form of common knowledge does {\em not} correspond to simultaneity. Rather, it corresponds to a notion of tight coordination, of which simultaneity is an instance.

cs.MA↗
arXiv2009

An Optimal Self-Stabilizing Firing Squad

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 non-crashed 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 FireAlg, the first self-stabilizing firing squad algorithm. The FireAlg 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.

cs.DC↗
arXiv2007

Causing Communication Closure: Safe Program Composition with Reliable Non-FIFO Channels

A semantic framework for analyzing safe composition of distributed programs is presented. Its applicability is illustrated by a study of program composition when communication is reliable but not necessarily FIFO\@. In this model, special care must be taken to ensure that messages do not accidentally overtake one another in the composed program. We show that barriers do not exist in this model. Indeed, no program that sends or receives messages can automatically be composed with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. A notion of \emph{sealing} is defined, where if a program $P$ is immediately followed by a program $Q$ that seals $P$ then $P$ will be communication-closed--it will execute as if it runs in isolation. The investigation of sealing in this model reveals a novel connection between Lamport causality and safe composition. A characterization of sealable programs is given, as well as efficient algorithms for testing if $Q$ seals $P$ and for constructing a seal for a significant class of programs. It is shown that every sealable program that is open to interference on $O(n^2)$ channels can be sealed using O(n) messages.

cs.DC↗
arXiv2006

Characterizing Solution Concepts in Games Using Knowledge-Based Programs

We show how solution concepts in games such as Nash equilibrium, correlated equilibrium, rationalizability, and sequential equilibrium can be given a uniform definition in terms of \emph{knowledge-based programs}. Intuitively, all solution concepts are implementations of two knowledge-based programs, one appropriate for games represented in normal form, the other for games represented in extensive form. These knowledge-based programs can be viewed as embodying rationality. The representation works even if (a) information sets do not capture an agent's knowledge, (b) uncertainty is not represented by probability, or (c) the underlying game is not common knowledge.

cs.GT↗
arXiv2003

Using Counterfactuals in Knowledge-Based Programming

This paper adds counterfactuals to the framework of knowledge-based programs of Fagin, Halpern, Moses, and Vardi. The use of counterfactuals is illustrated by designing a protocol in which an agent stops sending messages once it knows that it is safe to do so. Such behavior is difficult to capture in the original framework because it involves reasoning about counterfactual executions, including ones that are not consistent with the protocol. Attempts to formalize these notions without counterfactuals are shown to lead to rather counterintuitive behavior.

cs.DC↗
arXiv2000

Knowledge and common knowledge in a distributed environment

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. We argue 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.

cs.DC↗