Demo Notes (Week 10 Tuesday)

1. Scheduler
2. Session Types

These are the demo notes I presented and added to in today's lecture, with a few corrections made afterwards (noted below). -Rob

1. Scheduler

If we don't know anything about a scheduler, we assume it can choose whatever interleavings between processes it wants, for example:

x-x-x-x-x-x-x-x

y-y-y-y-y-y-y-y

x-x-x-    x-x-x
      y-y-

x-  x-  x-  x-
  y-  y-  y-  y

etc.

2. Session Types

2.1. Choice and selection

2.1.1. Server process: providing choice

serve_eat_here |- Δ, x : SEatHere
                                 serve_takeaway |- Δ, x : STakeAway
------------------------------------------------------------------ &
x.case(serve_eat_here,serve_takeaway) |- Δ, x : SEatHere & STakeAway

SEatHere = dual(EatHere)
STakeAway = dual(TakeAway)
SEatHere & STakeAway = dual(EatHere (+) TakeAway)

2.1.2. Customer process: making selection

// Selection 1: send choice "eat here" then wait for food 

         eat_here |- Γ, x : EatHere
---------------------------------------------- (+)1
x[inl].eat_here |- Γ, x : EatHere (+) TakeAway

EatHere = dual(SEatHere)
TakeAway = dual(STakeAway)
EatHere (+) TakeAway = dual(SEatHere & STakeAway)

// Selection 2: send choice "takeaway" then wait for takeaway

         takeaway |- Γ, x : TakeAway
---------------------------------------------- (+)2
x[inr].takeaway |- Γ, x : EatHere (+) TakeAway

2.1.3. Dynamic Semantics of Choice/Selection

Run 1: left choice
ch x. x[inl].eat_here | x.case(serve_eat_here,serve_takeaway)
==> ch x. (eat_here | serve_eat_here)

Run 2: right choice
ch x. [inr].takeaway | x.case(serve_eat_here,serve_takeaway)
==> ch x. (takeaway | serve_takeaway)

2.2. Input and output (incl. empty input/output)

// Customer process
x[y].(pay | x(z).x().get_rcpt)

// Server process
x(y).x[z].(give_rcpt | x[].0)

2.2.1. Customer process typing derivation

                         get_rcpt |- D,z:GetReceipt
                     ---------------------------------- ⊥
                     x().get_rcpt |- D,z:GetReceipt,x:⊥
                  ----------------------------------------- ⅋
pay |- G,y:Pay    x(z).x().get_rcpt |- D,x:(GetReceipt ⅋ ⊥)
------------------------------------------------------------------ (x)
x[y].(pay | x(z).x().get_rcpt) |- G,D,x:(Pay (x) (GetReceipt ⅋ ⊥))

2.2.2. Server process typing derivation

Having derived the customer process type, we figured out what the server process' type ought to be by taking its dual:

dual(Pay (x) (GetReceipt ⅋ ⊥))
= dual(Pay) ⅋ dual(GetReceipt ⅋ ⊥)
= dual(Pay) ⅋ (dual(GetReceipt) (x) dual(⊥))
= dual(Pay) ⅋ (dual(GetReceipt) (x) 1)

Thus, calling dual(GetReceipt) = GiveReceipt for brevity:

x(y).x[z].(give_rcpt | x[].0) |- x : dual(Pay) ⅋ (GiveReceipt (x) 1)

But constructing the typing derivation tree makes sure of it:

                                                  ------------ 1
   give_rcpt |- T,y:dual(Pay),z:GiveReceipt       x[].0 |- x:1
  --------------------------------------------------------------- (x)
  x[z].(give_rcpt | x[].0) |- T,y:dual(Pay),x:(GiveReceipt (x) 1)
---------------------------------------------------------------------- ⅋
x(y).x[z].(give_rcpt | x[].0) |- T,x:(dual(Pay) ⅋ (GiveReceipt (x) 1))

2.2.3. Dynamic Semantics of Input/Output

2.2.3.1. Relevant reduction/equivalence rules

ch x. (x[y].(P | Q) | x(y).R) ==> ch y. (P | ch x. (Q | R))  "beta-(x)⅋"
ch x. (x[].0 | x().P) ==> P  "beta-1⊥"
ch x:A. (P | Q) == ch x:dual(A).(Q | P)  "swap"

2.2.3.2. Process reduction example (from class, with mistake fixed)

                  Customer                      Server
ch x. (x[y].(pay | x(z).x().get_rcpt) | x(y).x[z].(give_rcpt | x[].0))
            (P   |    Q             ) |             R
