bluuebunny/crossref_metadata_2025 huggingface dataset:
Static analysis of upper and lower bounds on dependences and parallelism
Authors: Pugh William , Wonnacott David
Published: October 2002

Existing compilers often fail to parallelize sequential code, even when a program can be manually transformed into parallel form by a sequence of well-understood transformations (as in the case for many of the Perfect Club Benchmark programs). These failures can occur for several reasons: the code transformations implemented in the compiler may not be sufficient to produce parallel code, the compiler may not find the proper sequence of transformations, or the compiler may not be able to prove that one of the necessary transformations is legal.

When a compiler fails to extract sufficient parallelism from a program, the programmer may try to extract additional parallelism. Unfortunately, the programmer is typically left to search for parallelism without significant assistance. The compiler generally does not give feedback about which parts of the program might contain additional parallelism, or about the types of transformations that might be needed to realize this parallelism. Standard program transformations and dependence abstractions cannot be used to provide this feedback.

In this paper, we propose a two-step approach to the search for parallelism in sequential programs. In the first step, we construct several sets of constraints that describe, for each statement, which iterations of that statement can be executed concurrently. By constructing constraints that correspond to different assumptions about which dependences might be eliminated through additional analysis, transformations, and user assertions, we can determine whether we can expose parallelism by eliminating dependences. In the second step of our search for parallelism, we examine these constraint sets to identify the kinds of transformations needed to exploit scalable parallelism. Our tests will identify conditional parallelism and parallelism that can be exposed by combinations of transformations that reorder the iteration space (such as loop interchange and loop peeling).

This approach lets us distinguish inherently sequential code from code that contains unexploited parallelism. It also produces information about the kinds of transformations needed to parallelize the code, without worrying about the order of application of the transformations. Furthermore, when our dependence test is inexact we can identify which unresolved dependences inhibit parallelism by comparing the effects of assuming dependence or independence. We are currently exploring the use of this information in programmer-assisted parallelization.
Fixpoint computation for polyvariant static analyses of higher-order applicative programs
Authors: Ashley J. Michael , Consel Charles
Published: October 2002

This paper presents an optimized general-purpose algorithm for polyvariant, static analyses of higher-order applicative programs. A polyvariant analysis is a very accurate form of analysis that produces many more abstract descriptions for a program than does a conventional analysis. It may also compute intermediate abstract descriptions that are irrelevant to the final result of the analysis. The optimized algorithm addresses this overhead while preserving the accuracy of the analysis. The algorithm is also parameterized over both the abstract domain and degree of polyvariance. We have implemented an instance of our algorithm and evaluated its performance compared to the unoptimized algorithm. Our implementation runs significantly faster on average than the other algorithm for benchmarks reported here.
Axiomatic bootstrapping
Authors: Appel Andrew W.
Published: October 2002

If a compiler for language
L
is implemented in
L
, then it should be able to compile itself. But for systems used interactively commands are compiled and immediately executed, and these commands may invoke the compiler; so there is the question of how ever to cross-compile for another architecture. Also, where the compiler writes binary files of static type information that must then be read in by the bootstrapped interactive compiler, how can one ever change the format of digested type information in binary files?

Here I attempt an axiomatic clarification of the bootstrapping technique, using
Standard ML of New Jersey
as a case study. This should be useful to implementors of any self-applicable interactive compiler with nontrivial object-file and runtime-system compatibility problems.
Closure analysis in constraint form
Authors: Palsberg Jens
Published: October 2002

Flow analyses of untyped higher-order functional programs have in the past decade been presented by Ayers, Bondorf, Consel, Jones, Heintze, Sestoft, Shivers, Steckler, Wand, and others. The analyses are usually defined as abstract interpretations and are used for rather different tasks such as type recovery, globalization, and binding-time analysis. The analyses all contain a global
closure analysis
that computes information about higher-order control-flow. Sestoft proved in 1989 and 1991 that closure analysis is correct with respect to call-by-name and call-by-value semantics, but it remained open if correctness holds for arbitrary beta-reduction.

This article answers the question; both closure analysis and others are correct with respect to arbitrary beta-reduction. We also prove a subject-reduction result: closure information is still valid after beta-reduction. The core of our proof technique is to define closure analysis using a constraint system. The constraint system is equivalent to the closure analysis of Bondorf, which in turn is based on Sestoft's.
Beyond induction variables
Authors: Gerlek Michael P. , Stoltz Eric , Wolfe Michael
Published: October 2002

