Sound Concurrent Traces for Online Monitoring Technical Report
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要