==> "beta-(x)⅋"
        P         (        Q           |            R            )
ch y. (pay | ch x.((x(z).x().get_rcpt) | x[z].(give_rcpt | x[].0)))
      ( P  |                     Q                                )
==> swap // Note, actually we didn't need to do this swap
      (                          Q                             |  P )
ch y. ((ch x.((x(z).x().get_rcpt) | x[z].(give_rcpt | x[].0))) | pay)
             (           P        |           Q             )
==> swap
             (           Q              |         P         )
ch y. ((ch x.((x[z].(give_rcpt | x[].0) | x(z).x().get_rcpt))) | pay)
                          P'          Q'                R'
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
=/> "beta-(x)⅋" // Mistake in class, ch. x needs to go to right of P'
ch y. (ch x. (ch z. (give_rcpt | (x[].0 | x().get_rcpt)) | pay))
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
==> "beta-(x)⅋" // Fixed, so we didn't need to apply Assoc after all
             (    P'       | ch x. ( Q'   |        R'      ))
ch y. (ch z. (give_rcpt | ch x. (x[].0 | x().get_rcpt)) | pay)
==> "beta-1⊥"
ch y. (ch z. (give_rcpt | get_rcpt) | pay)

2.2.3.3. Process reduction example (shorter solution)

Note the swap for channel y we did in class was actually unnecessary. Consequently, at the end of this reduction sequence, y's type is dual to the type that y had at the end of the immediately above example:

                  Customer                      Server
ch x. (x[y].(pay | x(z).x().get_rcpt) | x(y).x[z].(give_rcpt | x[].0))
==> "beta-(x)⅋"
ch y. (pay | ch x. (x(z).x().get_rcpt | x[z].(give_rcpt | x[].0)))
==> "swap"
ch y. (pay | ch x. (x[z].(give_rcpt | x[].0)) | x(z).x().get_rcpt)
==> "beta-(x)⅋"
ch y. (pay | ch z. (give_rcpt | ch x. (x[].0 | x().get_rcpt)))
==> "beta-1⊥"
ch y. (pay | ch z. (give_rcpt | get_rcpt))

2.3. Deadlock freedom of Session Types

P |- Γ, x : A      Q |- Δ, x : dual(A)
-------------------------------------- Cut
       ch x:A. (P | Q) |- Γ, Δ

Absence of communication loops between P and Q.
Wadler: "Communications along Γ and Δ are disjoint, so P and Q are restricted to communicate with each other only along x. If communication could occur along two channels rather than one, then one could form a loop of communications between P and Q that leads to deadlock."
Examples of deadlock-prone concurrent processes:

ch x. (x(u).wait_meal | x(v).wait_payment)
  - won't type check, because their types for x aren't dual

ch x, y. (x(u).wait_meal | y(v).wait_payment)
  - also won't type check, because we can't introduce ch for
    two channels at once

These would be rejected by session types, because Cut is the only typing rule to introduce a `ch` binder when typechecking parallel composition of two well-typed processes, and (1) their types for the one channel must be dual, and (2) Cut does not allow you to bind more than one channel simultaneously for these processes to communicate by:

---------------------------------------------------------------- Cut?
ch x:A⅋C. ch y:B⅋D. (x(u).wait_meal | y(v).wait_payment) |- Γ, Δ  (No.)

2.4. What if you wanted to express systems that allow deadlock?

An additional rule "Binary Cut allows one to express systems where communications form a loop and may deadlock"

P |- Γ, x : A, y : B      Q |- Δ, x : dual(A), y : dual(B)
---------------------------------------------------------- BiCut
            ch x:A, y:B. (P | Q) |- Γ, Δ

The deadlock-prone example would be accepted by session types with the BiCut rule added:

     R |- Θ, y : A, x : B 
    ---------------------- ⅋
    x(y).R |- Θ, x : A ⅋ B

(NB: Remember, order in session typing environments is ignored)

          etc.                                  etc.
----------------------------  ---------------------------------------------
wait_meal |- Γ,u:A,x:C,y:B⅋D  wait_pay |- Δ,x:dual(A⅋C),v:dual(B),y:dual(D)
----------------------------  ---------------------------------------------
x(u).wait_meal |- Γ,x:A⅋C,y:B⅋D  y(v).wait_pay |- Δ,x:dual(A⅋C),y:dual(B⅋D)
---------------------------------------------------------------------------
      ch x:A⅋C,y:B⅋D. (x(u).wait_meal | y(v).wait_pay) |- Γ, Δ