Newtonian Arbiters Cannot be Proven Correct

From bibtex.

Abstract

Computing hardware is designed by refining an abstract specification through various lower levels of abstraction to arrive at a transistor layout implemented in a physical medium. Formalizing the refinements—one task of the mathematical semantics of computation—involves proving that the device described at each level of abstraction does indeed behave as prescribed by the description at the next higher level. One obstacle to this goal that has long been recognized is that certain classes of behaviors can be physically realized only approximately. The notorious problem of metastable operation precludes, for example, the realization on classical principles of flipflops that react in bounded time to arbitrary input signals. The literature suggests that the difficulty lies ultimately in the specification's requiring that the realizing device react properly in bounded time. We show, however, that a simple-time-unbounded synchronization problem, namely, mutual exclusion by means of an arbiter, cannot be solved with perfect reliability using continuous, i.e., Newtonian, physical phenomena. In particular, for any physical device operating on Newtonian principles that satisfies specific assumptions concerning an arbiter's input-output behavior, there always exist competing requests to which it reacts by granting them all.