Browse Theses

A program execution monitor is a system that monitors the run-time behavior of a program. Examples include profilers, tracers, and debuggers. Monitors are an important element in any software development environment. However, despite their ubiquity, formal and general treatments of program execution monitoring are rare.

This thesis introduces monitoring semantics--a formal model of program execution monitors. Using the framework of continuation semantics, one can specify the behavior of a large family of program execution monitors. The resulting specification can then be automatically combined with the standard semantics to yield a composite semantics that is formally consistent with respect to the standard semantics.

Beyond its theoretical interest, monitoring semantics provides a basis for implementing a large family of source-level monitoring activities for any language for which a continuation semantics is available. To demonstrate the generality and effectiveness of this approach, we use our methodology to automatically synthesize debugging behaviors with standard interpreters. The enhanced interpreters are guaranteed to be consistent with the standard interpretation. This solves the consistency problem that still persists in many debugging methodologies for strict and especially non-strict programming languages. We present the synthesis of correct profilers, tracers and, most importantly, interactive source-level debuggers for strict and non-strict functional programming languages and compare their specifications.

Finally, using standard partial evaluation techniques as an optimization strategy, monitoring semantics forms a practical basis for building actual monitors. Our system can be optimized in two levels of specialization: specializing the interpreter with respect to a monitor specification automatically yields an instrumented interpreter; further specializing this instrumented interpreter with respect to a source program yields an instrumented program, i.e., one in which the extra code to perform monitoring has been automatically embedded into the program.

All these ideas add up to a complete methodology for specifying, implementing and reasoning about a large family of program execution monitors for sequential deterministic programming languages.