Open Collections

Proving Newtonian Arbiters Correct, almost surely

University of British Columbia

An arbiter is a circuit that grants its clients mutually exclusive access to a shared resource. The ideal arbiter cannot be built—either requests must occur synchronously, mutual exclusion is not guaranteed, or the arbiter may become hung indefinitely and fail to make a decision. This thesis explores arbiters whose failure mode is the latter; they are not live. Two specific arbiters are investigated: a "toy" arbiter, whose model was chosen for its .tractability; and Seitz's nMOS interlock, which was chosen as an example of a widely used and studied design. Both arbiters are modeled by nonlinear continuous dynamic systems, and both models are Newtonian: given an initial set of system states, the future image of that set has exactly the same dimension. The toy is shown to be almost surely live—with probability 1, the arbiter eventually, grants some pending request—while still satisfying all the other properties of an ideal arbiter. The analysis is more general than previously published results in that the inputs of the arbiter may vary while the arbiter is metastable, and conditions are given that ensure liveness even in the presence of such variations. The verification is accomplished by proof that the set of states forever trapped in the metastable region of the toy is lower dimensional than the state space of the toy as a whole. Parallels between the toy and the interlock can then be drawn.

Thesis/Dissertation

application/pdf

2009-03-16

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

http://hdl.handle.net/2429/6067

Computer Science

University of British Columbia

UBCV

DSpace