Operational Semantics of Process Monitors

TL;DR

This paper develops an SOS-style operational semantics for CSPe, a runtime monitor specification language, to improve understanding, correctness, and further study of its properties and implementation.

Contribution

It introduces the first operational semantics for CSPe, explicitly handling failures, enabling better correctness proofs and further research.

Findings

Operational semantics for CSPe successfully models explicit failures.

Provides a foundation for correctness and optimization of CSPe implementations.

Facilitates further study of CSPe's properties and runtime verification applications.

Abstract

CSPe is a specification language for runtime monitors that can directly express concurrency in a bottom-up manner that composes the system from simpler, interacting components. It includes constructs to explicitly flag failures to the monitor, which unlike deadlocks and livelocks in conventional process algebras, propagate globally and aborts the whole system's execution. Although CSPe has a trace semantics along with an implementation demonstrating acceptable performance, it lacks an operational semantics. An operational semantics is not only more accessible than trace semantics but also indispensable for ensuring the correctness of the implementation. Furthermore, a process algebra like CSPe admits multiple denotational semantics appropriate for different purposes, and an operational semantics is the basis for justifying such semantics' integrity and relevance. In this paper, we develop an SOS-style operational semantics for CSPe, which properly accounts for explicit failures and will serve as a basis for further study of its properties, its optimization, and its use in runtime verification.

Equations

$$eT$$

$$T(e)$$

$$\varnothing |{|}_{E}T$$

$$T_1|{|}_E{T}_2$$

$$[[\text{STOP}]]$$

$$[[\text{FAIL}]]$$

$$[[?x:E\to P]]$$

Full text

1 Introduction

Specification-based runtime monitoring [5] checks a program’s execution trace against a formal specification. Often more rigorous than testing due to the presence of a formal specification, this technique is also computationally much cheaper than formal verification methods like model checking, as it only needs to look at concrete program runs with instrumentation. $\text{CSP}_{E}$ [10] is a language based on Hoare’s Communicating Sequential Processes [6] for developing the formal specification. Unlike many other languages in this niche, $\text{CSP}_{E}$ can directly express concurrency. Moreover, it builds up the specification in a bottom-up manner by composing smaller, interacting components, helping to model complex behavior.

$\text{CSP}_{E}$’s main appeal as a specification language, compared to plain CSP, is a FAIL construct that signals a global failure, aborting all processes in the model at once. This construct can be used like assert(false) in C or Java, allowing to code invariants that mark some states as (should-be) unreachable. By contrast, deadlocks and livelocks, the conventional notions of failure in CSP, affect only the deadlocked or livelocked process(es). These failures are thus very difficult to propagate into a failure for the entire system, as desired for assertion failures. However, the semantics of how FAIL propagates throughout the model requires special treatment. Because the propagation preempts all other activities, normal execution rules must apply only when FAIL is not currently propagating. This is a negative constraint, which is generally problematic [4].

While earlier work [10] demonstrated a trace semantics and a reasonably efficient implementation for $\text{CSP}_{E}$, an operational semantics has been lacking. Developing an operational semantics is highly desirable for several reasons. Firstly, though a trace semantics more naturally defines the set of behaviors (i.e. traces) that comply with a $\text{CSP}_{E}$ specification, an operational semantics more directly defines the implementation. Secondly, process algebras admit multiple denotational semantics capturing different aspects of operationally defined behavior [3]. Investigating the full spectrum of such semantics requires an operational semantics. Finally, an operational semantics provides a more accessible presentation of the semantics than denotational semantics.

1.1 Contributions

In this paper, after reviewing the syntax and trace semantics of $\text{CSP}_{E}$ (Section 2), we present the following contributions.

• •

We define an operational semantics in SOS format [8], which properly captures the propagation of FAIL while avoiding the complexities of rules with negative premises (Section 3).

• •

We prove that the operational semantics induces the previously published trace semantics (Section 4).

2 Syntax and Trace Semantics of $\text{CSP}_{E}$

