Channel<P>

Channels allow asynchronous type-safe communication between two processes. Channels are templated by a Session Type, P, to specify what operations are allowed on them at any given time.

Functions

self.send(e : T) -> Unit

  • Given: self : -T;P
  • Action: Sends the result of evaluating expression e : T to the remote process. If e is linear, the sent value will be copied. If it is non-linear, then the value will be moved to the remote process.
  • Result: self : P

self.recv() -> T

  • Given: self : +T;P
  • Action: Receives a value of type T from the remote processs.
  • Result: self : P

unfold(self) -> Unit

  • Given: self : ?P_1;P_2
  • Action: Unfolds an interation of P_1 from ?P_1.
  • Result: self : P_1;?P_1;P_2

unfold(self) -> Unit

  • Given: self : *?P_1;P_2
  • Action: Unfolds an interation of P_1 from *?P_1 (P_1 is guarded).
  • Result: self : P_1;*?P_1;P_2

more(self) -> Unit

Deprecated; See unfold.

more(self) -> Unit

Deprecated; See unfold.

weaken(self) -> Unit

  • Given: self : ?P_1T;P_2
  • Action: Finishes loop ?P_1.
  • Result: self : P_2

self[P_i] : Unit

  • Given: self : InternalChoice<P_1, ..., P_n>
  • Action: Selects protocol P_i from the internal choice to follow.
  • Result: self : P_i

self[lbl_i] : Unit

  • Given: self : InternalChoice<lbl_1 : P_1, ..., lbl_n : P_n>
  • Action: Selects protocol P_i identified by unique label lbl_i from the internal choice to follow.
  • Result: self : P_i

self.cancel() -> Unit

  • Since: 1.3.4
  • Given: self : Cancelable<...Cancelable<P_1>;P_2>;P_3
  • Action: Cancels (skips over) the innermost session type
  • Result: self : Cancelable<P_2>;P_3

Channel-Specific Control Flow Operations

accept(self) {...}

  • Given: self : !P_1;P_2
  • Action: Allows us to repeat the loop body as many times as are requested by the remote process to fulfill !P_1. Outside of the loop, the channel thus continues as c : P_2.
  • See here for details.

acceptWhile(self, e : boolean) {...}

  • Given: self : !P_1;P_2 or self : *!P_1;P_2
  • Action: Allows us to repeat the loop body as many times as are requested by the remote process so long as e evaluates to true. Outside of the loop, the channel thus continues as c : !P_1;P_2 or self : *!P_1;P_2 (the session is returned to its state before the acceptWhile).
  • See here for details.

acceptIf(self, e : boolean) {...}

  • Given: self : !P_1;P_2 or self : *!P_1;P_2
  • Action: Allows us to unfold a single iteration of the of course loop so long as the remote process requests it of us and e evaluates to true. After the acceptIf, the channel thus continues as c : !P_1;P_2 or self : *!P_1;P_2 (the session is returned to its state before the acceptIf)
  • Details forthcoming; however, the original Bismuth paper may be useful.

offer self (| P_i => ...)*

  • Given: self : ExternalChoice<P_1, ..., P_n>
  • Action: Allows us to perform a case analysis on each offered session type to allow for us to branch to a program which follows the selected session type.

Example:

// Given c : ExternalChoice<-int, +boolean;-boolean>

offer c 
  | -int => c.send(5);
  | +boolean => {
  	boolean b := c.recv(); 
  	c.send(!b);
    }

offer self (| lbl_i => ...)*

  • Given: self : ExternalChoice<lbl_1 : P_1, ..., lbl_n : P_n>
  • Action: Allows us to perform a case analysis on each offered session type to allow for us to branch to a program which follows the selected session type.

Example:

// Given c : ExternalChoice<sendInt: -int, recvBool: +boolean;>

offer c 
  | sendInt => c.send(5);
  | recvBool => boolean b := c.recv();

Specifications

  • Size: TODO
  • Default Location: FIXME
  • Default Modifiers: Temporal, Linear