A Session Type Provider
Compile-Time API Generation of Distributed Protocols with Refinements in F#Rumyana Neykova

Raymond Hu Nobuko Yoshida Fahd Abdeljallal

1Part One
Type Providers

2Type Providers
Problem: Languages do not integrate information-We need to bring information into the language

PLDI’163

Before Type Providers

With Type Providers

all data is typed
on-demand generation
autocompletion
background type-checking
4WorldBank Type Providers

Source

IDE/PROGRAM

Com󰇴󰇮󰇱󰈥r5

Ty󰇴e 󰈑󰈦󰈢v󰇯󰈧e󰈦Useful for structured data?

How about structured communication?

A6BC👍

A generalisation to distributed protocols requires
a notion of schema for structured interactions between services
an understanding of how to extract the localised behaviour foreach services

How about structured communication?

A7

BC

Part Two
Session Types

8

POPL’08

9

Session Types
Protocol Validation(int) from C to S;(bool) from S to C;✅

Program Verification
runB c = let (x, c’) =receive c in send true c’A system of well-behaved processes is free fromdeadlocks, orphan messages and reception errors
10✅

Useful for structured data?

👍Data Type providers bring information into thelanguage as strongly tooled, strongly typed

How about structured communication?

👍Session Type providers bring communication intothe language as strongly tooled, strongly typed
11

Our Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.

Session12

TypeProvider

Our Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.

Session13

TypeProvider

Our Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.send(S, Div, 6, 3)

Session14

TypeProvider

Our Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.send(S, Div, 6, 3).

Session15

TypeProvider

Our Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.send(S, Div, 6, 3).receive(S, Res, y)Session16

TypeProvider

Our Solution: Session Type Providers
Div(x:int, y:int) from S to C;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.

Session17

TypeProvider

Our Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.send(S, Div, 6, “hello”)

Session18

Type

Wrong payload

ProviderOur Solution: Session Type Providers
Div(x:int, y:int) from C to S;
Res(z:float) from S to C;

type Prot = STP<“Prot.scr”, A>

Session19

Type

Wrong protocol

ProviderSession Type providers bring communication into
the language as strongly tooled, strongly typed

Calculator Revisited!
y!=0

global protocol Calc(role S, role C){
choice at C {Div(x:int, y:int) from C to S;
Res(z:float) from C to S;
do Calc(C, S);} or {
Add(x:int, y:int) from C to S;
Res(z:int) from S to C;
do Calc(C, S);} or {
Sqrt(x:float) from C to S;
Res(y:float) from S to C;
do Calc(C, S);} or {
Bye() from C to S;
x>0Bye() from S to C;}}
21

Scribble with refinements
global protocol Calc(role S, role C){
choice at C {Div(x:int, y:int) from C to S;@y!=0Res(z:float) from S to C;
do Calc(C, S);} or {
Add(x:int, y:int) from C to S;
Res(z:int) from S to C;
do Calc(C, S);} or {
Sqrt(x:float) from C to S;@x>0Res(y:float) from S to C;
do Calc(C, S);} or {Bye() from C to S;
interaction refinement
Bye() from S to C;}}New22

Part ThreeA Session Type Provider

23

What do you get from a session type provider?
Ses󰇷󰇮󰈣󰈡 Ty󰇴e󰈤

Saf󰇪󰇹󰈠

A statically well-typed endpoint program will never perform a
non-compliant I/O action w.r.t. the source protocol.

Ty󰇴e 󰈑󰈦󰈢v󰇯󰈧e󰈦sUsa󰇨󰇮󰇱󰇯t󰈂

compile-time generation
background type checking & auto-completiona platform for tool integration (e.g. protocol validation)In󰇹e󰈦󰇧c󰇹󰇯o󰈡 r󰇪ﬁ󰇳󰈥󰈩en󰇹󰈤

Rel󰇮󰈜󰇨i󰇱󰇮t󰈂

runtime enforcement of constraint
implicitly send values that can be inferred (safe by construction)
do not send values that can be locally inferred24

