Relay Pattern


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

Links to examples that use this pattern

Multiple Sleeping Barbers with waiting customers Problem, Multiple Sleeping Barbers Problem and Single Sleeping Barbers Problem.