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 metadatas

Cited literature [58 references]  Display  Hide  Download

https://hal.inria.fr/hal-01882414
Contributor : Yliès Falcone <>
Submitted on : Thursday, September 27, 2018 - 8:06:38 AM
Last modification on : Friday, October 25, 2019 - 1:21:00 AM
Long-term archiving on: Friday, December 28, 2018 - 1:04:45 PM

File

rv18-tutorial.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01882414, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

191

Files downloads

254