Proving Newtonian Arbiters Correct, almost surely
| Autor: | Mitchell, Ian M. |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 1996 |
| Druh dokumentu: | Text |
| Popis: | 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. Science, Faculty of Computer Science, Department of Graduate |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|