Keywords

1 Do You Want to Know a Secret

In the Cockaigne of software development, programs are verified using a smorgasbord of pre-deployment techniques, and executed only when their correctness is ascertained. Reality, however, tells a different story. Mainstream verification practices, including testing [47], only reveal the presence of errors [29]. Exhaustive approaches like model checking [41] are laborious to use, e.g. building effective program models is non-trivial, and known to suffer from state explosion problems [27]. Other methods such as type systems [48] are intentionally lightweight to prevent disrupting the software development lifecycle; this, in turn, limits their precision since type-based analyses occasionally rule out well-behaved programs. Present-day software poses even more challenges. Static verification often relies on having access to the program source code, which is not necessarily available when software is constructed from libraries or components subject to third-party restrictions. Moreover, modern applications are increasingly developed in decentralised fashion, where the constituent parts are not always known pre-deployment. This tends to increase both the complexity of software and the resources required to verify it, while at the same time, decreasing the time available to conduct its verification. Lately, with the availability of large data volumes, cutting-edge software components rely on machine learning to adapt their behaviour without the need to be explicitly programmed. Analysing these types of software artifacts statically is difficult, not least because their internal representation is notoriously hard to understand.

Although the proverbial correctness cake cannot be had and eaten, slices of it may still be savoured after the program has been deployed. In certain cases, post-deployment techniques such as Runtime Verification (RV) [20, 37] can be used instead of, or in tandem with, static techniques to increase correctness assurances about a program or System under Scrutiny (SuS). RV uses monitors—computational entities consisting of logically-distinct instrumentation and analysis units—to observe the execution of the SuS. Analysers, i.e., sequence recognisers [13], are typically synthesised automatically from formal descriptions of correctness properties expressed in a specification logic.

When devising a RV tool, substantial effort is focussed on the specification language that is used to describe correctness properties, and the synthesis procedure which generates the analysis that runtime checks these properties [6, 20, 45]. Arguably, less attention is given to the instrumentation aspect, particularly, how the SuS is equipped to run with monitors, and the manner in which the computation of the SuS is extracted and reported for analysis. There is no one-size-fits-all solution to these challenges. For instance, inline instrumentation—the de facto technique employed by state-of-the-art RV [20, 34]—relies on access to the program source or unobfuscated binary, thus obliging the RV monitors to be expressed in the same language as that of the SuS. The hallmark of a flexible RV tool is, therefore, its ability to support various instrumentation techniques to cater for the different scenarios where RV is used. The RV tool should also provide a common interface for describing what properties should be verified, agnostic of the underlying instrumentation mechanism dealing with the technicalities of how the verification is performed. This contributes to lowering the learning curve of the tool and facilitate its adoption.

This paper presents the RV tool detectEr that addresses the analysis and instrumentation aspects of runtime monitoring. Our tool targets asynchronous component systems. It automatically synthesises correct analyser code from properties expressed in terms of the monitorable safety fragment of the modal \(\mu \)-calculus. Since the correctness of the synthesised analysers is studied in prior work (see [1, 5, 17, 39]), our account elaborates on the usability and instrumentation aspects of the tool. detectEr, developed on top of the Erlang [15, 26] ecosystem, supports three instrumentation methods to cater for different SuS set-ups:

  • Inline: targets programs written in the Erlang language;

  • Outline: accommodates program binaries that are compiled for and run on the Erlang Virtual Machine (EVM), but whose source code is unavailable;

  • Offline: analyses recorded runs of programs that may execute outside the EVM.

We show how, from the same correctness specifications, detectEr is able to runtime monitor system components using these different instrumentation methods.

The paper is structured as follows. Section 2 introduces our running example that captures the typical interaction between concurrent processes, along with useful properties one may wish to runtime check on such systems. Sections 3 and 4 focus on the specification logic used by detectEr and how this is synthesised into executable analysis code. Section 5 summarises the role the instrumentation has with respect to the runtime analysis, and the mechanism detectEr employs to identify the SuS components in need of monitoring. Sections 6–8 overview the three instrumentation methods mentioned above, while Sect. 9 concludes.

