Queue based mutual exclusion with linearly bounded overtaking |
| |
| Authors: | Wim H. Hesselink Alex A. Aravind |
| |
| Affiliation: | a Department of Computing Science, University of Groningen, P.O. Box 407, 9700 AK Groningen, The Netherlandsb Computer Science Program, University of Northern British Columbia, Prince George, BC, Canada, V2N4Z9 |
| |
| Abstract: | The queue based mutual exclusion protocol establishes mutual exclusion for N>1 threads by means of not necessarily atomic variables. In order to enter the critical section, a competing thread needs to traverse as many levels as there are currently competing threads. Competing threads can be overtaken by other competing threads. It is proved here, however, that every competing thread is overtaken less than N times, and that the overtaking threads were competing when the first one of them exits. |
| |
| Keywords: | Mutual exclusion Refinement Shared memory Bounded overtaking Verification |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
