Bound Pattern


Bound(R,n), where R is a region and n is an integer.


At most n threads can be in region R at any point of time.


Global Invariant

Unbounded Global Invariant

in - out <= n

Bounded Global Invariant Counter Version

B <= n

Links to examples that use this pattern

Reader writer problem, Single Sleeping Barber Problem, Multiple Roller Coaster Cars Problem, Multiple Sleeping Barbers Problem, and Multiple Sleeping Barbers with waiting customers Problem