2 A Day in the Life

We consider an idiomatic calculator server that handles client requests for arithmetic computation. Our server can be naturally expressed as an actor (process) [12] that blocks, and waits for client requests sent as asynchronous messages. These messages are addressed to the server using its unique process ID (PID), and deposited in its mailbox that buffers multiple client requests. The server unblocks upon consuming a message from the mailbox. In our client-server protocol, messages contain the type of operation to be executed on the server, its arguments (if applicable), and the client PID to whom the corresponding server reply is addressed.

Fig. 1.
figure 1

Our calculator server and its abstraction in terms of symbolic actions

Full size image

Our calculator server is implemented as the Erlang module, calc_server, in Fig. 1a. The server logic is encapsulated in the function loop(Tot) that is forked to execute as an independent process by the launcher invoking start(), line 1. Processes in Erlang are forked via the built-in function spawn(), parametrised on line 1 by the module name, calc_server, the name of the function to spawn, loop, and the list of arguments accepted by loop, [0]. The server process reads messages from its mailbox (line 3), and pattern-matches against the three types of operations requested by clients, : (i) addition ( ) and multiplication ( ) requests carry the operands and , lines 4 and 8, and, (ii) stop ( ) requests that carry no arguments, line 12. Pattern variables and in Fig. 1a are instantiated to concrete data in client request messages via pattern matching. Every request fulfilled by the server results in a corresponding reply that is sent to the PID of the client instantiated in variable , lines 5, 9 and 13. Server replies carry the status tag, \(\textsf {ok}\) or \(\textsf {bye}\), and the result of the requested operation. Parameter Tot of loop() is used by the server to track the number of client requests serviced, and is returned in reply to a request. The server loops on and requests, incrementing Tot before recursing, lines 6 and 10; a request does not loop and terminates the server computation.

In the sequel, we focus on a system set-up consisting of one server and client to facilitate our exposition. The forked loop(Tot) function for some initial service count Tot induces a server runtime behaviour that can be abstractly described by the state transition model in Fig. 1b. Transitions between the states of Fig. 1b denote the computational steps that produce (visible) program events (e.g. event that carries the concrete payload values , and \({\textit{Tot}}\)). There are a number of correctness properties we would like such behaviour to observe. For instance, we do not control the value Tot that the server loop is launched with and, therefore, could require the invariant

figure q

Similarly, one would expect the safety properties

figure r

and “A request for adding two numbers always returns their sum” to hold, amongst others. The properties are data-dependent, which makes them hard to ascertain using static techniques such as type systems. Besides properties that reason on data, the implementation in Fig. 1a is expected to comply with control properties, such as,

figure s

that describe the message exchanges between the server and client processes. All these properties are hard to ascertain without access to the source code.

3 I Want to Tell You

We overview the detectEr specification syntax, sHML [4, 10, 38], which is the safety logical fragment of the modal \(\mu \)-calculus [43, 44], and show how a selection of the properties in Sect. 2 can be formally specified in this logic.

The Logic. Specifications in sHML are defined over the states of transition models (such as the one of Fig. 1b), and are generated from the following grammar:

figure t

sHML expresses recursive properties as maximal fix-point formulae \(\textsf {max}x.\varphi \), that bind free occurrences of \(x\) in \(\varphi \). A central construct to sHML is the universal modal operator, \(\mathbf {[}\,p,c\,\mathbf {]}\,\varphi \). To handle reasoning over event data, sHML modalities are augmented with symbolic actions [10], consisting of event patterns \(p\in \textsc {Pat} \), and decidable constraints, \(c\in \textsc {BExp} \). This is similar to how sets of actions are expressed in tools such as CADP [40] and mCRL 2 [22]. The pattern \(p\) contains data variables, \(A, B,\ldots \in {\textsc {Var}}\), that bind free data variables in \(c\), along with any other free variables in constraints of the continuation \(\varphi \). The pair \((p,c)\) describes a concrete set of actions, \(a \in {\textsc {Act}}\) (i.e., program events). An action a is in this set when: (i) \(p\) matches the shape of a, and maps the variables in \(p\) to the payload data in a as the substitution \(\sigma \), and (ii) the instantiated constraint \(c\sigma \) of \(p\) also holds. A state Q of the SuS (model) satisfies \(\mathbf {[}\,p,c\,\mathbf {]}\,\varphi \) if the following holds: whenever Q transitions to state \(Q'\) with action a that is included in the set described by \((p,c)\) with \(\sigma \), then \(Q'\) must satisfy the instantiated continuation formula \(\varphi \sigma \).

