Group Pattern


Group(R_1,N_1,R_2,N_2...,R_n,N_n), where R_1, R_2 till R_n are regions, and N_1, N_2 till N_n are integers.


R_1, R_2 ...,R_n are regions in one cluster. It is requires that N_i threads in R_i (1 <= i <= n) meet, form a group, and leave respective synchronization regions togather.


Representation as Global Invariant

Unbounded Global Invariant

And 1<= i <= n ( And 1<= j <= n (Out_i <= (In_j/N_j) * N_i))

Bounded Global Invariant Counter Version

And 1 < i,j <= n (G_ij <= 0)

Links to examples that use this pattern

Multiple Sleeping Barbers Problem, Multiple Sleeping Barbers with waiting customers Problem, Single Roller Coaster Cars Problem, and Multiple Roller Coaster Cars Problem.