Linear induction variable detection is usually associated with the strength reduction optimization. For restructuring compilers, effective data dependence analysis requires that the compiler detect and accurately describe linear and nonlinear induction variables as well as more general sequences. In this article we present a practical technique for detecting a broader class of linear induction variables than is usually recognized, as well as several other sequence forms, including periodic, polynomial, geometric, monotonic, and wrap-around variables. Our method is based on Factored Use-Def (FUD) chains, a demand-driven representation of the popular Static Single Assignment (SSA) form. In this form, strongly connected components of the associated SSA graph correspond to sequences in the source program: we describe a simple yet efficient algorithm for detecting and classifying these sequences. We have implemented this algorithm in Nascent, our restructuring Fortran 90+ compiler, and we present some results showing the effectiveness of our approach.
Optimal evaluation of array expressions on massively parallel machines
Authors: Chatterjee Siddhartha , Gilbert John R. , Schreiber Robert , Teng Shang-Hua
Published: October 2002

We investigate the problem of evaluating Fortran 90-style array expressions on massively parallel distributed-memory machines. On such a machine, an elementwise operation can be performed in constant time for arrays whose corresponding elements are in the same processor. If the arrays are not aligned in this manner, the cost of aligning them is part of the cost of evaluating the expression tree. The choice of where to perform the operation then affects this cost.

We describe the communication cost of the parallel machine theoretically as a metric space; we model the alignment problem as that of finding a minimum-cost embedding of the expression tree into this space. We present algorithms based on dynamic programming that solve the embedding problem optimally for several communication cost metrics: multidimensional grids and rings, hypercubes, fat-trees, and the discrete metric. We also extend our approach to handle operations that change the shape of the arrays.
Matching-based incremental evaluators for hierarchical attribute grammar dialects
Authors: Carle Alan , Pollock Lori
Published: October 2002

Although attribute grammars have been very effective for defining individual modules of language translators, they have been rather ineffective for specifying large program-transformational systems. Recently, several new attribute grammar “dialects” have been developed that support the modular specification of these systems by allowing modules, each described by an attribute grammar, to be composed to form a complete system. Acceptance of these new
hierarchical
attribute grammar dialects requires the availability of efficient batch and incremental evaluators for hierarchical specifications. This paper addresses the problem of developing efficient incremental evaluators for hierarchical specifications. A matching-based approach is taken in order to exploit existing optimal change propagation algorithms for nonhierarchical attribute grammars. A sequence of four new matching algorithms is presented, each increasing the number of previously computed attribute values that are made available for reuse during the incremental update.
Type checking concurrent I/O
Authors: Carlisle W. H.
Published: October 2002

In parallel programming languages multityped data structures may be shared by two or more processes. Process I/O to these structures is assumed to be physically interleaved but logically parallel. This article addresses a syntactic mechanism to specify a type for such structures and extends an example language and its type-checking algorithm to these structures.
BURS automata generation
Authors: Proebsting Todd A.
Published: October 2002

A simple and efficient algorithm for generating bottom-up rewrite system (BURS) tables is described. A small code-generator generator implementation produces BURS tables efficiently, even for complex instruction set descriptions. The algorithm does not require novel data structures or complicated algorithmic techniques. Previously published methods for on-the-fly elimination of states are generalized and simplified to create a new method, triangle trimming, that is employed in the algorithm. A prototype implementation, burg, generates BURS tables very efficiently.
Efficiently computing Φ-nodes on-the-fly
Authors: Cytron Ron K. , Ferrante Jeanne
Published: October 2002

Recently, Static Single-Assignment Form and Sparse Evaluation Graphs have been advanced for the efficient solution of program optimization problems. Each method is provided with an initial set of flow graph nodes that inherently affect a problem's solution. Other relevant nodes are those where potentially disparate solutions must combine. Previously, these so-called φ-nodes were found by computing the iterated dominance frontiers of the initial set of nodes, a process that could take worst-case quadratic time with respect to the input flow graph. In this article we present an almost-linear algorithm for determining exactly the same set of φ-nodes.
Efficient instruction scheduling for delayed-load architectures
Authors: Kurlander Steven M. , Proebsting Todd A. , Fischer Charles N.
Published: October 2002

A fast, optimal code-scheduling algorithm for processors with a delayed load of one instruction cycle is described. The algorithm minimizes both execution time and register use and runs in time proportional to the size of the expression-tree. An extension that spills registers when too few registers are available is also presented. The algorithm also performs very well for delayed loads of greater than one instruction cycle. A heuristic that schedules DAGs and is based on our optimal expression-tree-scheduling algorithm is presented and compared with Goodman and Hsu's algorithm Integrated Prepass Scheduling (IPS). Both schedulers perform well on benchmarks with small basic blocks, but on large basic blocks our scheduler outperforms IPS and is significantly faster.
An incremental algorithm for satisfying hierarchies of multiway dataflow constraints
Authors: Vander Zanden Brad
Published: October 2002