The logical variant [4, 10] we use for detectEr combines necessities and conjunctions into one construct, \(\bigwedge _{i \in I}\mathbf {[}\,p_i,c_i\,\mathbf {]}\,\varphi _i\), to denote \(\mathbf {[}\,p_1,c_1\,\mathbf {]}\,\varphi _1 \wedge \ldots \wedge \mathbf {[}\,p_n,c_n\,\mathbf {]}\,\varphi _n\), \(I = \{1,\ldots ,n\}\) being a finite index set. Conjunctions assume that every pair \((p_i,c_i)\) describes a disjoint set of actions to facilitate the generation of deterministic monitors [35, 36]. detectEr supports the five action patterns of Table 1 that capture the lifecycle of, and interactions between the processes of the SuS. A action is exhibited by a process when it creates a child process; its dual, , is exhibited by the corresponding child upon initialisation. Process actions signal termination, while and describe interaction. The labelled state transition model of Fig. 1b uses the actions and from Table 1.

Table 1. Trace event actions capturing the behaviour exhibited by the SuS
Full size table

Example 1

Recall the SuS behaviour in Fig. 1b. Formula \(\varphi _0\) with symbolic action \((p,c)\) describes a property requiring that a state does not exhibit an output event that consists of , acknowledged with \(\textsf {bye}\) AND A NEGATIVE TOTAL, Tot.

figure bc

