Synthesising Correct Concurrent Runtime Monitors - Runtime Verification - page 113

( ii ) the system and the monitor themselves consist of concurrent sub-systems and sub-
monitors. Previous work on correct monitor synthesis[17,27,4] abstracts away from
the internal working of a system, representing it as a string of events

/

states (execu-
tion trace). It also focusses on a logic that is readily amenable to runtime analysis,
namely Linear Temporal Logic (LTL)[8]. Moreover, it expresses synthesis in terms of
abstract or single-threaded monitors—using pseudocode or automata—executing wrt.
such trace. By contrast, we strive towards a more intensional formal definition of online
correctness for synthesised concurrent monitors whereby, for arbitrary property ϕ ,the

synthesised monitor M ϕ running concurrently wrt. some system S (denoted as S M ϕ )

observes the following condition:

S violates ϕ in the current execution i ff S M ϕ detects the violation (1)

The setting described in (1) brings to the fore a number of additional issues:

(i) Apart from the formal semantics of the source logic (used to specify the property

ϕ ), we also require a formal semantics for the target languages of both the system

and the monitor executing in parallel, i.e., S

M ϕ . In most cases, the latter may

not always be available.

(ii) A property logic semantics is often defined over systems rather than traces ,which

may not lend itself well to the formulation of correctness runtime analysis outlined
in condition (1) above. In the case of concurrent systems, this aspect is accentu-
ated by the fact that systems may behave non-deterministically and typically have
multiple execution paths as a result of di

ff erent thread interleavings scheduled at

runtime.

(iii) Concurrent monitors may also have multiple execution paths. Condition (1) thus

requires stronger guarantees than those for single-threaded monitors so as to en-
sure that all these paths correspond to an appropriate runtime check of system
property being monitored. Stated otherwise, correct concurrent monitors must al-
ways detect violations, irrespective of their runtime interleaving.

(iv) Online monitor correctness needs to ensure that monitor execution cannot be in-

terfered by the system, and viceversa. Whereas adequate monitor instrumentation
typically prevents direct interferences, condition (1) must consider indirect inter-
ferences such as system divergences [25,18], i.e.,infinite internal looping making
the system unresponsive, which may prevent the monitors from progressing.

(v) Ensuring correctness along the lines of condition (1) can be quite onerous because

every execution path of the monitor running concurrently with the monitored sys-
tem, S M ϕ , needs to be analysed so as to ensure consistent detections along

every thread interleaving. Consequently, one needs to devise scalable techniques
facilitating monitor correctness analysis.

We conduct our study in terms of actor-based [19] concurrent monitors written in Er-
lang [7,2], an industry strength language for constructing fault-tolerant systems; we also
restrict ourselves to the monitoring of systems written in the same language. We limit
ourselves to reactive properties describing system interactions with the environment and
focus on the synthesis of asynchronous monitors, performing runtime analysis through
the Erlang Virtual Machine (EVM)'s tracing mechanism. Despite the typical drawbacks