Click the items below to execute several examples. Features include:
(For simplicity, this implementation omits several features. Namely, the number of roles are fixed to three, no asynchronous communication, no scatter/gather (multicast), and no TCP nor HTTP binding. For these features, see full version. This web-based OCaml toplevel is compiled using Js_of_ocaml).
Note: Please use monadic version of let-binnding let* s = (send or receive) in ..
for
communication primitives, instead of normal let s = (send or receive) in ..
, as this version uses
a monadic verion
of OCaml's Thread
library implemented on top of lwt.
Enter/Return | Submit code |
Ctrl + Enter | Newline |
Up / Down | Browse history |
Ctrl + l | Clear display |
Ctrl + k | Reset toplevel |
Tab | Indent code |
ocaml-mpst
?ocaml-mpst
is a communication library powered by Multiparty Session Types (abbreviated as MPST) in OCaml. Thus it ensures:
--- under the assumption that all communication channels are used linearly. Linearity is checked either dynamically (default) or statically, via another library linocaml
.
let ring = (a --> b) msg @@ (b --> c) msg @@ (c --> a) msg finish
--- This is a simple three-party ring-based protocol with participants A
, B
and C
, circulating messages with label msg
in this order.
(a --> b) msg
specifies a message with label msg
is sent from a
to b
. Protocols are composed by applying combinator -->
to existing protocols (possibly via OCaml's function application operator @@
, as above).finish
denotes termination of a protocol.(More combinators will be explained later.)
sa
for A
, sb
for B
, and sc
for C
) from the protocol:let sa = get_ch a ring
let sb = get_ch b ring
let sc = get_ch c ring
(* Participant A *)
Thread.create (fun () ->
let sa = send sa#role_B#msg "Hello, " in
let `msg(str, sa) = receive sa#role_C in
print_endline str;
close sa
) ();;
(* Participant B *)
Thread.create (fun () ->
let `msg(str,sb) = receive sb#role_A in
let sb = send sb#role_C#msg (str ^ "MPST") in
close sb
) ();;
(* Participant C *)
let `msg(str, sc) = receive sc#role_C in
let sc = send sc#role_A#msg (str ^ " World!") in
close sc
It will start two threads behaving as the participant A
and B
, then runs C
in the main thread.
send s#role_X#msg value
outputs on channel s
to role X
, with a message label msg
and payload value value
. Expression s#role_X#msg
is a standard method invocation syntax of OCaml, chained twice in a row. It returns a continuation channel which should be re-bound to the same variable s
ensuring linearity, which is why sending is written as let s = send s#roleX .. in
.receive s#role_W
inputs the message from role W
. The received message will have form `msg(val, s)
packed inside a OCaml's polymorphic variant constructor `msg
, with payload value val
and continuation channel s
(again, re-binding existing channel variable s
).close
terminates a communication channel.###
The above code is session-typed, as prescribed in the protocol ring
above. The all communications are deadlock-free, faithful to the protocol, and type-error free!
Some basic notes:
(x --> y) msg @@ cont
, -->
is a 4-ary operator taking an output role x
, input role y
, message label msg
and continuation cont
, where @@
is a function application operator (equivalent to $
in Haskell).send s#role_X#msg value
is parsed as ((send (s#role_X#msg)) value)
.More examples including branching, loops and delegation will come soon!