کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
435533 | 1441724 | 2011 | 13 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: Queue based mutual exclusion with linearly bounded overtaking Queue based mutual exclusion with linearly bounded overtaking](/preview/png/435533.png)
The queue based mutual exclusion protocol establishes mutual exclusion for N>1N>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 NN times, and that the overtaking threads were competing when the first one of them exits.
Research highlights
► High fairness verified for simple mutual exclusion.
► In this MX algorithm for NN threads, no thread is overtaken more than N−1N−1 times.
► Refinement methods are very useful for verification of concurrent algorithms.
► Proof assistants are essential for the verification of concurrent algorithms.
Journal: Science of Computer Programming - Volume 76, Issue 7, 1 July 2011, Pages 542–554