In Perfect Harmony: Orchestrating Causality in Actor-Based Systems

TL;DR

ACTORCHESTRA is a runtime verification framework for Erlang that automatically tracks causality across multiple actors, enabling detection of complex behavioral violations with minimal manual intervention.

Contribution

It introduces a novel instrumentation and specification language for multi-actor causal property monitoring in Erlang systems.

Findings

Effective detection of complex behavioral violations in real-world systems

Acceptable runtime overhead for causal monitoring

Automated translation of properties into executable monitors

Abstract

Runtime verification has gained popularity as a lightweight approach for increasing assurance in systems under scrutiny. Performing runtime checks enables dynamic monitoring and alerts for unexpected behavior, thereby improving reliability and correctness. Actor-based systems present significant challenges for runtime verification. Properties frequently span multiple actors with complex causal dependencies, while nondeterministic message interleavings can obscure execution semantics. Moreover, most existing monitoring tools are designed for single-process behavior. This paper presents ACTORCHESTRA, a runtime verification framework for Erlang that automatically tracks causality across multi-actor interactions. The framework instruments Erlang systems that comply with OTP guidelines via targeted code injection. This method establishes the orchestration infrastructure required to track causal relationships between actors without requiring manual modifications to the target system. To ease the specification of multi-actor properties, the framework provides WALTZ, a specification language that automatically compiles properties into executable Erlang monitors that integrate with the instrumented system. Three case studies demonstrate ACTORCHESTRA's effectiveness in detecting complex behavioral violations in real-world actor systems. A performance evaluation quantifies the runtime overhead of the monitoring infrastructure and analyzes the trade-offs between added safety guarantees and execution costs.