One-way dataflow constraints have gained popularity in many types of interactive systems because of their simplicity, efficiency, and manageability. Although it is widely acknowledged that multiway dataflow constraint could make it easier to specify certain relationships in these applications, concerns about their predictability and efficiency have impeded their acceptance. Constraint hierarchies have been developed to address the predictability problem, and incremental algorithms have been developed to address the efficiency problem. However, existing incremental alogrithms for satisfying constraint hierarchies encounter two difficulties : (1) they are incapable of guaranteeing an acylic solution if a constraint hierarchy has one or more cyclic solutions and (2) they require worst-case exponential time to satisfy systems of multioutput constriants. This article surmounts these difficulties by presenting an incremental algorithm called QuickPlan that satisfies in worst-case

O(N
2
)

time any hierarchy of multiway, multiout-put dataflow constraint that has at least one acyclic solution, where
N
is the number of constraints. With benchmarks and real problems that can be solved efficiently using exisitng algorithms, its performance is competitive or superior. With benchmarks and real problems that cannot be solved using exisitng algorithms or that cannot be solved efficiently, QuickPlan finds solutions and does so efficiently, typically in
O(N)
time or less. QuickPlan is based on the strategy of propagation of degrees of freedom. The only restriction it imposes is that every constraint method must use all of the variables in the constraint as either an input or an output variable. This requirement is met in every constraint-based, interactive application that we have developed or seen.
Language support for the specification and development of composite systems
Authors: Feather Martin S.
Published: October 2002

When a complex system is to be realized as a combination of interacting components, development of those components should commence from a specification of the behavior required of the composite system. A separate specification should be used to describe the decomposition of that system into components. The first phase of implementation from a specification in this style is the derivation of the individual component behaviors implied by these specifications.

The virtues of this approach to specification are expounded, and specification language features that are supportive of it are presented. It is shown how these are incorporated in the specification language Gist, which our group has developed. These issues are illustrated in a development of a controller for elevators serving passengers in a multistory building.
Indirect distributed garbage collection
Authors: Piquer José M.
Published: October 2002

In new distributed systems, object mobility is usually allowed and is sometimes used by the underlying object manager system to benefit from object access locality. On the other hand, in-transit references to objects can exist at any moment in asynchronous distributed systems. In the presence of object mobility and in-transit references, many garbage collector (GC) algorithms fail to operate correctly. Others need to use the system's object finder to find the objects while performing their work. As a general principle, a GC should never interfere with object manager polices (such as forcing migration or fixing an object to a given processor). However, if the GC uses the object finder, it will change the access pattern of the system, and eventually it could foul the global allocation policy. In this article we propose a new GC family, Indirect Garbage Collectors, allowing to separate the problems of object management (placement, replication, and retrieval) from garbage collection. This property allows our algorithms to be implemented on top of almost any existent distributed object system, without having to use the object finder.
Proofs as programs
Authors: Bates Joseph L. , Constable Robert L.
Published: October 2002

The significant intellectual cost of programming is for problem solving and explaining, not for coding. Yet programming systems offer mechanical assistance for the coding process exclusively. We illustrate the use of an implemented program development system, called PRL ("pearl"), that provides automated assistance with the difficult part. The problem and its explained solution are seen as formal objects in a constructive logic of the data domains. These formal explanations can be executed at various stages of completion. The most incomplete explanations resemble applicative programs, the most complete are formal proofs.
Lightweight closure conversion
Authors: Steckler Paul A. , Wand Mitchell
Published: October 2002

We consider the problem of lightweight closure conversion, in which multiple procedure call protocols may coexist in the same code. A lightweight closure omits bindings for some of the free variables of the procedure that is represents. Flow analysis is used to match the protocol expected by each procedure and the protocol used at its possible call sites. We formulate the flow analysis as a deductive system that generates a labeled transition system and a set of constraints. We show that any solution to the constraints justifies the resulting transformation. Some of the techniques used are similar to those of abstract interpretation, but others appear to be novel.
A methodology for synthesis of recursive functional programs
Authors: Banerjee Debasish
Published: October 2002

John Backus introduced the Functional Programming (FP) system, the variable-free applicative system having reduction semantics. Backus has also introduced a unique expansion technique for reasoning about a class of recursive FP programs. As a natural outgrowth of this expansion technique, an FP program synthesis methodology is described in this paper.

