This paper describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly.

When transforming programs for complex instrumentation and optimization, it is essential to understand the effect of the transformations, to best optimize the transformed programs, and to speedup the transformation process. This paper describes a powerful method for composing transformation rules to achieve these goals.

Dynamic languages such as Python allow programs to be written more easily using high-level constructs such as comprehensions for queries and using generic code. Efficient execution of programs then requires powerful optimizations - incrementalization of expensive queries and specialization of generic code. Effective incrementalization and specialization of dynamic languages require precise and scalable alias analysis.

This paper describes the use of a powerful graph query language for querying programs, and a novel combination of transformations for generating efficient implementations of the queries. The language supports graph path expressions that allow convenient use of both vertices and edges of arbitrary kinds as well as additional global and local parameters in graph paths. Our implementation method combines transformation to Datalog, recursion conversion, demand transformation, and specialization, and finally generates efficient analysis programs with precise complexity guarantees. This combination improves an O(VE) time complexity factor using previous methods to O(E), where V and E are the numbers of graph vertices and edges, respectively. We also describe implementations and experiments that confirm the analyzed complexities.

This paper describes a language and framework that allow coordinated transformations driven by invariants to be specified declaratively, as invariant rules, and applied automatically. The framework supports incremental maintenance of invariants for program design and optimization, as well as general transformations for instrumentation, refactoring, and other purposes. This paper also describes our implementations for transforming Python and C programs and experiments with successful applications of the systems in generating efficient implementations from clear and modular specifications, in instrumenting programs for runtime verification, profiling, and debugging, and in code refactoring.

In this paper, we introduce the new technique of high-confidence software monitoring (HCSM), which allows one to perform software monitoring with bounded overhead and concomitantly achieve high confidence in the observed error rates. HCSM is formally grounded in the theory of supervisory control of finite-state automata: overhead is controlled, while maximizing confidence, by disabling interrupts generated by the events being monitored - and hence avoiding the overhead associated with processing these interrupts - for as short a time as possible under the constraint of a user-supplied target overhead Otarget. HCSM is a general technique for software monitoring in that HCSM-based instrumentation can be attached at any system interface or API. A generic controller implements the optimal control strategy described above. As a proof of concept, and as a practical framework for software monitoring, we have implemented HCSM-based monitoring for both bounds checking and memory leak detection. We have further conducted an extensive evaluation of HCSM's performance on several real-world applications, including the Lighttpd Web server, and a number of special-purpose micro-benchmarks. Our results demonstrate how confidence grows in a monotonically increasing fashion with the target overhead, and that tight confidence intervals can be obtained for each target-overhead level.

This paper describes a framework that supports powerful queries in debugging tools, and describes in particular the transformations, alias analysis, and type analysis used to make the queries efficient. The framework allows queries over the states of all objects at any point in the execution as well as over the history of states. The transformations are based on incrementally maintaining the results of expensive queries studied in previous work. The alias analysis extends the flow-sensitive intraprocedural analysis to an efficient flow-sensitive interprocedural analysis for an object-oriented language with also a form of context sensitivity. We also show the power of the framework and the effectiveness of the analyses through case studies and experiments with XML DOM tree transformations, an FTP client, and others. We were able to easily determine the sources of all injected bugs, and we also found an actual bug in the case study on the FTP client.

This paper describes a transformational method applied to the core component of role-based access control (RBAC), to derive efficient implementations from a specification based on the ANSI standard for RBAC. The method is based on the idea of incrementally maintaining the result of expensive set operations, where a new method is described and used for systematically deriving incrementalization rules. We calculate precise complexities for three variants of efficient implementations as well as for a straightforward implementation based on the specification. We describe successful prototypes and experiments for the efficient implementations and for automatically generating efficient implementations from straightforward implementations.

Object abstraction supports the separation of what operations are provided by systems and components from how the operations are implemented, and is essential in enabling the construction of complex systems from components. Unfortunately, clear and modular implementations have poor performance when expensive query operations are repeated, while efficient implementations that incrementally maintain these query results are much more difficult to develop and to understand, because the code blows up significantly, and is no longer clear or modular.This paper describes a powerful and systematic method that first allows the "what" of each component to be specified in a clear and modular fashion and implemented straightforwardly in an object-oriented language; then analyzes the queries and updates, across object abstraction, in the straightforward implementation; and finally derives the sophisticated and efficient "how" of each component by incrementally maintaining the results of repeated expensive queries with respect to updates to their parameters. Our implementation and experimental results for example applications in query optimization, role-based access control, etc. demonstrate the effectiveness and benefit of the method.