The project aims to ensure the correctness of concurrent programs, given their complex behaviour. Despite being primarily known for its functional programming features, OCaml also provides support for imperative programming through the use of references, which are mutable variables enabling the sharing of states. However, their use in functional programming could introduce software bugs typically associated with non-deterministic behaviour. This makes it essential to verify the correctness of concurrent programs that use references.
The project sought to address these challenges through runtime verification, which is a technique that monitors OCaml program execution and checks for adherence to safety properties. This technique involves instrumenting the program to generate a trace that captures information about the events occurring during the OCaml program execution, including reads, writes, and reference initialisations. Hence, in simpler terms, whenever a read, write or initialisation event occurs during program execution, it is automatically recorded and reported in the trace text file through the instrumentation technique. This trace is reported and saved in a text file, using file channels in OCaml.
In addition to the above, a data structure was implemented to represent the trace of an OCaml program into a list of events, enabling monitoring and analysis to capture the behaviour of the program. For the purpose of capturing and organising the events, the data structure implemented in OCaml reports the event types and reference types; the event types would represent different program actions such as initialisation, reading, and writing to a reference, while the reference types would contain specific information about the reference, including its name and current value. The data structure enables tracking of the program’s trace, which can be analysed to capture the program’s behaviour after being converted from a text file.
To formally specify the properties that the project set out to verify, the specification logic sHML was utilised. This is a syntactic subset of the Hennessy-Milner logic (HML) with recursion that specifies safety properties. The properties were expressed as sHML formulae interpreted over the states of transition models of programs being analysed. Using sHML to express the properties to be checked, the project sought to generate manually specified or automatically synthesised properties that could capture the essential program behaviour aspects, ensuring correctness despite non-deterministic behaviour.
The project applied a monitoring algorithm to check the synthesised properties against the program’s trace during execution. Once the set list of events is fed in, the monitoring algorithm returns a boolean flag. If the program’s behaviour violates any of the specified properties, the monitoring algorithm flags a false value and also reports the line number in which the trace violates the safety property. In contrast, if the property is not violated, a true value is returned.
The approach adopted in this project allows developers to pinpoint where any violations occur and identify cases where the program’s behaviour is incorrect. This tends to facilitate locating any issues found in the OCaml program towards ensuring program correctness.
Figure 1. Using runtime verification as a technique to monitor OCaml programs
Student: Emma Sciberras
Supervisor : Prof. Adrian Francalanza