ocaml-mpst

You can try some features of ocaml-mpst-light.

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.

Examlpes (click to insert) -- More to come sooner!

Command

Enter/Return Submit code
Ctrl + Enter Newline
Up / Down Browse history
Ctrl + l Clear display
Ctrl + k Reset toplevel
Tab Indent code

What is 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.

ocaml-mpst in 5 minutes

  1. Write down a protocol using Global Combinators.
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.

(More combinators will be explained later.)

  1. Extract channels for each participants (here 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
  1. Run threads in parallel, one for each participant!
(* 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.

### 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:

More examples including branching, loops and delegation will come soon!