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 'aAn 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]]logic_p is the type inferred at log_ch (in the bottom of the center column).