Exclusion Pattern
Syntax
Exclusion(R_1,R_2,...,R_n), where R_i is a region (1<=i<=n).
Description
Threads can be in at most one region out of n regions at any point of time (mutally exclusion).
Diagram
Representation as Global Invariant
Unbounded Global Invariant
Let Comb(n,n-1) denote the collection of combinations of n-1 out of n from the set {1,2,...,n}. Then the global invariant is
Or C in Comb(n,n-1) (And i in C (In_i - Out_i == 0))
For example, if n=3, Comb(3,2) is {{1,2},{1,3},{2,3}}. Therefore, the global invariant for Exclusion(R_1,R_2,R_3) is
((In_1 - Out_1 == 0) and (In_2 - Out_2 == 0)) or
((In_1 - Out_1 == 0) and (In_3 - Out_3 == 0)) or
((In_2 - Out_2 == 0) and (In_3 - Out_3 == 0))
Bounded Global Invariant Counter Version
Or C in Comb(n,n-1) ( And i in C ((E_i == 0)))
Links to examples that use this pattern
Single Sleeping Barber Problem, Multiple Sleeping Barbers Problem, Reader writer problem, and Gyroscope Rudder problem