ocaml mpst in 5 minutes

The tutorial below guides you through creating a very simple ring protocol, where three roles (a, b, c) are forwarding a message to each other.

1. Before we start, we have to import the required libraries.

open Concur_shims (* a wrapper over the standard communication libraries (lwt and Event)*)
open Mpst (* the mpst-ocaml library *)
open Mpst.Util (* definition for the of roles (a, b, c) and labels (msg) in the example *)
let (let*) = IO.bind  (* needed for the monadic send, receive *)

2. Write down a protocol using Global Combinators.

let ring = gen @@ (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.

• Protocol (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).
• Combinator finish denotes termination of a protocol.
• the function gen forces the evaluation of the combinators.

2. Extract channels for each participant (here sa for A, sb for B, and sc for C) from the protocol:

let ea = get_ch a ring
let eb = get_ch b ring
let ec = get_ch c ring

3. Create threads for each participant! You have two option for implementing the processes.

• Option i. checks dinamically that channels are used linearly.

• Option ii. checks statically that channels are used linearly.

  1. With Dynamic linearity checks

let tA =
  Thread.create (fun () ->
      print_endline "A start";
      let* ea = send (ea#role_B#msg) () in
      let* `msg((), ea) = receive (ea#role_C) in
      print_endline "A done";
      close ea
    ) ()

let tB =
  Thread.create (fun () ->
      print_endline "B start";
      let* `msg((), eb) = receive (eb#role_A) in
      let* eb = send (eb#role_C#msg) () in
      print_endline "B done";
      close eb
    ) ()

let tC =
  Thread.create (fun () ->
      print_endline "C start";
      let* `msg((), ec) = receive (ec#role_B) in
      let* ec = send (ec#role_A#msg) () in
      print_endline "C done";
      close ec
    ) ()

• Primitive 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 .

• Primitive 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_ constructormsg, with payload value val` and continuation channel `s` (again, re-binding existing channel variable `s`).

• Primitive close terminates a communication channel.

  2. With Static linearity checks

(* Participant A *)
let tA =
  Thread.create (fun () -> 
    let%lin ea# = send (fun x -> x#role_B#msg) "Hello, " in
    let%lin `msg(str, #ea) = receive (fun x -> x#role_C) in
    print_endline str;
    close es
  ) ()

(* Participant B *)
let tB =
  Thread.create (fun () ->
    let%lin `msg(str,#eb) = receive (fun x -> x#role_A) in
    let%lin #eb = send eb (fun x -> x#role_C#msg) (str ^ "MPST") in
    close eb
  ) ()

(* Participant C *)
let tC = 
  Thread.create (fun () ->
    let%lin `msg(str, #ec) = receive (fun x -> x#role_C) in
    let%lin #ec = send ec (fun x -> x#role_A#msg (str ^ " World!") in
    close ec

3. Run all threads.

let () = IO.main_run @@ IO_list.iter Thread.join [tA; tB; tC]

4. Run the example.

• Open the dune file (/examples/mpst/dune) and add a new executable entry to it:

(executable
 (name ring_protocol)
 (modules ring_protocol)
 (libraries mpst))

• Open the terminal, assuming the name of your file is ring_protocol.ml, execute the following command:

dune build examples/mpst/ring_protocol.ml
dune exec ./examples/mpst/ring_protocol.exe

Congratulations! You have completed your first ocaml-mpst example. You can go back to the instructions page and continue with other examples.

The above will start three threads behaving as the participant A and B, and C.

The above code is session-typed, as prescribed in the protocol ring above. All communications are deadlock-free, faithful to the protocol, and type-error free!

Some basic notes:

• In a protocol (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).
• Output expression send s#role_X#msg value is parsed as ((send (s#role_X#msg)) value).