日本語

session-ocaml - Communication protocol inferred for OCaml

by Keigo Imai, Nobuko Yoshida and Shoji Yuen


NOTE: This page is less frequently updated than http://www.ct.info.gifu-u.ac.jp/~keigoi/session-ocaml/

What is session-ocaml?

Session-ocaml is a novel library for concurrent / distributed programming in OCaml featuring session types. The characteristics of it includes:

  • Statically checked, multiple simultaneous sessions.
  • The novel protocol types which provide a clear describtion of concurrent services.
    • Type inference.
    • Labelled branching and recursion, effectively represented using polymorphic variants in OCaml.
    • Delegation enables a ongoing session to be passed around threads.

Source code

Available at Github

Example

An "XOR server"

open Session0
(* The service channel *)
let xor_ch = new_channel ();;

(* The xor server *)
Thread.create (fun () ->
  accept_ xor_ch (fun () ->
  let%s x,y = recv () in
  send (xor x y) >>
  close ())) ();;                                                                            

(* A client *)
connect_ xor_ch (fun () ->
  send (false,true) >>
  let%s b = recv () in
  print_bool b; close ()) ()
The protocol type inferred for xor_ch:
[`msg of req * (bool*bool) * 
 [`msg of resp * bool * 
  [`close]]]

A logical operation server

open Session0
type binop =
  And | Or | Xor | Imp

(* The service channel *)
let log_ch = new_channel ()

let eval_binop = function
  | And -> (&&) | Or -> (||)
  | Xor -> xor
  | Imp ->
    (fun a b -> not a || b)
  
(* A logical operation
   server *)
let rec logic_server () = 
  match%branch0 () with
  |`bin ->
    let%s op = recv () in
    let%s x,y = recv () in                                                                                  
    send (eval_binop op x y)
    >>= logic_server
  |`fin -> close ();;

Thread.create
  (accept_ log_ch
      logic_server) ();;

(* A client *)
connect_ log_ch (fun () ->
  [%select0 `bin] >>
  send And >>
  send (true, false) >>
  let%s ans = recv () in                                                                                   
  (print_bool ans;
  [%select0 `fin] >>
  close ())) ()
The protocol type inferred for log_ch:
[`branch of req *
 [`bin of
  [`msg of req * binop *
   [`msg of req * (bool*bool) * 
    [`msg of resp * bool * 'a]]]
 |`fin of [`close]]] as 'a

An example with delegation

open Session

let deleg_ch = new_channel ()

let rec main_thread () =
  accept arith_ch ~bindto:_0 >>
  connect deleg_ch ~bindto:_1 >>
  deleg_send _1 ~release:_0 >>
  close _1 >>=
  main_thread

let rec worker_thread () =
  accept deleg_ch ~bindto:_1 >>
  deleg_recv _1 ~bindto:_0 >>
  close _1 >>
  arith_server () >>=
  worker_thread

let _ =
  for i = 0 to 5 do
    Thread.create
      (run worker_thread) ()
  done;
  run main_thread ()
The protocol type inferred for deleg_ch:
[`deleg of req *
 (logic_p, serv) sess *
  [`close]]
where logic_p is the type inferred at log_ch (in the bottom of the center column).

Related work

Technical backgrounds

See our draft paper.