The methodology synthesizes recursive FP programs of the form
f
=
p
→,
q
;
E
(
f
.
h
) from their preformulated case-by-case descriptions, which in turn come from given input-output example specifications. After explaining the methodology informally, formalization in the form of a definition and a synthesis theorem is introduced. A sufficient condition for the functional form
E
, for successful synthesis under the present methodology, is obtained structurally. Several illustrative examples of synthesis are also included.
On the use of regular expressions for searching text
Authors: Clarke Charles L. A. , Cormack Gordon V.
Published: October 2002

The use of regular expressions for text search is widely known and well understood. It is then surprising that the standard techniques and tools prove to be of limited use for searching structured text formatted with SGML or similar markup languages. Our experience with structured text search has caused us to reexamine the current practice. The generally accepted rule of “leftmost longest match” is an unfortunate choice and is at the root of the difficulties. We instead propose a rule which is semantically cleaner. This rule is generally applicable to a variety of text search applications, including source code analysis, and has interesting properties in its own right. We have written a publicly available search tool implementing the theory in the article, which has proved valuable in a variety of circumstances.
Toward a complete transformational toolkit for compilers
Authors: Bergstra J. A. , Dinesh T. B. , Field J. , Heering J.
Published: October 2002

PIM is an equational logic designed to function as a “transformational toolkit” for compilers and other programming tools that analyze and manipulate imperative languages. It has been applied to such problems as program slicing, symbolic evaluation, conditional constant propagation, and dependence analysis. PIM consists of the untyped lambda calculus extended with an algebraic data type that characterizes the behavior of lazy stores and generalized conditionals. A graph form of PIM terms is by design closely related to several intermediate representations commonly used in optimizing compilers. In this article, we show that PIM's core algebraic component, PIM

t

, possesses a
complete
equational axiomatization (under the assumption of certain reasonable restrictions on term formation). This has the practical consequence of guaranteeing that every semantics-preserving transformation on a program representable in PIM

t

can be derived by application of PIM

t

rules. We systematically derive the complete PIM

t

logic as the culmination of a sequence of increasingly powerful equational systems starting from a straightforward “interpreter” for closed PIM

t

terms. This work is an intermediate step in a larger program to develop a set of well-founded tools for manipulation of imperative programs by compilers and other systems that perform program analysis.
A study of the applicability of existing exception-handling techniques to component-based real-time software technology
Authors: Lang Jun , Stewart David B.
Published: October 2002

This study focuses on the current state of error-handling technology and concludes with recommendations for further research in error handling for component-based real-time software. With real-time programs growing in size and complexity, the quality and cost of developing and maintaining them are still deep concerns to embedded software industries. Component-based software is a promising approach in reducing development cost while increasing quality and reliability. As with any other real-time software, component-based software needs exception detection and handling mechanisms to satisfy reliability requirements. The current lack of suitable error-handling techniques can make an application composed of reusable software nondeterministic and difficult to understand in the presence of errors.
Dynamic currency determination in optimized programs
Authors: Dhamdhere D. M. , Sankaranarayanan K. V.
Published: October 2002

Compiler optimizations pose many problems to source-level debugging of an optimized program due to reordering, insertion, and deletion of code. On such problem is to determine whether the value of a varible is
current
at a breakpoint—that is, whether its actual value is the same as its expected value. We use the notion of
dynamic currency
of a variable in source-level debugging and propose the use of a
minimal unrolled graph
to reduce the run-time overhead of dynamic currency determination. We prove that the minimal unrolled graph is an adequate basis for performing bit-vector data flow analyses at a breakpoint. This property is used to perform dynamic currency determination. It is also shown to help in recovery of a dynamically noncurrent variable.
A new, simpler linear-time dominators algorithm
Authors: Buchsbaum Adam L. , Kaplan Haim , Rogers Anne , Westbrook Jeffery R.
Published: October 2002

We present a new linear-time algorithm to find the immediate dominators of all vertices in a flowgraph. Our algorithm is simpler than previous linear-time algorithms: rather than employ complicated data structures, we combine the use of microtrees and memoization with new observations on a restricted class of path compressions. We have implemented our algorithm, and we report experimental results that show that the constant factors are low. Compared to the standard, slightly superlinear algorithm of Lengauer and Tarjan, which has much less overhead, our algorithm runs 10-20% slower on real flowgraphs of reasonable size and only a few percent slower on very large flowgraphs.
Componential set-based analysis
Authors: Flanagan Cormac , Felleisen Matthias
Published: October 2002

