Reliable Contracts for Unreliable Half-Duplex Communications

Etienne Lozes, ENS de Cachan, France

Unreliable communications are commonplace in real programming languages, as illustrated e.g. by UDP communications, but they are poorly addressed by concurrency models for which the theory of contracts (aka session behaviours) have been studied. We show how to use contracts for unreliable communications, parametrized by a flexible model of errors (message loss, out-of-order, urgent messages,...), which gives a new perspective on the role and foundations of contracts. Our claim is indeed that the fundamental property ensured by contracts is that communications are half-duplex, and that other better-studied properties (progress and buffer boundedness) come almost for free afterwards.