This section reviews the syntax and trace semantics of $\text{CSP}_{E}$. Figure 1 presents the syntax. A $\text{CSP}_{E}$ term represents a process, which is an entity that successively emits events drawn from an alphabet $\Sigma$. Terms are built from the following constructs, with the indicated meanings. For a thorougher explanation, see [10].

• •

The stuck term STOP does not emit anything.

• •

The failing term FAIL aborts all processes.

• •

Prefix $?x:E\rightarrow P$ chooses and emits an event $e\in E$, then executes $[e/x]P$.

• •

Choice $P\mathrel{\Box}Q$ executes $P$ or $Q$, whichever manages to emit something first.

• •

Parallel composition $P\mathrel{||_{E}}Q$ executes $P$ and $Q$ in parallel. Their events are interleaved arbitrarily, except events in $E$ are synchronized.

An event set $E$ can be specified by any computable function parametrized by the $x$’s bound by surrounding prefix operators.

In this short paper, we omit recursion and the terminating action $\checkmark$ in the interest of conciseness. This paper’s focus is on analyzing FAIL, and $\checkmark$ complicates the presentation substantially without adding anything of conceptual significance. Recursion seems to be similar, though it is still under investigation.

Figure 2 presents the trace semantics. A trace is a (possibly empty) sequence of events, and $\Sigma^{*}$ is the set of all traces. The concatenation of traces $s$ and $t$ is written $st$. A trace set is any prefix-closed set of traces, which can be empty, unlike in conventional process algebras. The trace semantics of $\text{CSP}_{E}$ assigns to each term $P$ a trace set $\llbracket P\rrbracket$, which is intuitively the set of traces $P$ can emit.

The semantic map uses some operations on trace sets. If $T$ is a trace set, $eT$ prepends $e$ to all members of $T$ and adjoins $\varepsilon$, while $T(e)$ discards all traces in $T$ that do not start with $e$ and drops the leading $e$ from all remaining traces. The $\mathrel{||_{E}}$ operator is defined by eqs. 1 and 2. Though significantly simplified, these equations are equivalent to the ones found in [10] modulo the absence of $\checkmark$. In [10], this operator was defined “coinductively”, which was correct but misleading. Formally, by the Knaster-Tarski Theorem, the defining equations (1) and (2) have a greatest solution in the complete lattice of total binary functions on TraceSets ordered by point-wise inclusion, which was taken to be $\mathrel{||_{E}}$. However, if $\mathrel{||_{E}}^{\prime}$ and $\mathrel{||_{E}}^{\prime\prime}$ are any two solutions of these equations, then for any $T_{1}$ and $T_{2}$, every trace in $T_{1}\mathrel{||_{E}}^{\prime}T_{2}$ is also in $T_{1}\mathrel{||_{E}}^{\prime\prime}T_{2}$, by straightforward induction on the trace’s length. Thus, the solution is unique, and $\mathrel{||_{E}}$ is this unique solution.

Lemma 1

$\mathrel{||_{E}}$* is continuous, i.e. $\left(\bigcup S_{1}\right)\mathrel{||_{E}}\left(\bigcup S_{2}\right)=\bigcup_{T_{1}\in S_{1},T_{2}\in S_{2}}T_{1}\mathrel{||_{E}}T_{2}$.*

Proof

The defining equations (1) and (2) preserve continuity, so in fact the Knaster-Tarski construction can be carried out in the space of continuous binary operators, which is also a complete lattice under point-wise inclusion.

3 Operational Semantics

This section presents the operational semantics. The semantics is given in Figure 3, which defines internal transitions $P\mathrel{\overset{a}{\mapsto}}Q$ between terms. Some transitions do not emit events but instead emit the silent action $\tau$. A visible transition $P\mathrel{\overset{s}{\Mapsto}}Q$ happens when $P$ internally transitions to $Q$ in zero or more steps, and the non-$\tau$ actions it emits along the way forms $s$.

