Towards the Unification of the Functional and Performance Analysis of Protocols or, Is the Alternating-Bit Protocol Really Correct?

In the past 15 years the alternating-bit protocol has been perhaps the most widely verified protocol, the benchmark of protocol verification techniques; is it really correct? We claim that the answer is negative. The problem is that existing concepts of correctness do not capture an important sense in which a protocol may be incorrect. Specifically, although protocol goals (e.g., delivering messages) may be attained eventually, the time periods to achieve these goals may increase indefinitely. A notion of correctness which allows one to consider both the probability of reaching a goal as well as the time or computational effort required to achieve the goal is required. We present a novel approach to protocol correctness which unifies functional and performance considerations using a recently proposed probabilistic semantics for programs