On the sequential nature of interprocedural program-analysis problems

In this paper, we study two interprocedural program-analysis problems—interprocedural slicing and interprocedural dataflow analysis— and present the following results:

? Interprocedural slicing is log-space complete forP.

? The problem of obtaining “meet-over-all-valid-paths” solutions to interprocedural versions of distributive dataflow-analysis problems isP-hard.

? Obtaining “meet-over-all-valid-paths” solutions to interprocedural versions of distributive dataflow-analysis problems that involve finite sets of dataflow facts (such as the classical “gen/kill” problems) is log-space complete forP.

These results provide evidence that there do not exist fast (N?-class) parallel algorithms for interprocedural slicing and precise interprocedural dataflow analysis (unlessP =N?). That is, it is unlikely that there are algorithms for interprocedural slicing and precise interprocedural dataflow analysis for which the number of processors is bounded by a polynomial in the size of the input, and whose running time is bounded by a polynomial in the logarithm of the size of the input. This suggests that there are limitations on the ability to use parallelism to overcome compiler bottlenecks due to expensive interprocedural-analysis computations.     

Identifying modules via concept analysis

Describes a general technique for identifying modules in legacy code. The method is based on concept analysis - a branch of lattice theory that can be used to identify similarities among a set of objects based on their attributes. We discuss how concept analysis can identify potential modules using both “positive” and “negative” information. We present an algorithmic framework to construct a lattice of concepts from a program, where each concept represents a potential module. We define the notion of a concept partition, present an algorithm for discovering all concept partitions of a given concept lattice, and prove the algorithm to be correct     

Symbolic analysis via semantic reinterpretation

The paper presents a novel technique to create implementations of the basic primitives used in symbolic program analysis: forward symbolic evaluation, weakest liberal precondition, and symbolic composition. We used the technique to create a system in which, for the cost of writing just one specification—an interpreter for the programming language of interest—one obtains automatically generated, mutually-consistent implementations of all three symbolic-analysis primitives. This can be carried out even for languages with pointers and address arithmetic. Our implementation has been used to generate symbolic-analysis primitives for the x86 and PowerPC instruction sets.     

Reducing concurrent analysis under a context bound to sequential analysis

This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only a partial guarantee of correctness: the approach bounds the number of context switches allowed in the concurrent program, and aims to prove safety, or find bugs, under the given bound. In this paper, we show how to obtain simple and efficient algorithms for the analysis of concurrent programs with a context bound. We give a general reduction from a concurrent program P, and a given context bound K, to a sequential program P _s ^K such that the analysis of P _s ^K can be used to prove properties about P. The reduction introduces symbolic constants and assume statements in P _s ^K . Thus, any sequential analysis that can deal with these two additions can be extended to handle concurrent programs as well, under a context bound. We give instances of the reduction for common program models used in model checking, such as Boolean programs, pushdown systems (PDSs), and symbolic PDSs. Supported by NSF under grants CCF-0540955, CCF-0524051, and CCF-0810053, and by IARPA under AFRL contract FA8750-06-C-0249. Any opinions, findings, and conclusions or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of either NSF or IARPA. Supported by a Microsoft Research Fellowship.     

Design and implementation of a fine-grained software inspection tool

Although software inspection has led to improvements in software quality, many software systems continue to be deployed with unacceptable numbers of errors, even when software inspection is part of the development process. The difficulty of manually verifying that the software under inspection conforms to the rules is partly to blame. We describe the design and implementation of a tool designed to help alleviate this problem. The tool provides mechanisms for fine-grained inspection of software by exposing the results of sophisticated whole-program static analysis to the inspector. The tool computes many static-semantic representations of the program, including an accurate call graph and dependence graph. A whole-program pointer analysis is used to make sure that the representation is precise with respect to aliases induced by pointer usage. Views on the dependence graph and related representations are supported. Queries on the dependence graph allow an inspector to answer detailed questions about the semantics of the program. Facilities for openness and extensibility permit the tool to be integrated with many software development processes. The main challenge of the approach is to provide facilities to navigate and manage the enormous complexity of the dependence graph.     

Computational Divided Differencing and Divided-Difference Arithmetics

Tools for computational differentiation transform a program that computes a numerical function F(x) into a related program that computes F(x) (the derivative of F). This paper describes how techniques similar to those used in computational-differentiation tools can be used to implement other program transformations—in particular, a variety of transformations for computational divided differencing. The specific technical contributions of the paper are as follows:– It presents a program transformation that, given a numerical function F(x) defined by a program, creates a program that computes F[x ₀, x ₁], the first divided difference of F(x), where – It shows how computational first divided differencing generalizes computational differentiation.– It presents a second program transformation that permits the creation of higher-order divided differences of a numerical function defined by a program.– It shows how to extend these techniques to handle functions of several variables.The paper also discusses how computational divided-differencing techniques could lead to faster and/or more robust programs in scientific and graphics applications.Finally, the paper describes how computational divided differencing relates to the numerical-finite-differencing techniques that motivated Robert Paige's work on finite differencing of set-valued expressions in SETL programs.     

Efficient comparison of program slices

Theslice of a program with respect to a componentc is a projection of the program that includes all components that might affect (either directly or transitively) the values of the variables used atc. Slices can be extracted particularly easily from a program representation called a program dependence graph, originally introduced as an intermediate program representation for performing optimizing, vectorizing, and parallelizing transformations. This paper presents a linear-time algorithm for determining whether two slices of a program dependence graph are isomorphic.This work was supported in part by a David and Lucile Packard Fellowship for Science and Engineering, by the National Science Foundation under grants DCR-8552602 and CCR-8958530, by the Defense Advanced Research Projects Agency, monitored by the Office of Naval Research under contract N00014-88-K-0590, and by grants from IBM, DEC, Xerox, 3M, Eastman Kodak, and the Cray Research Foundation.