The main challenge in this semantics is capturing the propagation of FAIL. For example, in $P\mathrel{||_{\varnothing}}\textit{FAIL}$, the $P$ must not be allowed to keep emitting events, for then $P$ could do so indefinitely, withholding the propagation of FAIL. Instead, FAIL should kill all processes including $P$, transitioning the whole term to FAIL. To achieve this effect, the usual rule that allows the left operand to transition must apply only when the right operand is not failing. This constraint is tricky to capture because it is a negative constraint.

In our semantics, the constraint is captured by the viability annotation $\hat{P}$. This annotation restricts the range of the metavariable $\hat{P}$ to exclude doomed terms, i.e. terms for which transitioning to FAIL has become inevitable and are now propagating FAIL within themselves. These annotations are placed so that when a term is doomed, rules that propagate FAIL become the only applicable ones, thus forcing the propagation to take place.

Proposition 1

A doomed process always transitions to FAIL while emitting nothing but $\tau$.

Proof

$D\mathrel{\overset{a}{\mapsto}}P$* implies $a=\tau\wedge P\in\textit{Doomed}\wedge|D|>|P|$, where $|P|$ denotes term size, by induction on $D$. Thus, a doomed term can only $\tau$-transition, and only finitely many times, while staying doomed. Another induction shows $\forall D\neq\textit{FAIL}.\ \exists D^{\prime}.\ D\mathrel{\overset{\tau}{\mapsto}}D^{\prime}$, so a doomed term keeps transitioning until it reaches FAIL.*

4 Correspondence Between the Semantics

This section establishes a correspondence between the two semantics: a process’ denotation is precisely the set of traces it can emit, up to but not including any transitions that doom the process. This means that the monitor comparing a system to $P$ can declare a failure as soon as the system’s trace strays out of $\llbracket P\rrbracket$.

Theorem 4.1

$\llbracket P\rrbracket=\{s\mid\exists M.\ P\mathrel{\overset{s}{\Mapsto}}M\not\in\textit{Doomed}\}$.

A special case of this theorem is particularly illuminating: the doomed set is precisely the set of terms with empty trace sets, corresponding to the fact that doomed terms silently transition to FAIL.

Proposition 2

$P\in\textit{Doomed}\Longleftrightarrow\llbracket P\rrbracket=\varnothing$.

Proof

Induction on $P$.

Furthermore, trace sets faithfully follow non-silent transitions, in that the traces which follow an event $e$ in $\llbracket P\rrbracket$ are precisely the traces of terms $Q$ that follow $P$ after a sequence of transitions that emit $e$.

Lemma 2

$\llbracket P\rrbracket(e)=\bigcup_{P\mathrel{\overset{e}{\Mapsto}}Q}\llbracket Q\rrbracket$.

Proof

Induction on the size of $P$, where event sets do not count toward size, e.g. $|?x:E\rightarrow P^{\prime}|:=|P^{\prime}|+1$. This way, $|[e/x]P^{\prime}|=|P^{\prime}|$, so when $P=(?x:E\rightarrow P^{\prime})$, the inductive hypothesis applies to $[e/x]P^{\prime}$, despite it not being a subterm. Several lemmas are needed along the way, two of which are of particular note. Take for example $P=P_{1}\mathrel{||_{E}}P_{2}$ with $\llbracket P_{1}\rrbracket,\llbracket P_{2}\rrbracket\neq\varnothing$ and $e\in E$. Inductive hypotheses give $\llbracket P\rrbracket(e)=(\bigcup_{P_{1}\mathrel{\overset{e}{\Mapsto}}Q_{1}}\llbracket Q_{1}\rrbracket)\mathrel{||_{E}}(\bigcup_{P_{2}\mathrel{\overset{e}{\Mapsto}}Q_{2}}\llbracket Q_{2}\rrbracket)$. Then, continuity (Lemma 1) lets us commute the $\bigcup$ and $\mathrel{||_{E}}$, equating this to $\bigcup_{P_{1}\mathrel{\overset{e}{\Mapsto}}Q_{1},P_{2}\mathrel{\overset{e}{\Mapsto}}Q_{2}}(\llbracket Q_{1}\rrbracket\mathrel{||_{E}}\llbracket Q_{2}\rrbracket)$. Then, a lemma characterizing those $Q$ with $P\mathrel{\overset{e}{\Mapsto}}Q$ equates this to $\bigcup_{P\mathrel{\overset{e}{\Mapsto}}Q}\llbracket Q\rrbracket$.