Set-based analysis (SBA) produces good predictions about the behavior of functional and object-oriented programs. The analysis proceeds by inferring
constraints
that characterize the data flow relationships of the analyzed program. Experiences with MrSpidey, a static debugger based on SBA, indicate that SBA can adequately deal with programs of up to a couple of thousand lines of code. SBA fails, however, to cope with larger programs because it generates systems of constraints that are at least linear, and possibility quadratic, in the size of the analyzed program. This article presents theoretical and practical results concerning methods for reducing the size of constraint systems. The theoretical results include of proof-theoretic characterization of the
observable behavior
of constraint systems for program components, and a complete algorithm for deciding the observable equivalence of constraint systems. In the course of this development we establish a close connection between the observable equivalence of constraint systems and the equivalence of regular-tree grammars. We then exploit this connection to adapt a variety of algoirthms for simplifying grammars to the problem of simplifying constraint systems. Based on the resulting algorithms, we have developed
componential set-based analysis
, a modular and polymorphic variant of SBA. Experimental results verify the effectiveness of the simplification algorithms and the componential analysis. The simplified constraint systems are typically an order of magnitude smaller than the original systems. These reductions in size produce significant gains in the speed of the analysis.
Dependency analysis for Standard ML
Authors: Blume Matthias
Published: October 2002

Automatic dependency analysis is a useful addition to a system like CM, our compilation manager for Standard ML of New Jersey. It relieves the programmer from the tedious and error-prone task of having to specify compilation dependencies by hand and thereby makes its usage more user friendly. But dependency analysis is not easy, as the general problem for Standard ML is NP-complete. Therefore, CM has to impose certain restrictions on the programming language to recover tractability. We prove the NP-completeness result, discuss the restrictions on ML that are used by CM, and provide the resulting analysis algorithms.
Static correlated branch prediction
Authors: Young Cliff , Smith Michael D.
Published: October 2002

Recent work in history-based branch prediction uses novel hardware structures to capture branch correlation and increase branch prediction accuracy.
Branch correlation
occurs when the outcome of a conditional branch can be accurately predicted by observing the outcomes of previously executed branches in the dynamic instruction stream. In this article, we show how to instrument a program so that it is practical to collect run-time statistics that indicate where branch correlation occurs, and we then show how to use these statistics to transform the program so that its static branch prediction accuracy is improved. The run-time information that we gather is called a
path profile
, and it summarizes how often each executed sequence of program points occurs in the program trace. Our path proles are more general than those previously proposed. The code transformation that we present is called
static correlated branch prediction
(SCBP). It exhibits better branch prediction accuracy than previously thought possible for static prediction techniques. Furthermore, through the use of an overpruning heuristic, we show that it is possible to determine automatically an appropriate trade-off between code expansion and branch predictability so that our transformation improves the performance of multiple-issue, deeply pipelined microprocessors like those being built today.
Efficient demand-driven evaluation. Part 1
Authors: Pingali Keshav , Arvind
Published: October 2002

We describe a program transformation technique for programs in a general stream language L whereby a data-driven evaluation of the transformed program performs exactly the same computation as a demand-driven evaluation of the original program. The transformational technique suggests a simple denotational characterization of demand-driven evaluation.
Undecidability of context-sensitive data-dependence analysis
Authors: Reps Thomas
Published: October 2002

A number of program-analysis problems can be tackled by transforming them into certain kinds of graph-reachability problems in labeled directed graphs. The edge labels can be used to filter out paths that are not interest: a path
P
from vertex
s
to vertex
t
only counts as a“valid connection” between
s
and
t
if the word spelled out by
P
is in a certain language. Often the languages used for such filtering purposes are languages of matching parantheses. In some cases, the matched-parenthesis condition is used to filter out paths with mismatched calls and returns. This leads to so-called “context-
sensitive
” program analyses, such as context-
sensitive
interprocedural slicing and context-
sensitive
interprocedural dataflow analysis. In other cases, the matched-parenthesis condition is used to capture a graph-theoretic analog of McCarthy's rules: “car (cons(x,y)) = x” and “cdr(cons(x,y)) =y”. That is, in the code fragment

c = cons(a,b); d = car(c);

the fact that there is a “structure-transmitted data-dependence” from a to d, but not from b to d, is captured in a graph by (1) using a vertex for each variable, (2)an edge from vertex
i
to vertex
j
when
i
is used on the right-hand side of an assignment to
j
, (3) parentheses that match as the labels on the edges that run from a to c and c to d, and (4) parentheses that do not match as the labels on the edges that run from a to c and c to d. However, structure-transmitted data-dependence analysis is context-
insensitive
, because there are no constraints that filter out paths with mismatched calls and returns. Thus, a natural question is whether these two kinds of uses of parentheses can be combined to create a context-
sensitive
analysis for structure-transmitted data-dependences. This article answers the question in the negative: in general, the problem of context
sensitive
, structure-transmitted data-dependence analysis is undecidable. The results imply that in general, both context-
sensitive
set-based analysis and ∞-CFA (when data constructors and selectors and selectors are taken into account) are also undecidable.
The Compilation of Loop Induction Expressions
Authors: Sites Richard L.
Published: October 2002

