Monitoring Semantics: a Formal Framework for Specifying, Implementing and Reasoning about Execution Monitors

Authors:

Amir Kishon, Charles Consel, and Paul Hudak

Abstract:

We introduce monitoring semantics, a non-standard model of program execution that captures “monitoring activity” as found in debuggers, profilers, tracers, etc.  A monitoring semantics is a conservative extension of a language’s standard denotational semantics, and is parameterized with respect to specifications of monitoring activity.

Beyond its theoretical interest, monitoring semantics forms a practical baais for building effective monitors, with standard partial evaluation techniques being used as a key optimization strategy.  In particular, specializing a monitoring semantics with respect to a source program amounts to removing the interpretive overhead associated with the static aspects of monitoring, yielding an instrumented program in which the extra code to perform monitoring actions has been automatically "embedded" into the program.

A monitoring semantics can be automatically derived for any language for which a continuation semantics specification has been provided.  This is achieved by using functionals to embed non-standard behavior at all levels of recursion.  We illustrate the approach for a higher-order functional language, showing examples of several different monitor specifications, including benchmarks of their implementations.

Bibtex:

 @InProceedings{kishonhudakconsel91,
  author =      "A. Kishon and C. Consel and P. Hudak",
  title =       "Monitoring Semantics: a Formal Framework for Specifying,
                 Implementing and Reasoning about Execution Monitors",
  booktitle =   "ACM SIGPLAN Conference on Programming Language Design 
                 and Implementation",
  month =	Jun,
  year =        "1991",
  pages = "338-352"
} 

Links:

MonSem-PLDI91.pdf