Checking Consistency of Event-driven Traces

TL;DR

This paper introduces an axiomatic approach to verify the consistency of event-driven program traces, analyzes its computational complexity, and provides a practical tool for efficient checking in specific cases.

Contribution

It formalizes an axiomatic semantics for event-driven programs, proves the NP-completeness of trace consistency checking, and identifies a polynomial-time fragment with a prototype implementation.

Findings

Consistency checking is NP-complete in general.

Without nested posting, checking is polynomial-time.

Prototype tool performs well on various benchmarks.

Abstract

Event-driven programming is a popular paradigm where the flow of execution is controlled by two features: (1) shared memory and (2) sending and receiving of messages between multiple handler threads (just called handler). Each handler has a mailbox (modelled as a queue) for receiving messages, with the constraint that the handler processes its messages sequentially. Executions of messages by different handlers may be interleaved. A central problem in this setting is checking whether a candidate execution is consistent with the semantics of event-driven programs. In this paper, we propose an axiomatic semantics for eventdriven programs based on the standard notion of traces (also known as execution graphs). We prove the equivalence of axiomatic and operational semantics. This allows us to rephrase the consistency problem axiomatically, resulting in the event-driven consistency problem: checking whether a given trace is consistent. We analyze the computational complexity of this problem and show that it is NP-complete, even when the number of handler threads is bounded. We then identify a tractable fragment: in the absence of nested posting, where handlers do not post new messages while processing a message, consistency checking can be performed in polynomial time. Finally, we implement our approach in a prototype tool and report on experimental results on a wide range of benchmarks.