In an optimizing compiler, it is often desirable to compile subscript expressions such as Abase-2 + I*2 so that the value of the expression is available in a register and is simply incremented whenever I is incremented, thus avoiding the multiplication inside the loop. This change is effected by a standard optimization called strength reduction. Program loops often contain several such expressions stemming perhaps from references to operands A(I), A(I+1), B(I), and C(K,J,I,L). Under what circumstances can we do better than keeping four addresses in four separate registers or temporaries? A general technique is presented which minimizes the number of registers needed to hold such values, while simultaneously minimizing the amount of computation inside the loop. In the above collection, it is possible to use as few as two registers for the four I-dependent values.
Operators
Authors: Iverson Kenneth E.
Published: October 2002

Although operators, which apply to functions to produce functions, prove very useful in mathematics, they are absent from most programming languages. This paper illustrates their simplicity and power in terms of the operators of APL, and examines related constructs in other programming languages.
A Language for Array and Vector Processors
Authors: Perrott R. H.
Published: October 2002

The scientific community has consistently demanded from computing machines an increase in the number of instructions executed per second. The latest increase has been achieved by duplication of arithmetic units for an array processor and the pipelining of functional units for vector processors. The high level programming languages for such machines have not benefited from the advances which have been made in programming language design and implementation techniques.

A high level language is described in this paper which is appropriate for both array and vector processors and is defined without reference to the hardware of either type of machine. The syntax enables the parallel nature of a problem to be expressed in a form which can be readily exploited by these machines. This is achieved by using the data declarations to indicate the maximum extent of parallel processing and then to manipulate this, or a lesser extent, in the course of program execution. It was found to be possible to modify many of the structured programming and data structuring concepts for this type of parallel environment and to maintain the benefits of compile time and run time checking. Several special constructs and operators are also defined.

The language offers to the large scale scientific computing community many of the advances which have been made in software engineering techniques while it exploits the architectural advances which have been made.
Verification of Array, Record, and Pointer Operations in Pascal
Authors: Luckham David C. , Suzuki Norihisa
Published: October 2002

A practical method is presented for automating in a uniform way the verification of Pascal programs that operate on the standard Pascal data structures Array, Record, and Pointer. New assertion language primitives are introduced for describing computational effects of operations on these data structures. Axioms defining the semantics of the new primitives are given. Proof rules for standard Pascal operations on data structures are then defined using the extended assertion language. An axiomatic rule for the Pascal storage allocation operation, NEW, is also given. These rulers have been implemented in the Stanford Pascal program verifier. Examples illustrating the verification of programs which operate on list structures implemented with pointers and records are discussed. These include programs with side effects.
Global Context Recovery: A New Strategy for Syntactic Error Recovery by Table-Drive Parsers
Authors: Pai Ajit B. , Kieburtz Richard B.
Published: October 2002

Described is a method for syntactic error recovery that is compatible with deterministic parsing methods and that is able to recover from many errors more quickly than do other schemes because it performs global context recovery. The method relies on fiducial symbols, which are typically reserved key words of a language, to provide mileposts for error recovery. The method has been applied to LL(1) parsers, for which a detailed algorithm is given, and informally proved correct. The algorithm will always recover and return control to the parser if the text being analyzed satisfies only minimal requirements: that it contains one or more occurrences of fiducial symbols following the point at which an error is detected. Tables needed for error recovery have been automatically generated, along with parsing tables, by a parser constructor for the LL(1) grammars.

A theoretical characterization of fiducial symbols is given, and the utility of this characterization in practice is discussed. It has been applied to a grammar for the programming language Pascal to aid in selection of a set of fiducial symbols. The error recovery scheme has been tested on a set of student-written Pascal program texts and is compared with other error recovery strategies.
A Note on Median Split Trees
Authors: Comer Douglas
Published: October 2002

The median split tree is an elegant technique for searching static sets of keys when the frequency of access is highly skewed. This paper generalizes the median split search technique, relates it to sequential search and binary search, discusses the choice of an optimum search strategy for a given set of keys, and poses several related optimization problems.
On Parsing and Compiling Arithmetic Expressions on Vector Computers
Authors: Fischer Charles N.
Published: October 2002

