Relay(R_1,R_2), where R_1 and R_2 are regions.
The thread entering R_1 can leave immediately; however the K th thread entering R_2 is blocked and cannot leave R_2 until the K th thread arrives at R_1.
Representation as Global Invariant
Unbounded Global Invariant
Out_2 <= In_1
Bounded Global Invariant Counter Version
Re <= 0