Elarva : runtime verification for message passing concurrency

Abstract

In the era of multicores processors, software systems have to be highly concurrent to gain performance out of hardware. However verifying the correctness of concurrent applications is more difficult due to the high degree of non-determinism introduced from interaction with the environment and unpredictable order of scheduling. The industry demands new methodologies and tools that help analyse the behavior of concurrent systems. Traditional verification techniques such as model checking and testing, suffer in cases where the system is sufficiently large and lack of coverage respectively. Runtime verification is a good trade-off between model checking and testing because it only considers execution traces that are finite and can access certain information which is only available at systems runtime. In this thesis we examined ways how we can verify the correctness of a message passing concurrent system by runtime verification with the main difficulty found was how to tackle the instrumentation of the monitoring code with the target system. To aid us present the results obtained from the investigation we created ELARVA, a runtime verification framework for message passing concurrency. The main formal notations used to specify properties for runtime verification in the literature range from variations and extensions of LTL, duration calculus and automata. We opted for DATEs, a logic based on symbolic automata. This logic is designed for runtime verification and offers a high degree of expressivity since it requires much less computational resources than having a logic to be decidable over all execution paths. We tackled instrumentation via Erlang tracing mechanism which gave us an elegant way how to capture events without modifying the target system. The monitoring is done asynchronously to the target system. Upon violation detection we have the possibility to either take an action via the Supervisor behaviour, which allows us to the restart the target system to limit the damage, or to trigger some built-in recovery strategies. We also try to minimise the induced overhead by adopting a distributed monitoring approach where the target system runs on Erlang node while the monitoring code resides on a different Erlang node and on a separate machine with dedicated hardware. We applied a real-life scenario case-study to ELARVA to test the tool in terms of expressivity and correctness. We were able to monitor interesting properties and managed to detect all induced errors. We also managed to handle violations by restarting the system through the use of the Supervisor behaviour. We also conducted a qualitative measure between ELARVA and Exago, an offline monitoring tool implemented in Erlang, to highlight the strengths and weaknesses of both tools and the main differences between them. Finally we presented a performance benchmark which gave us a measure of the overhead induced by the monitoring code and proved that in certain situations we can minimise this overhead by using a distributed monitoring approach.