TOASTER
Timeout Asynchronous Session Types for Erlang
This is a blog post to accompany the tool presented in the paper [Erlang on TOAST] at the Erlang Workshop 2024.
Overview
The tool presented in the paper is the first development of a toolchain for generating correct-by-construction Erlang programs from TOAST, which are behavioural types. Behavioural types are a kind of formal model for describing the interaction structure of a concurrent system while providing guarantees of their behavioural properties. In the case of session types, the properties we are typically interested in providing are communication safety, deadlock freedom and ultimately, progress – whereby progress means that the system is guaranteed to either terminate successfully or continue to make progress indefinitely.
Timeout Asynchronous Session Types
See another [not-yet-written] blog post where we discuss TOAST in more detail.
Erlang on TOAST
todo
Toolchain Overview
Erlang on TAOST
todo
New Developments
Mapping TOAST Processes to Intput Protocol Notation
This is a tool I have developed that takes a TOAST process represented in Erlang syntax and automatically maps it to the input notation of the toolchain presented in [Erlang on TOAST]. In future work, I would like to extend this to be reversible.
TOAST Type-checker
In the original TOAST paper we presented the syntax of TOAST types and processes. In the extended TOAST paper we presented the typing system for TOAST.
In this update, I have implemented the typing system of TOAST into Erlang.
To handle the evaluation of the timing constraints and clocks, to tool uses erlport to call a python script (z3_interface.py) which in turn uses z3 to solve it.
Specifically, the Erlang side of the tool builds strings of python code, and then passes these to the z3_interface.py program which imports z3 and executes the code.
The approach used is rather rudimentary but effective in this case.
There are some limitations of this approach:
- Certain type-checking rules require a judgement to be evaluated forall over a continuous range of time (See rules [Del-\delta], [VRecv] and [DRecv]). Since we have not actually implemented the type-checking rules into z3, and are in Erlang, we simply define a few macros to determine the resolution/fine-grained-ness of the evaluation. Macro
DECIMAL_PRECISIONcan be set to determine how many decimal places the program will evaluate such expressions. - Additionally, in a similar vein, there are some instances where we would be required to evaluate judgements for the continuous range up to
infinity. In such cases, we once again defer to a macroINFINITYwhich determines the value the program will evaluate until. Naturally, this value should be greater than any constants in any of the timing-constraints. - Finally, we do not enforce or check the actual data types of the messages exchanged by the process and type. This is rather intentional, since we do not actually enforce these types in the runtime monitors, and only care about the labels. Perhaps if in the future we were to try and integrate parts of our toolchain into Erlang’s dialyzer then this would be something to consider.
Future Plans
Extracting TOAST Protocols from TOAST Types
Since the typing system of TOAST has been implemented, it is now possible to determine if a given TOAST process will exhibit desirable behaviour guaranteed by the TOAST type.
The next step in the toolchain would be to either (a) assist the user in designing TOAST processes and checking they are well-typed against a TOAST type; or, (b) develop a tool to automatically derive the possible TOAST processes from a given TOAST types.
The former is a time investment that would not really serve anyone much use, since it would still require the user to understand how to design not only the TOAST types, but the TOAST processes too.
While the latter circumvents the issue of manually designing a TOAST process, and is the option we are most interested in pursuing. To begin, we would likely develop a tool for automatically deriving the maximal implementation of a given TOAST type, and then provide a suite of options for how to reduce this implementation such that it remains well-typed. We already have some ideas and sketches on paper for some of the conditions for reducing the maximal implementation, but this, on the whole, is not currently under development.
Updating the Monitors
Currently, we automatically generate a monitor specification from the given TOAST specification, which itself has been obtained from the mapping of some well-typed TOAST process.
Overall, it would be more fitting to use the actual TOAST type as the specification protocol for the runtime monitor. Indeed, this was originally the goal when we first started developing the tool (i.e., to go from types to programs) but, due to the difficulties encountered described in the paper, it was more appropriate at the time to go from TOAST processes.
Nevertheless, if we do develop the toolchain further to facilitate the extraction of TOAST processes from TOAST types, then the original paper’s vision of going from TOAST types to Erlang programs would be realisable. In such a case, we would like to extend the existing runtime monitors to be able to take the TOAST type as their protocol specifically. It is likely that this will actually take the form of the “maximal implementation” TOAST process of a given TOAST type, which once again, avoids the issues outlined in the paper regarding diagonal constraints and other complicated constraints.
Furthermore, it would be interesting to investigate the feasibility of implementing diagonal constraints in Erlang, as described in TOAST types. This would lift the primary limitation of our toolchain. However, I am yet to find some useful concrete examples of diagonal-constraints in real concurrent systems, so this is of lower priority.
Other Ideas (not in diagram)
- Implement TOAST into Erlang’s dialyzer in a similar way to the Session Type provider for F#. (I cannot find it now, but I remember seeing a video demo of an eclipse extension using this work.)