Newtonian arbiters cannot be proven correct
Michael Mendler, Terry Stroup · Formal Methods in System Design · 1993
Abstrlld.Computing hardware is designed by refining an abstract specification through various lower levels of abstraction to arme ar a tranmtor Jayout implCJ11en1ed in a physic:al medium.Fomalizing the reftnements-one taslc of the mathematical aemantics of computation-involves proving that the dc:vioe described at eadr Jevel of abstraction does indeed bohave as prescribed by thc dcscriptlon at lhe nm higher lcvcl.Onc obstacle to this goal that has long been recognized is thal certain dasses of behaviors can bc physic:a!lyrealizcd only approximately.Thc notorious prob!em of metastable operation predudes, for example, lhe rcalization on classical principlcs of fllpftops that react in bounded time to arbitrary input signals.The litcrature suggests that lbe dißicully lies ultimatcly in thc specification 's requiring that thc realizing device react propcrly in bounded time.We show, howcver, that a simplc•time""llboundod synchronization problcm, namely, mutual exc!usion by means of an arbitcr, cannot bc solved with perfect reliabilily using oontinllOUs, i.e~ Newtonian, physica!phenomena.In particular, for any physic:al device operating on Ncwtonian principles !hat satisfics specific assumptions c:onceming an arbitcr's input-output bchavior, therc always cxist compcting requcsts to which il re8Cl5 by granting them all.