A liveness contract is an agreement between the specifier of a system and a task to solve, and the programmer who makes her living by delivering protocols. In a shared-memory system, a liveness contract specifies infinite suffixes of executions in which the programmer is required to solve a distributed task. If the behavior of the system does not comply with the specification, no output is required. A convenient way to describe a large class of liveness contracts was recently proposed by Delporte et al. For a system ∏ of n processes, an adversary is a set A of subsets of ∏. The system is required to make progress only in executions in which the set of correct processes is in A. Given an adversary A and a task T, should the programmer sign the contract? Can she deliver? In this paper, we give a very simple resolution of this question for colorless tasks that contrasts with more involved arguments of the original paper of Delpote et al. More importantly, our resolution is constructive - it tells the programmer how to use A to solve T, when it is solvable. Our framework naturally generalizes to systems enriched with more powerful objects than read-write registers. We determine necessary and sufficient conditions for an adversary A to solve consensus using j-process consensus objects and read-write registers, which resolves an open question raised recently by Taubenfeld.
展开▼
