Sound Concurrent Traces for Online Monitoring Technical Report
Chukri Soueidi, Ylies Falcone
TL;DR
The paper addresses online verification of concurrent programs where total-order traces can yield unsound verdicts due to concurrency. It presents a non-blocking vector-clock algorithm that can run on the fly (asynchronously or synchronously) to produce sound representative traces, using per-thread clocks $VC$ and tree clocks to reduce join/copy costs. To guarantee sound monitors for total-order formalisms, it defines a monitorability framework based on a causal dependence relation $\mathcal{D}$ extracted from the monitor automaton and requires the necessary ordering $\mathrm{tno}(t,\mathcal{D})$ in traces. The FACTS tool implements these ideas on the JVM, instrumenting Java bytecode to emit sound/faithful traces and warn about non-monitorable traces; empirical evaluation on real and synthetic benchmarks shows effective detection of ordering deficiencies with acceptable overhead and improved performance via tree clocks.
Abstract
Monitoring concurrent programs typically rely on collecting traces to abstract program executions. However, existing approaches targeting general behavioral properties are either not tailored for online monitoring, are no longer maintained, or implement naive instrumentation that often leads to unsound verdicts. We first define the notion of when a trace is representative of a concurrent execution. We then present a non-blocking vector clock algorithm to collect sound concurrent traces on the fly reflecting the partial order between events. Moreover, concurrent events in the representative trace pose a soundness problem for monitors synthesized from total order formalisms. For this, we extract a causal dependence relation from the monitor to check if the trace has the needed orderings and define the conditions to decide at runtime when a collected trace is monitorable. We implement our contributions in a tool, FACTS, which instruments programs compiling to Java bytecode, constructs sound representative traces, and warns the monitor about non-monitorable traces. We evaluate our work and compare it with existing approaches.