The universal modality states that, for any event satisfying the symbolic action \((p,c)\) from a state Q, the state \(Q'\) it transitions to must then satisfy the continuation formula. No state can satisfy the continuation \(\textsf {ff}\), and formula \(\varphi _0\) can only be satisfied when Q does not exhibit the event described by \((p,c)\). All the states in Fig. 1b trivially satisfy this property (as there are no outgoing state transitions on \((p,c)\) of formula \(\varphi _0\)) with the exception of \(Q_3\). If this state exhibits the concrete event , it matches the pattern \(p\), yielding the substitution . As \(c\sigma \) also holds, then we can conclude that \(Q_3\) violates formula \(\varphi _0\). The formula \(\varphi _1\) below extends \(\varphi _0\) to one that is invariant for any state reachable from the current state; this formalises property \(\mathrm {P}_{1}\) from Sect. 2.

figure bf

Whereas corresponds to formula \(\varphi _0\), and cover the other possible actions produced in Fig. 1b, recursing on the fix-point variable \(x\). \(\blacksquare \)

Note that the formula variables , etc. in Example 1 are different to the program variables of Fig. 1a bearing the same name. In our setting, program behaviour is observed as events, and formulae variables are used to pattern-match and reason about data in these events. We adopt the convention of naming formulae and program variables identically, merely to indicate the link between program and event data to readers.

The Tool. The syntax used by detectEr deviates minimally from sHML. Concretely, the comma symbol delimiting patterns and constraints is dropped in favour of the when keyword, whereas vacuous constraints, i.e., when \({\top }\), may be omitted. The tool also supports a shorthand notation for patterns to specify atomic values directly; these are implicitly matched against action data, e.g. sub-formula from Example 1 can be abbreviated to . Moreover, redundant data variables can be replaced by the ‘don’t care’ pattern, ( ), that matches arbitrary data values. This sugaring enables us to rewrite \(\varphi _1\) from Example 1 as:

figure bn

Example 2

Property \(\mathrm {P}_{2}\) from Sect. 2 describes a fragment of the client-server interaction, asserting that server replies are always addressed to the clients issuing them. Unlike \(\varphi _1\), this property induces data dependency across nested formulae.

figure bo

\(\mathrm {P}_{2}\) can be formalised as the formula \(\varphi _2\), where the data dependency is expressed via the binders and in , which are then used in the constraint of sub-formulae and . The constraint scopes our reasoning to a single server instance. Formula \(\varphi _2\) is violated when (since the continuation would need to satisfy \(\textsf {ff}\)), and recurs on \(x\) otherwise. Recall that the aforementioned comparisons between variable instantiations is possible since the substitution \(\sigma \) obtained from matching the symbolic action of modality extends to the context of sub-formulae and .\(\blacksquare \)

Example 3

Property \(\mathrm {P}_{3}\) specifies a control aspect of the client-server interaction, demanding that requests issued by clients are never serviced more than once.

Formula \(\varphi _3\) expresses this requirement via a guarded fix-point that recurs on \(x\) for sequences of actions; this captures normal server operation that corresponds to sub-formulae followed by , and then followed by .

figure ce

Formula \(\varphi _3\) is violated when a action matched by is followed by a second action that is matched by . The constraint in sub-formula ensures that duplicate actions concern the same recipient.\(\blacksquare \)

Our earlier formula \(\varphi _2\) of Example 2 does not account for the case where the server interacts with more than one client. It disregards the possibility of other interleaved events, that are inherent to concurrent settings where processes are unable to control when messages are received. For instance, while sub-formula matches an initial action, a second action (e.g. due to a second client that interacts with the server) matches neither nor . This does not reflect the requirement of our original property \(\mathrm {P}_{2}\). The problem can be addressed by augmenting formulae with clauses that ‘eat up’ non-relevant actions.

figure cs

As the refinement of \(\varphi _2\) above shows however, this bloats specifications, which is why we chose to scope our exposition to a single client-server set-up for the benefit of readers. Introducing the nested maximal fix-point and sub-formula filters actions by recursing on variable \(y\); the rest of \(\varphi _2\) is unaltered.

4 What Goes on

Often, post-deployment verification techniques such as RV, do not have access to the entire execution graph of a SuS, e.g. the transition model in Fig. 1b. Instead, these are limited to the trace of (program) events that is generated by the current execution of the SuS. For instance, an execution might generate the trace of events ‘ ’, that corresponds to the (finite) path traversal in the transition model of Fig. 1b. In traces, events consist of concrete values instead of variable placeholders, e.g. \(\mathtt {pid_1}\) instead of , etc. This limitation can be problematic when verifying specifications that reason about entire SuS transition models, e.g. properties expressed in the \(\mu \)-calculus [11, 43, 44], CTL [19, 41], and other branching-time logics. Recent studies show that finite traces suffice to adequately verify a practically-useful subset of these properties, as long as the verification is confined to either determining satisfaction or violation [1, 5, 7, 38, 39] (not both). This is more commonly referred to as specification monitorability [39]. sHML, used in Sect. 3 to encode properties \(\mathrm {P}_{1}\)–\(\mathrm {P}_{3}\), has been shown to be a maximally-expressive subset of the \(\mu \)-calculus for the runtime analysis of violations. This means that (i) any program that violates a property expressed as a sHML formula can be detected at runtime, (ii) any \(\mu \)-calculus property whose violations can be detected at runtime can be expressed as a sHML formula.

From Specification to Analysis. detectEr synthesises automata-like analysers in Erlang from sHML; these inspect trace events incrementally and reach irrevocable verdicts. An analyser flags a rejection verdict when it processes a trace exhibiting the program behaviour that violates a property of interest—crucially, it never flags verdicts associated with the satisfaction of the property [1, 7, 39]. Intuitively, this is because the trace observed at runtime can never provide enough information to rule out the existence of violating behaviour in other execution branches of the program. The synthesised analyser code embeds this reasoning: when a trace event is not included in the set of actions denoted by the symbolic action of a necessity modality, an inconclusive verdict is flagged.

Our synthesis translates a sHML specification to Erlang code encoded as a higher-order function, tasked with the analysis of trace events. This function accepts an event as input, and returns a new function of the same kind that performs the residual analysis following the event just processed. The synthesis, \(\llbracket -\rrbracket \), that maps sHML constructs to Erlang syntax is as follows:

figure cz

In \(\llbracket -\rrbracket \), \(\textsf {ff}\) is translated into an anonymous function that flags rejection, modelling formula violations; \(\textsf {tt}\) is not synthesised into analysis code since it can never be violated. Maximal fix-point formulae are translated to named functions that can be referenced by \(\llbracket x\rrbracket \). The conjunction of necessities, \(\bigwedge _{i \in I}\mathbf {[}\,p_i,c_i\,\mathbf {]}\,\varphi _i\), maps naturally to a sequence of function clauses, where the pattern \(p_i\) matches the shape of the trace event, and the constraint \(c_i\)—expressed as an Erlang guard [26]—operates on variables bound in \(p_i\) and those instantiated in the parent function scope. Inconclusive verdicts are modelled via the catch-all clause (_) that matches any events other than those described by the clauses, \(\texttt {fun(}p_i\texttt {)}\, \texttt {when} \, c_i\). The order of clauses in Erlang does matter, and affects our synthesis in two ways: (i) it conveniently allows us to handle the inconclusive verdict case using a catch-all clause at the end of function definitions; (ii) the mutually-exclusive symbolic actions in a necessity conjunction allows us to synthesise them in the order specified, without affecting the commutativity of conjunctions. Note that the synthesis applies the generated functions, i.e., (), to unfold them once.

Fig. 2.
figure 2

Abstract model of the analyser synthesised from formula \(\varphi _2\)

Full size image

Figure 2 depicts the behaviour of the analyser that is synthesised from formula \(\varphi _2\) of Example 2. It consists of two states, , , the rejection verdict state , and the inconclusive verdict state . The transition from to in Fig. 2 corresponds to the modality in formula \(\varphi _2\), while the transitions between and , and express sub-formulae and . The auxiliary transitions from states leading to correspond to the catch-all (_) clause inserted by the synthesis for conjuncted necessities. Figure 2 illustratively labels these transitions by the complement of the set of actions from a given state. For example, the symbolic action set from to matches anything but events; events are, in turn, matched by labelling the transition between and . Verdict irrevocability, a prevalent RV requirement [6], is modelled by the detectEr synthesis in terms of final states ( and in Fig. 2). The analysis stops when a final state is reached.

Specification, in Practice. detectEr processes sHML formulae specified in plain text files. The syntax follows the one given in Sect. 3, albeit with two adaptations: (i) the keyword and is used in lieu of \(\bigwedge \), and, (ii) we adopt the Erlang operators for writing boolean constraint expressions, e.g. =:= instead of \(=\), andalso instead of \(\wedge \), orelse instead of \(\vee \), etc. Analysers resulting from the synthesis, \(\llbracket -\rrbracket \), are compiled to binaries to be packaged with the SuS executables.

5 The Magical Mystery Tour

Instrumentation is central to RV. It refers to the extraction of the computation of interest in the form of a sequence of trace events from an executing program, and its reporting to the runtime analysis discussed in Sect. 3. Formulae can be rendered unverifiable at runtime when the program events they assume cannot be extracted and reported by the instrumentation. The instrumentation also plays a role in dropping extraneous events that can infiltrate the trace being observed and potentially, interfere with the analysis.

What to Monitor. We provide the meta keywords with and monitor to target the SuS component of interest for a particular specification. The with keyword picks out the signature of the function that is forked whereas the monitor keyword defines the property to be analysed. For example, to runtime verify the behaviour of the calculator server of Fig. 1a against formula \(\varphi _2\), we write:

figure dy

From an instrumentation standpoint, with establishes the set of trace events corresponding to the SuS component it targets, thus enabling the specification to abstract from the events generated by other components. This helps to keep the size of specifications compact whenever possible. In using with, formula \(\varphi '_2\) need not account for superfluous events (e.g. those of another server component) that tend to make the specification exercise tedious and error-prone.

Fig. 3.
figure 3

Inline, outline and offline instrumentation methods offered by detectEr

Full size image

How to Monitor. detectEr offers three instrumentation methods, inline (Sect. 6), outline (Sect. 7), and offline (Sect. 8), to cater for different situations where the RV is conducted. These methods are depicted by the three set-ups of Fig. 3 that are instantiated with our calculator server, labelled by , and its parent launcher process, labelled by . Inlining statically instruments system components with the analyser, , which then executes as part of the SuS. Outline instrumentation decouples the SuS components from the extraction and analysis of trace events by way of the tracing infrastructure provided by the EVM. The offline set-up extends the latter notion to a SuS that (possibly) executes outside the EVM, mirroring the same architecture of Fig. 3b to enjoy the same outline arrangement (elided from Fig. 3c). The with keyword directs detectEr to instrument the analyser code over the relevant SuS components regardless of the instrumentation method used, to ensure that the same set of trace events is reported to the runtime analysis. This makes the analysers generated by our synthesis of Sect. 4 agnostic of the underlying instrumentation.

6 Come Together

Inlining [34] is the most efficient instrumentation method detectEr offers. While it assumes access to the source code of the SuS, it carries advantages such as low runtime overhead [31, 32] and immediate detections [20]. detectEr instruments invocations to synthesised analysers via code injection by manipulating the program abstract syntax tree (AST). This procedure is depicted in Fig. 4. In step , the Erlang program source code is preprocessed and parsed into the corresponding AST, step . The Erlang compilation pipeline includes a parse transformation phase [26], step , that offers an optional hook to allow the AST to be processed externally, prior to code generation. Our custom-built weaver leverages this mechanism to transform the program AST in step and produce the modified AST in step ; this is subsequently compiled by the Erlang compiler into the program binary, step . The compilation phase depends on the detectEr core modules and analyser binaries, as does the SuS, once it executes.

Fig. 4.
figure 4

Instrumentation pipeline for inlined program monitoring via weaving

Full size image

Instrumentation, in One Go. Step in Fig. 4 performs two transformations on the program AST. The first transformation initialises an analyser. It weaves code instructions that store the function encoding of the synthesised analyser (refer to Sect. 4) in the process dictionary (PD) of the instrumented process (PD s are process-local, mutable key-value stores with which Erlang actors are initialised). The weaver identifies spawn() calls that carry the function signature to be executed as a process. It then replaces the spawn() call with a counterpart which accepts an anonymous wrapper function that (i) stores the analyser function in the PD, and, (ii) applies the function specified inside the original spawn() call. Figure 5a recalls the function start() that forks our calculator server loop, line 1. The corresponding weaved version of its AST—given as Erlang code for illustration in Fig. 5a—performs the initialisation of (i) and (ii). Line 3 contains (omitted) boilerplate logic that determines whether a particular spawn() call should be instrumented. The meta keyword with from Sect. 5 is used to this end: it results in the synthesis of auxiliary code that enables the weaver to effect this judgement. For example, the specification ‘with calc_server:loop(_)...’ of formula \(\varphi '_2\) informs the weaver to initialise the analyser only for the function name loop forked by the invocation of spawn() on line 1 in Fig. 5a. In line 8, the encoding of the analyser function, , is stored in the PD. The signature used in the original spawn() call on line 1 is applied on line 10, where , and are respectively instantiated to values calc_server, loop, and [0] by the boilerplate logic on line 3 (omitted).

Fig. 5.
figure 5

Transformations to the AST of the calc_server program (shown as code)

Full size image

The second transformation decorates the program AST with calls at points of interest: these correspond to the actions catalogued in Table 1. Each call constructs an intermediate trace event description that is dispatched to the analyser. Lines 9 and 12 in Fig. 5a construct events and , and dispatch them to the analyser using the function anl:dsp() exposed by the core detectEr modules. The events and are analogously handled on lines 4 and 6 in Fig. 5b.

Our weaver performs the two transformations outlined above regardless of whether monitoring is required by the SuS. This induces a modular design where the SuS is weaved once, while the analyser binaries may be independently regenerated, e.g. to refine or add sHML specifications. Updates in these binaries can afterwards be put into effect by restarting the weaved SuS. To determine whether to analyse a trace event, the dispatcher implementation anl:dsp() internally checks against the PD whether an analyser function has been initialised for the instrumented process. When the analyser function is initialised, anl:dsp() applies the function to the event, and saves the resulting unfolded analyser function back to the PD; otherwise, anl:dsp() discards the event. An irrevocable verdict is reached by the analyser function once its application to an event returns the internal value that encodes or .

Weaving makes it difficult to extract trace events, since abnormal termination due to crashes cannot be easily anticipated. This limits the ability to runtime check correctness properties concerning process termination. An instrumentation approach via external observation easily sidesteps this restriction.

7 Tell Me What You See

Outlining externalises the acquisition and analysis of SuS trace events. It relies on the tracing infrastructure provided by the EVM [26], and supports any software component that is developed for the EVM ecosystem, e.g. Erlang, Elixir [42] and Clojerl [33]. Figure 3b in Sect. 5 shows the outlined set-up for our calculator server example. Outlining uses tracers, actor processes tasked with the handling of trace events exhibited by the SuS. Tracers register with the EVM tracing infrastructure to be notified of process events in connection to the actions of Table 1. Our outlining algorithm instruments tracers on-demand, depending on what processes need to be analysed. This approach departs considerably from inline instrumentation in Sect. 6, and rather than weaving the SuS statically, outlining defers the decision of what to instrument until runtime.

While outline instrumentation tends to induce higher runtime overhead, it offers a number of benefits over inlining. It takes a non-invasive approach that leverages the EVM to trace components without modification, making it easy to enable and disable the runtime analysis without the need of restarts or redeployments. By decoupling the SuS and tracer components, outlining induces a degree of partial failure—a faulty analyser does not compromise the running system, nor does a crashed system component affect the external tracer. As a result of this arrangement, trace events can be detected, giving us the full expressiveness with respect to the system actions of Table 1. The implementation of an adequate outline monitoring set-up comes with its own set of challenges. For example, the instrumentation should be engineered to scale in line with the SuS, while the runtime analysis of trace events is underway. It has to contend with the race conditions (e.g. trace event reordering) that arise from the asynchronous execution of the SuS and tracer components. Scalability requires the instrumentation to explicitly manage garbage collection, where redundant tracer processes are discarded to minimise resource consumption. Inline instrumentation is spared these complications since the analysis logic is weaved directly in SuS processes. Although our outline instrumentation algorithm handles these aspects, we refrain from providing further detail in this presentation. Interested readers are encouraged to consult [8] for more details.

Instrumentation, as We Go. The EVM tracing infrastructure enables processes to register their interest in receiving trace event messages from other processes. Erlang provides the built-in function trace(), that processes may invoke to enable and disable process tracing dynamically at runtime. Our tracers from Fig. 3b leverage this functionality to fork other tracers, and scale the RV set-up as the SuS executes. We configure the EVM tracing to automatically assign the tracer of an already-traced SuS process to the children it forks [26]. Using this as a default setting allows us to analyse groups of processes as one component. The with keyword guides the targeting of which processes tracers need to track and analyse. By contrast to inlining—where the set of trace events of a component is implicitly determined as a byproduct of weaving—outlining must actively isolate processes from a group to assign dedicated tracers. Recall the specification ‘with calc_server:loop(_)...’ of formula \(\varphi '_2\). This instructs our outline instrumentation to set up an independent tracer process for the calculator server loop forked by spawn() on line 1 in Fig. 5a.

Fig. 6.
figure 6

Outline instrumentation for the calculator server (analysers omitted)

Full size image

Tracers are programmed to react to and events in the trace. Figure 6 illustrates how the process creation sequence of the SuS is exploited to instrument a dedicated tracer for our calculator server. A tracer instruments other tracers whenever it encounters events. The initial RV configuration is shown in Fig. 6a, where the root tracer, , is assigned to the launcher process, , in step . forks the server function loop() to execute as the process which is automatically assigned the same tracer , as steps both indicate. Subsequently, instruments a new tracer, , when it processes the trace event due to in step . The data carried by contains the PID of the forked process (see Table 1) that designates the SuS process to be instrumented, , in this case. At this point, takes over the tracing of from the root tracer by invoking trace() to handle independently of , steps and . resumes its analysis of , receiving the event in step  ; this is followed by in step as a result of the service request issued by the client, , in step . In a similar way, the service reply sent by the server to in step results in being exhibited by and received by in step . Process eventually exits after the fork completes, step . The ensuing event in step is interpreted by the root tracer as the cue to self-terminate in step . This garbage collection measure maintains the lowest possible runtime overhead.

8 I’m Only Sleeping

We extend the notion of outline instrumentation to the offline case where the SuS may potentially run outside the EVM. To support offline instrumentation, detectEr implements a middleware that emulates the EVM tracing infrastructure, while preserving the configuration mentioned in Sect. 7, i.e., where forked system processes automatically inherit the tracer assigned to their parent. This enables detectEr to employ the same outline instrumentation algorithm for offline monitoring. Offline set-ups are generally the slowest in terms of verdict detection, by comparison to the inline and outline forms of instrumentation. This stems from the dependence outline instrumentation has on the timely availability of pre-recorded runtime traces that are subject to external software entities such as files, databases, and the SuS itself. However, the outline set-up and SuS can reside on different hardware since they are mutually detached. Such an arrangement makes overhead issues secondary.

Figure 3c from Sect. 5 overviews our offline arrangement. It mirrors the set-up in Fig. 3b: the only difference lies in how the offline tracing infrastructure obtains events. Our Log Tracer component in Fig. 3c exposes a trace() function, providing the same EVM feature subset relevant to outlining. The implementation relies on log files as the medium through which the SuS can communicate trace events to the offline set-up. It can process log files with complete system executions, or actively monitor files for changes to dynamically dispatch events to tracers while the SuS executes and writes events to file. Offline tracing supports the event actions in Table 1; these carry the event data and are assumed to follow a pre-defined format. For instance, the offline event description is mapped to the action \(\mathtt {pid_1}\,\mathsf {\rightarrow }\,\mathtt {pid_2},\,\texttt {calc\_server}\!\textsf {:}\!\texttt {loop}(\texttt {[0]})\) by the Log Tracer of Fig. 3c. Our file-based approach to collecting SuS events is motivated by the fact that file logging is widely-adopted in practice, and is offered by popular frameworks such as Lager [21] for Erlang, Log4J 2 [16] for Java [46], and the Python [49] logging facility. Besides logging, events may also be extracted from the SuS via other tracing frameworks, e.g. DTrace [23], LTTng [28], and OpenJ9 Trace [30].

9 Here, There and Everywhere

This paper presents detectEr, a RV tool that analyses program correctness post-deployment against properties expressed in a logic that has been traditionally used for static verification [14, 22, 40]. Sects. 5–8 describe how detectEr can flexibly runtime check the same specifications via three instrumentation methods. The tool can be found at https://duncanatt.github.io/detecter.

Future Work. We intend to asses the merits of our three instrumentation methods in terms of the multi-faceted overhead metrics proposed by [9]. We also plan to extend detectEr to handle sHML specifications where conjunctions and universal modalities can be treated as separate logical constructs [3, 4, 17, 18, 24, 25, 39]. This facilitates the composition of properties via conjunctions, e.g. formulae \(\varphi _1\)–\(\varphi _3\) from Sect. 3 can be combined as \(\varphi _1\wedge \varphi _2\wedge \varphi _3\) to synthesise one global monitor. Although detectEr focusses on properties that are known to be runtime monitorable, new results argue that monitoring can be systematically extended to the entire class of regular properties, albeit, with possibly weakened detection guarantees [2, 7]. We aim to incorporate these results within this tool.