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.
翻译:并发程序的监控通常依赖于收集轨迹来抽象程序执行。然而,针对一般行为属性的现有方法要么不适合在线监控,要么已不再维护,或者实现了可能导致结果不可靠的简单化插桩技术。我们首先定义了轨迹何时能代表并发执行的概念,接着提出了一种非阻塞向量时钟算法,用于实时收集反映事件间偏序关系的可靠并发轨迹。此外,代表性轨迹中的并发事件对基于全序形式化方法生成的监控器构成了可靠性问题。为此,我们从监控器中提取因果关系依赖关系,以检查轨迹是否具有所需的排序,并定义了在运行时判定已收集轨迹是否可监控的条件。我们将这些贡献实现为工具FACTS,该工具对编译为Java字节码的程序进行插桩,构建可靠的代表性轨迹,并向监控器发出不可监控轨迹的警告。我们评估了该工作,并与现有方法进行了比较。