This is joint work with Alex A. Aravind, published in A queue based mutual exclusion algorithm, Acta Informatica 46 (2009) 73-86. A proof script for the proof assistant PVS is available.
Competing threads can be overtaken by other threads. We have recently proved with PVS that every competing thread is overtaken less than k times where k is the number of competing threads at the moment that the first overtaking thread exits. A paper about this result has been submitted. In this work, we need a mild additional atomicity condition.
Several (N) children are playing in a garden. When they are thirsty, they can enter a room where a drink is offered, but there is only one glass. The room has N corners, numbered from 0 upward. Any child in corner 0 can take the glass. After it had its drink, the child goes back to the garden, to come back again when it is thirsty. A child that enters the room starts counting the other children in the room. Any child in the room that sees that there are not more than k children in the room other than itself, may move to corner k.
Each corner with a positive number has a chair where one child can sit on. Any child in this corner can decide to climb onto the chair. If the chair is occupied and a child decides to climb onto it, it first pushes the present occupant from the chair. A child pushed from the chair in corner k goes to corner k-1. The children in the room are thirsty and want to get a drink in corner 0. The organisers claim that there is always at most one child in corner 0, and that every child in the room will eventually get there.
Counting children takes time, but a child need not count children that entered after it started counting, and it may discount children that leave the room before it finished counting. When a child has pushed another from a chair, it must climb the chair, although another child may succeed earlier. After climbing a chair, a child that wants to count children needs to start from scratch.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink