Bound Pattern
Syntax
Bound(R,n), where R is a region and n is an integer.
Description
At most n threads can be in region R at any point of time.
Diagram
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