A Session Type Provider (Architecture)
F# Program

Scribble file

Validates
Scribble local file
Model Checker
SMT Solver

Generate types
FSM + guards

F# typesF# codeSes󰇷󰇮󰈣󰈡 Ty󰇴e 󰈑󰈦󰈢v󰇯󰈧e󰈦

The type provider framework is used for tool integration

25

Model26

Properties

CFSM

F# Type

CodeModelProperties

CFSM

F# TypeCode1(x:int) from A to C;
2(y:int) from B to C; @y>x

Bounded model checking as a validation methodology [FASE’16]
Safety Properties:
reception-error freedomorphan-message freedom
deadlock freedom27ModelProperties

CFSM

F# Type

CodeRefinement satisfiability
Refinement progress28/✅

ModelProperties

CFSM

F# TypeCode

Refinement satisfiability
check if the conjunction of all formulas is satisfiable
e.g. (and (> y (+ x 1))(< y 4)(> x 3))
1(x:int) from A to B; @x>3
choice at B {2() from B to A;}
or {3(y:int) from B to A; @y>x+1 and y<4}

Checks if all execution paths are reachable
1(x:int) from A to B; @x>3
choice at B {2() from B to A;}
or {3(y:int) from B to A; @y>x+1 and y>4}29✅

ModelProperties

CFSM

F# Type

CodeRefinement satisfiability
check if the conjunction of all formulas is satisfiable
e.g. (and (> y (+ x 1))(< y 4)(> x 3))
1(x:int) from A to B; @x>3
choice at B {2() from B to A;}
or {3(y:int) from B to A; @y>x+1 and y<4}1(x:int) from A to B; @x>3
choice at B {2() from B to A;}
or {3(y:int) from B to A; @y>x+1 and y>4}30✅

ModelProperties

CFSM

F# TypeRefinement progress
check if formula is satisfiable for all preceding solutions
e.g.(forall ((x Int)(y Int))(=> (> x 3)(or (< x y)(> x y))))1(x:int) from A to B; @x>3
2(y:int) from A to B;
choice at B {3() from B to A; @x>y}or {4(y:int) from B to A; @x>y}

Ensures that at any output point in the protocol
1(x:int)
from A to B; @x>3
implementations
therewillbealways
some2(y:int) from A to B;for which
the@x>=y}formula holds
choice at Bvalues{3() fromB to A;✅
or {4(y:int) from B to A; @x>y}1(x:int) from A to B; @x>3
2(y:int) from A to B; @y<=3choice at B {3() from B to A; @x>=y}or {4(y:int) from B to A; @x<y}31✅

CodeModel

Properties

CFSM

F# TypeRefinement progress
check if formula is satisfiable for all preceding solutions
e.g.(forall ((x Int)(y Int))(=> (> x 3)(or (< x y)(> x y))))1(x:int) from A to B; @x>3
2(y:int) from A to B;
choice at B {3() from B to A; @x>y}or {4() from B to A; @x<y}1(x:int) from A to B; @x>3
2(y:int) from A to B;
choice at B {3() from B to A; @x>=y}or {4() from B to A; @x<y}✅

1(x:int) from A to B; @x>3
2(y:int) from A to B; @y<=3choice at B {3() from B to A; @x>y}or {4() from B to A; @x<y}✅/32

CodeModel

Properties(x:T1) from A to B;

33

CFSM

F# TypeCode(y:T2) from B to C; (z:T3) from C to A;ModelProperties

CFSM

global protocol Calc(role S, role C){choice at C {Div(x:int, y:int) from C to S; @y!=0Res(z:float) from S to C;
do Calc(C, S);} or {
Bye() from C to S;
Bye() from S to C;}}34

F# Type

CodeModel

Properties

C?Bye

CFSM

F# TypeCode1

Map each state to a class

C?Div(int,int)
C!Res(float)

2

3
C!Bye

4

Map each transition to a method, e.g:
send method
receive methodModel

Properties

C?Bye

CFSM

F# Type

Code1

C?Div(int,int)
C!Res(float)2type State2 =member send: C*Res*float→ State1

3

type State3 =member send: C*Bye→ State4

4

type State4 =member finish: unit→ EndC!Bye

ModelProperties

CFSM

F# Typeglobal protocol Calc(role S, role C){choice at C {Div(x:int, y:int) from C to S; @y!=0Res(z:float) from S to C; @z=x/y
do Addeer(C, S);} or {
Client as C
Bye() from C to S;
Bye() from S to C;}}
RecServer as S

