package sessions

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

  • author essdotteedot [<essdotteedot[at]gmail[dot]com>]
  • version 0.1.0

A session type ('a,'b) session represents a protocol that a particular process carries out. Here 'a and 'b are duals of each other.

A process ('a,'b,'c) process is parameterized by a starting session type 'b, '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 unit.

The following operations are duals of each other :

  • [`Stop], [`Stop]
  • [`Send of 'a * 'b], [`Recv of 'a * 'b], where 'b is a session type
  • [`Offer of ('a, 'b) session * ('c, 'd) session ], [ `Choice of ('b, 'a) session * ('d, 'c) session ], where 'a, 'b, 'c, 'd are 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_str_send_int_stop is ([ `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 `Offer and `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 IO.

OCaml

Innovation. Community. Security.