## Newtonian Arbiters Cannot be Proven Correct

**Michael Mendler and Terry Stroup**
*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.

*Abridged version to appear in* Proceedings of the 2nd IFIP
WG10.5/WG10.2 Workshop on Designing Correct Circuits *J.
Staunstrup and R. Sharp editors.*

*LFCS report ECS-LFCS-92-252,
December 1992.*

Previous |

Index |

Next