We are striving to develop the new generation of OCaml-MPST which equips with timeouts (in particular, mixed choices in session-type/process-calculus terminology) and is supporting OCaml Multicore.
The older ECOOP 2020 version is still accessible at mpst1 branch.
ocaml-mpst
is a communication library powered by Multiparty Session Types
(abbreviated as MPST) in OCaml. Thus it ensures:
- Deadlock-freedom,
- Protocol fidelity (communication will take place according to a prescribed protocol) and
- Communication safety (you do not get any type-mismatch errors)
--- under the assumption that all communication channels are used linearly.
Linearity is checked either dynamically (default) or statically, via another
library linocaml
.
Install OPAM. then the following command will install OCaml-MPST in your OPAM switch:
opam pin -y https://github.com/keigoi/ocaml-mpst.git
It will install several packages from this and other repositories. To remove them, type:
opam pin remove ocaml-mpst rows hlist
.
Try OCaml-MPST Online!
- An interactive web interface (though with an older version) is available at:
To run a example, after installation, type the script below in the terminal:
git clone --recurse-submodules https://github.com/keigoi/ocaml-mpst.git
cd ocaml-mpst/
dune exec examples/mpst/calc.exe
- Create and go into
examples/my_example/
and prepare your owndune
file andmy_example.ml
.
(executable
(name my_example)
(modules my_example)
(preprocess
(staged_pps mpst.ppx.ty))
(libraries mpst))
- Declare the name of participants (roles) and labels:
open Mpst.BasicCombinators
open Mpst.Unicast
[%%declare_roles_prefixed a, b, c] (* note that the order matters *)
[%%declare_labels msg]
- Write down a protocol using Global Combinators.
let ring = (a --> b) msg @@ (b --> c) msg @@ (c --> a) 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 labelmsg
is sent froma
tob
. 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.
(More combinators will be explained later.)
- Extract channels for each participants (here
sa
forA
,sb
forB
, andsc
forC
) from the protocol:
let (`cons(sa, `cons(sb, `cons(sc, _)))) = extract ring;;
- Run threads in parallel, one for each participant!
(* Participant A *)
Thread.create (fun () ->
let sa = select sa#role_B#msg in
let `msg sa = branch sa#role_C in
close sa
) ();;
(* Participant B *)
Thread.create (fun () ->
let `msg sb = branch sb#role_A in
let sb = select sb#role_C#msg in
close sb
) ();;
(* Participant C *)
let `msg sc = branch sc#role_B in
let sc = select sc#role_A#msg in
close sc;
print_endline "Ring-based communication finished successfully!"
- Run it!
dune exec ./my_example.exe
It will start two threads behaving as the participant A
and B
, then runs C
in the main thread.
-
Primitive
select s#role_X#msg value
outputs on channels
to roleX
, with a message labelmsg
. Expressions#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 variables
ensuring linearity, which is why sending is written aslet s = select s#roleX .. in
. -
Primitive
branch s#role_W
inputs the message from roleW
. The received message will have formmsg s` packed inside a OCaml's _polymorphic variant_ constructor
msg, with continuation channel
s(again, re-binding existing channel variable
s`). -
Primitive
close
terminates a communication channel. -
To communicate OCaml values, use
(==>)
combinator andsend
andreceive
primitives (see the calculator example, for details).
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:
- In a protocol
(x --> y) msg @@ cont
,-->
is a 4-ary operator taking an output rolex
, input roley
, message labelmsg
and continuationcont
, where@@
is a function application operator (equivalent to$
in Haskell). - Output expression
select s#role_X#msg
is parsed as(select (s#role_X#msg))
.
More examples including branching, loops and delegation will come soon!
- See Examples