The problem of parsing and compiling arithmetic expressions on vector computers is considered. Methods are developed which allow encodings of one or more arithmetic expressions to be transformed directly into encodings of their corresponding derivation trees. The algorithm which performs this transformation is compact, efficient, and able to make extensive use of concurrent vector operations. Routines which concurrently transverse encoded derivation trees in a top-down or bottom-up manner are presented. These routines can be used to structure efficient, compact, and highly concurrent algorithms which complete the process of compiling arithmetic expressions.
Design of a Machine-Independent Optimizing System for Emulator Development
Authors: Ma Perng-Ti , Lewis T. G.
Published: October 2002

Methods are described to translate a certain machine-independent intermediate language (IML) to efficient microprograms for a class of horizontal microprogrammable machines. The IML is compiled directly from a high-level microprogramming language used to implement a virtual instruction set processor as a microprogram.

The primary objective of the IML-to-host machine interface design is to facilitate language portability. Transportability is accomplished by use of a field description model and a macro expansion table which describe the host machine to the translator system.

Register allocation scheme and control flow analysis are employed to allocate the symbolic variables of the IML to the general-purpose registers of the host machine. A set of 5-tuple microoperations (function, input, output, field, phase) is obtained with the aid of the field description model. Then a compaction algorithm is used to detect the parallelism of microoperations and to generate suboptimal code for a horizontal microprogrammable machine. The study concludes with a description of the effects of the above methods upon the quality of microcode produced for a specific commercial computer.
Derivation of Invariant Assertions During Program Development by Transformation
Authors: Broy Manfred , Krieg-Bruckner Bernd
Published: October 2002

Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a recursive program with a subsequent transformation into an iterative version by schematically applying suitable recursion removal rules. The connection between the approaches is demonstrated by augmenting such transformation rules by inductive assertions. It is argued that the latter approach to program development is superior since the correctness proof of a recursive program is easier in most cases. Considerable verification overhead can be avoided this way, in particular, some difficulties with the interaction of successive loops and their associated invariants.
Synthesis of Resource Invariants for Concurrent Programs
Authors: Clarke Edmund
Published: October 2002

Owicki and Gries have developed a proof system for
conditional critical regions
. In their system, logically related variables accessed by more than one process are grouped together as
resources
, and processes are allowed access to a resource only in a critical region for that resource. Proofs of synchronization properties are constructed by devising predicates called
resource invariants
which describe relationships among the variables of a resource when no process is in a critical region for the resource. In constructing proofs using the system of Owicki and Gries, the programmer is required to supply the resource invariants.

Methods are developed in this paper for automatically synthesizing resource invariants. Specifically, the resource invariants of a concurrent program are characterized as
least fixpoints
of a functional which can be obtained from the text of the program. By the use of this fixpoint characterization and a
widening operator
based on convex closure, good approximations may be obtained for the resource invariants of many concurrent programs.
A Formal System for Reasoning about Programs Accessing a Relational Database
Authors: Casanova Marco R. , Bernstein Phillip A.
Published: October 2002

A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic logic and incorporates a data definition language (DDL) for describing relational databases and a data manipulation language (DML) whose programs access data in a database. The DDL is a many-sorted first-order language that accounts for data aggregations. The DML features a many-sorted assignment in place of the usual data manipulation statements, in addition to the normal programming language constructs.
Describing and analyzing distributed software system designs
Authors: Avrunin George S. , Wileden Jack C.
Published: October 2002

In this paper we outline an approach to describing and analyzing designs for distributed software systems. A descriptive notation is introduced, and analysis techniques applicable to designs expressed in that notation are presented. The usefulness of the approach is illustrated by applying it to a realistic distributed software-system design problem involving mutual exclusion in a computer network.
Simple, efficient, asynchronous parallel algorithms for maximization
Authors: Greenberg Albert G. , Lubachevsky Boris D. , Odlyzko Andrew M.
Published: October 2002

The problem of computing the maximum of
n
inputs on an asynchronous parallel computer is considered. In general, the inputs may arrive staggered in time, the number of processors available to the maximization algorithm may vary during its execution, and the number of inputs,
n
, may be initially unknown. Two simple, efficient algorithms to compute the maximum are presented. Each algorithm may be invoked asynchronously, as new inputs and processors arrive. Performance measures that account for the response times of the invocations are introduced, and the algorithms are analyzed under these measures.
ACE: an automatic complexity evaluator
Authors: Le Métayer Daniel
Published: October 2002

