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