Barrier Pattern
Syntax
Barrier(R_1,R_2), where R_1 and R_2 are regions.
Description
The Kth thread to enter R_1 and the K th thread to enter R_2 meet at their respective synchronization regions and leave together.
Diagram
Representation as Global Invariant
Unbounded Global Invariant
Out_2 <= In_1 and Out_1 <= In_2
Bounded Global Invariant Counter Version
Ba_1 <= 0 and Ba_2 <= 0
Links to examples that use this pattern
Single Sleeping Barber Problem, Multiple Sleeping Barbers Problem, and Multiple Sleeping Barbers with waiting customers Problem