Exclusion Pattern


Exclusion(R_1,R_2,...,R_n), where R_i is a region (1<=i<=n).


Threads can be in at most one region out of n regions at any point of time (mutally exclusion).


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