In a system of N threads, a barrier is a synchronization mechanism to let the threads repeatedly pass through a barrier point. When a thread arrives at this point, it has to wait for all threads to arrive. The threads can pass the point only when all have arrived. In the literature, many barriers have been proposed. A proof of correctness is rarely provided. The attached file WHH598 presents four barriers with correctness proofs supported by the proof assistant PVS. Two of them are known, the other two seem to be new.
The partial barrier is a variation of the barrier. A partial barrier for size M is a synchronization mechanism for thread systems that allows threads repeatedly to pass an entry point only in batches of precisely M elements. The members of the batch can subsequently release membership. When all members have released, and enough new participants are available, a new batch can be formed and launched. The attached file WHH599 presents a partial barrier based on fetch-and-increment. This paper is supported by a PVS proof script .
It is also possible to construct a partial barrier using trylock. See the attached file WHH600. A PVS proof script is available. The fetch-and-increment solution is probably much more efficient than the trylock solution. The trylock solution, however, is more flexible, and, in my view, more interesting.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink