This module provides modules to create binary sessions types for statically verifying protocols between a pair of concurrent processes.
Binary processes which are parametrized by binary session types can be created using
Binary_process. A pair of processes can only be run if they have compatible (dual) session types.
A session type
('a,'b) session represents a protocol that a particular process carries out. Here
'b are duals of each other.
('a,'b,'c) process is parameterized by a starting session type
'a is it's return value and
'c is it's final session type. Two processes can be run only if they have dual initial session types a final session type of
The following operations are duals of each other :
[`Send of 'a * 'b],
[`Recv of 'a * 'b], where
'bis a session type
[`Offer of ('a, 'b) session * ('c, 'd) session ], [ `Choice of ('b, 'a) session * ('d, 'c) session ], where
'dare session types
Here are some examples of processes which are duals (assume we have an implementation of
IO called ExIO) :
module BP = Binary_session.Make (ExIO) let send_str_recv_int_stop = BP.(send "hello" >>= fun () -> recv () >>= fun (i : int) -> stop ()) let recv_str_send_int_stop = BP.(recv () >>= fun (s : string) -> send 1 >>= fun () -> stop ()) let _ = BP.run_processes send_str_recv_int_stop recv_str_send_int_stop
Note that the session type associated with the process
send_str_recv_int_stop was inferred as
([ `Send of string * [ `Recv of int * [ `Stop ] ] ],[ `Recv of string * [ `Send of int * [ `Stop ] ] ]) BP.session
as you can see it provides it's own session type
[ `Send of string * [ `Recv of int * [ `Stop ] ] ] as well as it's dual
[ `Recv of string * [ `Send of int * [ `Stop ] ] ].
The session type associated with the process
([ `Recv of string * [ `Send of int * [ `Stop ] ] ], [ `Send of string * [ `Recv of int * [ `Stop ] ] ]) BP.session
we see that it indeed has the dual of
send_str_recv_int_stop which means that
BP.run_processes send_str_recv_int_stop recv_str_send_int_stop can type check.
If these two processes were to differ in such a way that they were not duals then
BP.run_processes send_str_recv_int_stop recv_str_send_int_stop would not type check.
Here is another example using
`Choice as well as recursion.
module BP = Binary_session.Make (ExIO) let rec print_server () = BP.( offer (stop ()) (recv () >>= fun (s : string) -> lift_io (Lwt_io.printlf "print server : %s" s) >>= print_server) ) let rec print_client (i : int) = BP.( lift_io (Lwt_io.read_line Lwt_io.stdin) >>= fun (s : string) -> if s = "q" then choose_right (send (Printf.sprintf "Total lines printed : %d" (i+1)) >>= fun () -> choose_left (stop ())) else choose_right (send s >>= fun () -> print_client (i+1)) ) let _ = BP.run_processes print_server (print_client 0)
module type IO = sig ... end
Abstract type which can perform monadic concurrent IO.
module type Binary_process = sig ... end
A process which is parametrized by a binary session type.
module Make (I : IO) : Binary_process with type 'a io = 'a I.t and type chan_endpoint = I.chan_endpoint
Functor to create a module of type
Binary_process given a message module
I of type