Syncronization Patterns

We provide a set of global invariant patterns or idioms that can be used directly or composed to produce more complex synchronization specifications.

  • Bound(R, n): at most n threads can be in R at any point in time.

  • Exclusion (R_1, R_2, ..., R_n): at any point in time, threads can be in at most one synchronization region out of the n synchronization regions.

  • Resource((R_P, N_P), (R_C, N_C), n): a pool of resources (with n items in the pool initially) accessed by a producer region R_P that produces N_P resource items each time a thread executes it, and a consumer region R_C that consumes N_C resource items each time a thread executes it. If there are fewer than N_C resource items in the pool, a thread executing R_C waits at the entrance of the region until there are at least N_C resources in the pool.

  • Barrier(R_1,R_2): the k'th thread to enter R_1 and the k'th thread to enter R_2 meet at their respective synchronization regions and leave together.

  • Relay(R_1, R_2): a thread entering R_1 can leave R_1 immediately; however, the k'th thread entering R_2 is blocked and cannot leave R_2 until the k'th thread arrives at R_1. In this situation, an arrival of a thread at R_1 triggers a release of a thread at R_2.

    It is convenient to extend the barrier synchronization to the following more general form, called the Group synchronization.
  • Group((R_1, N_1), (R_2, N_2), ..., (R_n, N_n)): N_i threads entering R_i for i between 1 and n meet, form a group, and leave the respective synchronization regions together. For example, let n = 3, N_1 = 2, N_2 = 3, and N_3 = 4. Then, 2 threads in R_1, 3 threads in R_2, and 4 threads in R_3 form a group and leave together.

  • Asymmetric Group((n,R_11,N_11,R_12,N_12...,R_1n,N_1n,m,R_21,N_21,R_22,N_22,...,R_2m,N_2m): A cluster consists of multiple synchronization regions. The regions are divided into two sets. One set has n regions R_1i, and another has m regions R_2j. The two sets may overlap. For 0 <= k, all threads from the (k * N_2j)th thread to the ((k+1) * N_2j - 1)th thread entering R_2j may leave their respective regions only if all threads from the (k * N_1i)th thread to the ((k+1) * N_1i - 1)th thread have arrived at regions R_1i.

    Pattern-based synchronization specifications are formed by composing instances of the above patterns where composition is interpreted as logical conjunction.