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