Causing communication closure: safe program composition with reliable non-FIFO channels

摘要

A rigorous framework for analyzing safe composition of distributed programs is presented. It facilitates specifying notions of safe sequential execution of distributed programs in various models of communication. A notion of 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. None of its send or receive actions will match or interact with actions outside P. The applicability of sealing 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. In this model no program that sends or receives messages can be composed automatically with arbitrary programs without jeopardizing their intended behavior. Safety of composition becomes context-sensitive and new tools are needed for ensuring it. 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 class of straight-line programs. It is shown that every sealable program can be sealed using O(n) messages. In fact, 3n - 4 messages are necessary and sufficient in the worst case, despite the fact that a sealable program may be open to interference on Ω (n~2) channels.