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

Bismuth Documentation