Knowledge and Inhibition in Asynchronous Distributed Systems

Abstract

In an asynchronous distributed system, processes communicate only via message passing along channels with unbounded transmission time. Relative process speeds are arbitrary and processes do not have access to a common clock. For such systems, a useful means of providing temporal structure is the causality relation. Causality imposes a partial order on the events of an execution based on the necessity of certain events preceding other events. Causality can be used to give a sensible definition of a distributed global state in an asynchronous system, known as a consistent cut. We present a new knowledge-theoretic logic, with formal semantic definitions, for reasoning about causality and consistent cuts. The logic includes concurrent common knowledge, a new form of distributed agreement, which has an analogous role to that of common knowledge in synchronous systems. It is shown to be a necessary and sufficient condition for performing concurrent actions in asynchronous systems, and has a role in many distributed applications such as checkpointing, deadlock detection, and broadcasting. Concurrent common knowledge is also shown to be attainable by class of protocols termed distinguishable-consistent-cut-protocols or DCCPs. We examine four simple and efficient DCCPs and trade-offs between them. These trade-offs involve message complexities, necessity of FIFO channels, and the degrees to which events of the underlying system are suspended during execution of the protocols. We call such suspensions inhibition and formally define multiple forms of inhibition that are used in distributed protocols. We classify the DCCPs in this work according to their inhibitory characteristics, and prove new results which demonstrate close relationships between inhibition and the existence of DCCPs.