Barrier(R_1,R_2), where R_1 and R_2 are regions.
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.
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