Theorem 4.1 is a straightforward consequence of these facts.

Proof (of Theorem 4.1)

We show $s\in\llbracket P\rrbracket\Longleftrightarrow\exists Q.\ P\mathrel{\overset{s}{\Mapsto}}Q\not\in\textit{Doomed}$ by induction on $s$. For the base case, $\varepsilon\in\llbracket P\rrbracket\Longleftrightarrow P\not\in\textit{Doomed}$ by Proposition 2. If $P\not\in\textit{Doomed}$, then $P\mathrel{\overset{\varepsilon}{\Mapsto}}P\not\in\textit{Doomed}$, and if $P\in\textit{Doomed}$, then $P$ can only transition inside Doomed as noted in the proof of Proposition 1. For the inductive step, $s$ breaks down as $s=es^{\prime}$, and $s\in\llbracket P\rrbracket\Longleftrightarrow s^{\prime}\in\llbracket P\rrbracket(e)$. By Lemma 2, this is equivalent to having $s^{\prime}\in\llbracket P^{\prime}\rrbracket$ and $P\mathrel{\overset{e}{\Mapsto}}P^{\prime}$ for some $P^{\prime}$, which by inductive hypothesis is equivalent to $\exists P^{\prime},Q.\ P\mathrel{\overset{e}{\Mapsto}}P^{\prime}\mathrel{\overset{s^{\prime}}{\Mapsto}}Q\not\in\textit{Doomed}$.

5 Related Works

The main issue with $\text{CSP}_{E}$ semantics is the propagation of FAIL, which entails the negative constraint that normal computation rules apply only if FAIL-propagation rules do not. Negative premises of the form $P\not\mathrel{\overset{a}{\mapsto}}$ come quite naturally as a means for codifying such constraints, but negative premises are generally quite problematic. A transition relation satisfying negative rules may be not-existent, or non-unique, with no obvious guiding principle (such as minimality) in choosing the “right” one. Some formats do guarantee well-definedness, such as GSOS with the witnessing constraint [2] and ntyft/ntyxt [4]. But even then, negative rules tend to betray desirable properties such as compositionality of some forms of bisimulation [1].

Our approach exploits the fact that we only have a very specific negative constraint – the absence of doomed subprocesses – and encodes it with a restriction on the range of metavariables in transition rules. With trick, we manage to avoid negative premises altogether, essentially turning the system into a positive one. This approach is very commonly employed, e.g. in reduction rules for the call-by-value $\lambda$ calculus [7], where the argument in a function application should be evaluated only if the function expression cannot be evaluated any further.

We identify FAIL-induced failures by transitions into FAIL, but an alternative approach would be to have FAIL emit a special event $\digamma$, just as termination is signalled by $\checkmark$. Though we have not pursued this idea in detail, the central concern there will be to give $\digamma$ higher priority than all other events. Prioritized transition also involves a negative constraint but is known to be quite well-behaved, being translatable to plain CSP [9]. At the moment, it is not clear if FAIL propagation can be translated to the prioritized-transition primitive in [9].

6 Conclusion

We gave an operational semantics for $\text{CSP}_{E}$ that adequately captures the behavior of FAIL, the global failure operator, with positive operational rules. This semantics induces the previously defined trace semantics. As noted in the introduction, this development enables studies of other types of denotational semantics, while informing the implementation. An interesting direction of future work is to see if FAIL can be specified by priorities, and if that approach yields better-behaved semantics.

Acknowledgment

The authors would like to thank Yoshinao Isobe for comments on an earlier draft of this paper and stimulating discussions.