Concurrent languages present challenges for software correctness since standard approaches, such as unit testing, can be ineffective. This is due to the state-explosion problem, whereby having concurrent processes exponentially increases the number of states that would need to be verified. One approach to verifying the correctness of a concurrent program is runtime verification, which allows a monitor to observe the behaviour of a program as it executes. It would be necessary to supply a correctness specification to ensure that the monitor would be able to make a verdict regarding the correctness of the monitor.
In this project, the above-mentioned approach was implemented for Elixir, a concurrent programming language, by extending the functionality of an existing monitoring framework for Erlang, named detectEr. At the time of writing, detecEr only supported outline monitoring for Elixir, where the monitor would run alongside the target program, observing events without interference and not inline monitoring (where the monitor is woven into the source of the target program). While outline monitoring may offer better performance, inline monitoring would be useful in closed-source software that would need to be shared. This is outlined in Figure 1.
To implement inline functionality, it was necessary to extract and parse Elixir program abstract syntax trees and identify key nodes, such as those spawning processes or facilitating inter-process communication. This made it possible to weave the monitor code into the original source code as shown in Figure 2. Once this functionality was implemented, more testing was carried out to assess the feasibility of applying a monitor to an Elixir program, in terms of overhead and program disruption.
Figure 1. Outline monitor (left) and inline monitor (right)
Figure 2. Original abstract syntax tree (left) and woven abstract syntax tree (right)
Student: Paul Gauci
Supervisor : Prof. Adrian Francalanza