View Source Documentation
ElixirST (Session Types in Elixir) applies session types to a fragment of the Elixir language.
It statically checks that the programs use the correct communication structures (e.g. send
/receive
) when dealing with message passing between processes.
The design decisions of ElixirST and its underlying theory are described in the following papers:
- Gerard Tabone and Adrian Francalanza. Session Fidelity for ElixirST: A Session-Based Type System for Elixir Modules. ICE 2022. (doi, pdf)
- Gerard Tabone and Adrian Francalanza. Session Types in Elixir. AGERE 2021. (doi, pdf)
- Gerard Tabone and Adrian Francalanza. Static Checking of Concurrent Programs in Elixir Using Session Types. Technical report, 2022. (pdf)
Example
To session typecheck modules in Elixir, add use ElixirST
and include any assertions using the annotations @session
and @dual
preceding any public function (def
). The following is a simple example
, which receives one label (?Hello()
):
defmodule Example do
use ElixirST
@session "server = ?Hello().end"
@spec server(pid) :: atom()
def server(_pid) do
receive do
{:Hello} -> :ok
end
end
@dual "server"
@spec client(pid) :: {atom()}
def client(pid) do
send(pid, {:Hello})
end
end
ElixirST runs automatically at compile time (mix compile
) or as a mix task (mix sessions [module name]
):
$ mix sessions SmallExample
[info] Session typechecking for client/1 terminated successfully
[info] Session typechecking for server/0 terminated successfully
If the client sends a different label (e.g. :Hi) instead of the one specified in the session type (i.e. @session "!Hello()"
), ElixirST will complain:
$ mix sessions Examples.SmallExample
[error] Session typechecking for client/1 found an error.
[error] [Line 7] Expected send with label :Hello but found :Hi.
A (Failing) Example
In the next example, session typechecking fails because the session type !Hello()
was expecting to find a send action with {:Hello}
but found {:Yo}
:
defmodule Module2 do
use ElixirST
@session "!Hello().end"
@spec do_something(pid) :: {:Yo}
def do_something(pid) do
send(pid, {:Yo})
end
end
Output:
mix compile
== Compilation error in file example.ex ==
** (throw) "[Line 7] Expected send with label :Hello but found :Yo."
Session Types in Elixir
Session types are used to ensure correct communication between concurrent processes.
The session type operations include the following: !
refers to a send action, ?
refers to a receive action, &
refers to a branch (external choice), and +
refers to an (internal) choice.
Session types accept the following grammar:
S =
!label(types, ...).S (send)
| ?label(types, ...).S (receive)
| &{?label(types, ...).S, ...} (branch)
| +{!label(types, ...).S, ...} (choice)
| rec X.(S) (recurse)
| X (recursion var)
| end (terminate)
types =
atom
| boolean
| number
| atom
| pid
| {types, types, ...} (tuple)
| [types] (list)
The following are some session type examples along with the equivalent Elixir code.
Send
!Hello()
- Sends label:Hello
Equivalent Elixir code:
send(pid, {:Hello})
Receive
?Ping(number)
- Receives a label:Ping
with a value of typenumber
.Equivalent Elixir code:
receive do {:Ping, value} -> value end
Branch
&{ ?Option1().!Hello(number), ?Option2() }
The process can receive either
{:Option1}
or{:Option2}
. If the process receives the former, then it has to send{:Hello}
. If it receives{:Option2}
, then it terminates.Equivalent Elixir code:
receive do {:Option1} -> send(pid, {:Hello, 55}) # ... {:Option2} -> # ... end
Choice
+{ !Option1().!Hello(number), !Option2() }
The process can choose either
{:Option1}
or{:Option2}
. If the process chooses the former, then it has to send{:Hello}
. If it chooses{:Option2}
, then it terminates.Equivalent Elixir code:
send(pid, {:Option1}) send(pid, {:Hello, 55}) # or send(pid, {:Option2})
Recurse
X = &{?Stop(), ?Retry().X}
- If the process receives{:Stop}
, it terminates. If it receives{:Retry}
it recurses back to the beginning.Equivalent Elixir code:
def rec() do receive do {:Stop} -> # ... {:Retry} -> rec() end end
Using ElixirST
Installation
The package can be installed by adding elixirst
to your list of dependencies in mix.exs
:
def deps do
[
{:elixirst, "~> 0.8.3"}
]
end
Documentation can be found at https://hexdocs.pm/elixirst.
Use in Elixir modules
To session typecheck a module, link the ElixirST library using this line:
use ElixirST
Insert any checks using the @session
attribute followed by a function that should be session typechecked, such as:
@session "pinger = !Ping().?Pong()"
def function(), do: ...
The @dual
attribute checks the dual of the specified session type.
@dual "pinger"
# Equivalent to: @session "?Ping().!Pong()"
Other examples can be found in the examples
folder.
Cite
Feel free to cite ElixirST as follows (or use .bib file):
Francalanza, A., & Tabone, G. (2023). ElixirST: A session-based type system for Elixir modules. Journal of Logical and Algebraic Methods in Programming, 135, 100891. https://doi.org/10.1016/j.jlamp.2023.100891
Acknowledgements
Some code related to Elixir expression typing was adapted from typelixir by Cassola (MIT licence).
This project is licenced under the GPL-3.0 licence.