PRL Seminars 1998-99

Abstract

Modern programming languages provide tools for enhancing productivity. For example, module systems and objects encourage re-use and partitioning of functionality. But a new class of performance issues arises when applying these tools.

We propose a means to control performance and improve reliability based on the notion of a logical programming environment (LPE). We demonstrate the effectiveness of the methods by carrying out significant systems implementation in a specific LPE called MetaPRL.

The talk will present MetaPRL, a system I developed as part of my thesis research. To the user, MetaPRL behaves as an enhanced modular compiler, where the compilation path is augmented by a rich logical superstructure that can be called upon, when desired, to perform program transformation and verification.

I'll discuss two applications of this approach to the Ensemble group communication system. One is automatic and verified code optimization, and the other is modular interactive verification of safety properties of protocol stacks.