Skip to Main content Skip to Navigation
Conference papers

Can We Monitor All Multithreaded Programs?

Abstract : Runtime Verification (RV) is a lightweight formal method which consists in verifying that an execution of a program is correct wrt a specification. The specification formalizes with properties the expected correct behavior of the system. Programs are instrumented to extract necessary information from the execution and feed it to monitors tasked with checking the properties. From the perspective of a monitor, the system is a black box; the trace is the only system information provided. Parallel programs generally introduce an added level of complexity on the program execution due to concurrency. A concurrent execution of a parallel program is best represented as a partial order. A large number of RV approaches generate monitors using formalisms that rely on total order, while more recent approaches utilize formalisms that consider multiple traces. In this tutorial, we review some of the main RV approaches and tools that handle multithreaded Java programs. We discuss their assumptions, limitations, ex-pressiveness, and suitability when tackling parallel programs such as producer-consumer and readers-writers. By analyzing the interplay between specification formalisms and concurrent executions of programs, we identify four questions RV practitioners may ask themselves to classify and determine the situations in which it is sound to use the existing tools and approaches.
Complete list of metadata

Cited literature [58 references]  Display  Hide  Download
Contributor : Yliès Falcone Connect in order to contact the contributor
Submitted on : Thursday, September 27, 2018 - 8:06:38 AM
Last modification on : Thursday, October 21, 2021 - 3:45:25 AM
Long-term archiving on: : Friday, December 28, 2018 - 1:04:45 PM


Files produced by the author(s)


  • HAL Id : hal-01882414, version 1



Antoine El-Hokayem, Yliès Falcone. Can We Monitor All Multithreaded Programs?. RV 2018 - 18th International Conference on Runtime Verification, Nov 2018, Limassol, Cyprus. pp.1-24. ⟨hal-01882414⟩



Record views


Files downloads