Resource Pattern



Syntax

Resource(Rp,Np,Rc,Nc,n), where Rp and Rc are regions and Np,Nc and n are integers.

Description

Two synchronization regions, Rp and Rc, are in one cluster. There is a pool of resources. Initially, there are n resource items in the pool. When a thread executes Rp, it produces (or returns) Np resource items. When a thread executes Rc, it consumes (or borrows) Nc resource items. If there are less than Nc resource items in the pool, a thread executing Rc waits until there are at least Nc resource in the pool.

Diagram





Representation as Global Invariant

Unbounded Global Invariant

In_c <= (Out_p * N_p + n)/N_c

Bounded Global Invariant Counter Version

R_pc <= n

Links to examples that use this pattern

Hungry Birds problem and Gyroscope Rudder problem.