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