There has been a great deal of research done on the evaluation of the complexity of particular algorithms; little effort, however, has been devoted to the mechanization of this evaluation. The ACE (Automatic Complexity Evaluator) system is able to analyze reasonably large programs, like sorting programs, in a fully mechanical way. A time-complexity function is derived from the initial functional program. This function is transformed into its nonrecursive equivalent according to MacCarthy's recursion induction principle, using a predefined library of recursive definitions. As the complexity is not a decidable property, this transformation will not be possible in all cases. The richer the predefined library is, the more likely the system is to succeed. The operations performed by ACE are described and the use of the system is illustrated with the analysis of a sorting algorithm. Related works and further improvements are discussed in the conclusion.
Efficient incremental LR parsing for syntax-directed editors
Authors: Degano Pierpaolo , Mannucci Stefano , Mojana Bruno
Published: October 2002

A technique for generating parsers which is an extension to LR techniques and is based on parsing table splitting, is presented. Then this technique is slightly extended to support incremental syntax analysis. Given a context-free grammar and a set “
IC
” of nonterminals devised to be incremental, a set of subtables is generated to drive the analysis of program fragments derivable from nonterminals in
IC
.

The proposed technique generates parsing tables which are considerably smaller than the standard ones, even when incrementality is not exploited. Thus, these tables may be stored as arrays permitting faster access and accurate error handling. Furthermore, our tables are suitable for generating syntax-directed editors which provide a full analytic mode. The efficiency of the analytic component of a syntax-directed editor obtained in this way and its easy integration with the generative component stress the advantages of incremental program writing.
Editing by example
Authors: Nix Robert P.
Published: October 2002

An editing by example system is an automatic program synthesis facility embedded in a text editor that can be used to solve repetitive text editing problems. The user provides the editor with a few examples of a text transformation. The system analyzes the examples and generalizes them into a program that can perform the transformation to the rest of the user's text. This paper presents an overview of the design, analysis, and implementation of a practical editing by example system. It studies the problem of synthesizing a text processing program that generalizes the transformation implicitly described by a small number of input/output examples. A class of text processing programs called
gap programs
is defined and the problems associated with synthesizing them from examples are examined, leading to an efficient heuristic that provably synthesizes a gap program from examples of its input/output behavior. The editing by example system derived from this analysis has been embedded in a production text editor. By developing an editing by example system that solves a useful class of text processing problems, this work demonstrates that program synthesis is feasible in the domain of text editing.
Mechanizing a theory of program composition for UNITY
Authors: Paulson Lawrence C.
Published: October 2002

Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which Charpentier and Chandy [1999] have illustrated by developing a large example in the UNITY formalism. The present paper describes extensive experiments on mechanizing the compositionality theory and the example, using the proof tool Isabelle. Broader issues are discussed, in particular, the formalization of program states. The usual representation based upon maps from variables to values is contrasted with the alternatives, such as a signature of typed variables. Properties need to be transferred from one program component's signature to the common signature of the system. Safety properties can be so transferred, but progress properties cannot be. Using polymorphism, this problem can be circumvented by making signatures sufficiently flexible. Finally the proof of the example itself is outlined.
The apprentice challenge
Authors: Moore J. Strother , Porter George
Published: October 2002

We describe a mechanically checked proof of a property of a small system of Java programs involving an unbounded number of threads and synchronization, via monitors. We adopt the output of the javac compiler as the semantics and verify the system at the bytecode level under an operational semantics for the JVM. We assume a sequentially consistent memory model and atomicity at the bytecode level. Our operational semantics is expressed in ACL2, a Lisp-based logic of recursive functions. Our proofs are checked with the ACL2 theorem prover. The proof involves reasoning about arithmetic; infinite loops; the creation and modification of instance objects in the heap, including threads; the inheritance of fields from superclasses; pointer chasing and smashing; the invocation of instance methods (and the concomitant dynamic method resolution); use of the start method on thread objects; the use of monitors to attain synchronization between threads; and consideration of all possible interleavings (at the bytecode level) over an unbounded number of threads. Readers familiar with monitor-based proofs of mutual exclusion will recognize our proof as fairly classical. The novelty here comes from (i) the complexity of the individual operations on the abstract machine; (ii) the dependencies between Java threads, heap objects, and synchronization; (iii) the bytecode-level interleaving; (iv) the unbounded number of threads; (v) the presence in the heap of incompletely initialized threads and other objects; and (vi) the proof engineering permitting automatic mechanical verification of code-level theorems. We discuss these issues. The problem posed here is also put forth as a benchmark against which to measure other approaches to formally proving properties of multithreaded Java programs.