What is a synchronization diagram?

:: cmx, concurrency, diagrams

A synchronization diagram displays the synchronization behavior of a set of threads as a sequence of discrete events between them. A diagram contains a fixed number of rows starting on the left and extending to the right by some number of columns. Each row models the behavior of a thread, and each column represents a synchronizing event. Time flows from left to right.

The simplest diagram is a channel put/get interaction.

        |      put  ,--. ||

 putter |  v  ----->|ch| ||

        |           `--' ||

        +                +

        | ,--. get       ||

 getter | |ch|----->  v  ||

        | `--'           ||

A more interesting example is the cmx forward construct.

(define (forward m1 m2)
  (bind (accept m1) (curry offer m2)))

Here’s a "proof" that it works.

         |      offer   ,--. :                   | ,--. accept       |     put  ,--. ||

 say     |  m0 -------->|m1| :                   | |m0|--------> m*  |  v ----->|m*| ||

         |              `--' :                   | `--'              |          `--' ||

         +                   +                   +                   +               +

         | ,--. accept       |      offer   ,--. ||                  :               :

 forward | |m1|--------> m0  |  m0 -------->|m2| ||                  :               :

         | `--'              |              `--' ||                  :               :

         +                   +                   +                   +               +

         :                   | ,--. accept       |      offer   ,--. | ,--. get      ||

 hear    :                   | |m2|--------> m0  |  m* -------->|m0| | |m*|-----> v  ||

         :                   | `--'              |              `--' | `--'          ||

Clearly, all threads finish (at the double bars). Less obviously, hear is not able to commit to the exchange until after say has initiated. Most importantly, say and hear finish together, as v is delivered.

For cmx constructs, a row corresponds to an expression in the calculus of mediated exchange and the diagram condenses neatly.

 say     | offer m1 m0    :                | m* = accept m0 | put m* v   ||

 forward | m0 = accept m1 | offer m2 m0    ||               :            :

 hear    :                | m0 = accept m2 | offer m0 m*    | v = get m* ||

I’ve drawn many synchronization diagrams on paper and as picts, and I need to decide where to put them. The protocol used by cmx was discovered by iteratively modeling events, determining what went wrong, and adjusting the model; this modeling process might be worth documenting, too.

About three months ago, I caught a synchronization timing bug in the code dispatch replaces and I just finished integrating cmx (and event-lang) back into Neuron to squash it.

Informal proof by synchronization diagram

:: cmx, concurrency, diagrams

Let v be some value. Denote by mK the mediator identified by (sub)script K, and by m-NAME the mediator identified by name NAME. Define the primitive mediated operations (offer, accept, put, get) as in http://docs.racket-lang.org/cmx/.

Further,

(define (say m v [m0 (make-mediator)])
  (seq (offer m m0) (bind (accept m0) (λ (m*) (put m* v)))))
 
(define (hear m)
  (bind (accept m) (λ (m0) (seq (offer m0 m0) (get m0)))))
 
(define (forward m1 m2)
  (bind (accept m1) (λ (m0) (offer m2 m0))))

and

(define m-say (make-mediator))
(define m-hear (make-mediator))
(define sayer (thread (λ () (sync (say m-say v)))))
(define hearer (thread (λ () (sync (hear m-hear)))))
(define forwarder (thread (λ () (sync (forward m-say m-hear)))))

Then the synchronization diagram for say, forward, and hear is:

 say     | offer m1 m0    :                | m* = accept m0 | put m* v   ||

 forward | m0 = accept m1 | offer m2 m0    ||               :            :

 hear    :                | m0 = accept m2 | offer m0 m*    | v = get m* ||

Theorem [Progress]: A forwarded say/hear exchange never gets stuck.

Proof: By demonstration.

Let m0 be a fresh mediator, and suppose each of (say, hear, forward) is running in a separate thread, as shown above, at some time t0.

Note that each primitive operation must be paired with a complementary operation in another thread, through a shared mediator, to succeed at run time.

The following ordered sequence of successful pairings is observed:

At some time t1 > t0, the sayer transfers m0 to the forwarder through the control channel of racketid[m-say].

At some time t2 > t1, the forwarder transfers m0 to the hearer through the control channel of m-hear and then ends.

From this point on, the remaining threads behave as in the second half of a simple say/hear exchange:

At some time t3 > t2, the hearer transfers m0 to the sayer through the control channel of m0.

At some time t4 > t3, the sayer transfers v to the hearer through the data channel of m0 and then both threads end. ∎