Div{ResBye
Bye

37CodeModelProperties

C?Bye

CFSM

F# TypeCodetype State1 =member branch: unit→ ChoiceS1

1C?Div(int,int)
C!Res(float)

type Div = interface ChoiceS1
member receive: int*int→ State2
type Bye = interface ChoiceS1
member receive: → State3

2

type State2 =member send: C*Res*float→ State1

3

type State3 =member send: C*Bye→ State4

4

type State4 =member finish: unit→ EndC!Bye

ModelProperties

CFSM

F# Type

Code

1
C?Bye
C?Div

let rec calcServer (c:Calc.State1) =match c.branch() with|:? Calc.Bye as bye->

2C!Res|:? Calc.Div as div ->3calcServer c1

C!Bye439Model

Properties

CFSM

F# TypeCode1C?ByeC?Div2C!Res

let rec calcServer (c:Calc.State1) =let x, y = new Buf<int>(),new Buf<int>()
match c.branch() with|:? Calc.Bye as bye->
bye.receive(C).send(C, Bye).finish()|:? Calc.Div as div ->let c1 = div.receive(C, x, y).send(C, Res, x.Val/y.Val)

3

calcServer c1

C!Bye4

ModelProperties

CFSM

send
constraints as lambda functions
serialise payload
manage and use TCP sockets

41

F# Type

Codequotations
splicingModelProperties

CFSMF# Type

type Prot = STP<“Prot.scr”, C>
let s = new Prot().Init()s.send(S, Div, 6, 3)

Code.Net IL CODEemit

Compiler
Type declarations

How to compile this code?

Session42

Type

ProviderAST ofgenerated code

ModelProperties

CFSM

F# Type

CodeSafety guarantees

A statically well-typed STP-endpoint program will neverperform a non-compliant I/O action w.r.t. the source protocol.

Compile-time performanceping-pongType and Code Generation (no refinements)
Protocol checking (no refinements)
Type and Code Generation (with refinements)
Protocol checking (with refinements)API Generation does not impact the development time44

Run-time performanceping-pong-no-refinements

ping-pong-refinements

Runtime overhead due to:branching, runtime checks, serialisation
The performance overhead of the library stays in 5%-7% range
The performance overhead of run-time checks is up to 10%-12%45

Future work and Resources
Framework Summary
Type-driven development of distributed protocols
Support for refinements on message interactions…ask me for more supported features
Future Work
Static verification of refinements
Partial model checking
Support for erased type providers (event-driven branching)
Resources:Session type provider: https://session-type-provider.github.io
Scribble: http://scribble.doc.ic.ac.uk/
MRG: mrg.doc.ic.ac.uk
46

Thank you!

47

Q&AAnswers

Questionspa󰇶󰈤󰇪-> an󰇧󰇰󰈠s󰈥 -> p󰇶e󰇺t󰈂 󰇵ri󰇳󰇺

48

48

Q&A
Answers

Questionspa󰇶󰈤󰇪-> an󰇧󰇰󰈠s󰈥 -> p󰇶e󰇺t󰈂 󰇵ri󰇳󰇺
Che󰈛󰈬 t󰇬󰇪 󰇺󰈣ol 󰈇󰈢󰈦 m󰈣󰇶e 󰈆󰇪󰈜tu󰇶󰇪󰈤:documentation on the fly
non-blocking receive
explicit connections
49

49

recompilation on protocol change
online vs offline mode
support by any .Net language