bluuebunny/crossref_metadata_2025 huggingface dataset:
Contract Soundness for object-oriented languages
Authors: Findler Robert Bruce , Felleisen Matthias
Published: November 2005

Checking pre- and post-conditions of procedures and methods at runtime helps improve software reliability. In the procedural world, pre- and post-conditions have a straightforward interpretation. If a procedure's pre-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the procedure failed to compute the expected result.

In the object-oriented world, checking pre- and post-conditions for methods, often called contracts in this context, poses complex problems. Because methods may be overridden, it is not sufficient to check only pre- and post-conditions. In addition, the contract hierarchy must be checked to ensure that the contracts on overridden methods are properly related to the contracts on overriding methods. Otherwise, a class hierarchy may violate the substitution principle, that is, it may no longer be true that an instance of a class is substitutable for objects of the super-class.

In this paper, we study the problem of contract enforcement in an object-oriented world from a foundational perspective. More specifically, we study contracts as refinements of types. Pushing the analogy further, we state and prove a contract soundness theorem that captures the essential properties of contract enforcement. We use the theorem to illustrate how most existing tools suffer from a fundamental flaw and how they can be improved.
On objects and events
Authors: Eugster Patrick Th. , Guerraoui Rachid , Damm Christian Heide
Published: November 2005

This paper presents linguistic primitives for publish/subscribe programming using events and objects. We integrate our primitives into a strongly typed object-oriented language through four mechnisms: (1) serialization, (2) multiple subtyping, (3)closures, and (4) deferred code evaluation. We illustrate our primitives through Java, showing how we have overcome its respective lacks. A precompiler transforms statements based on our publish/subscribe primitives into calls to specifically generated typed adapters, which resemble the typed stubs and skeletons by the rmic precompiler for remote method invocations in Java
Object-oriented composition untangled
Authors: Ostermann Klaus , Mezini Mira
Published: November 2005

Object-oriented languages come with pre-defined composition mechansims, such as inheritance, object composition, or delegation, each characterized by a certain set of composition properties, which do not themselves individually exist as abstractions at the language level. However, often non-standard composition semantics is needed, with a mixture of composition mechanisms. Such non-standard semantics are simulated by complicated architectures that are sensitive to requirement changes and cannot easily be adapted without invalidating existing clients. In this paper, we propose
compound references
, a new abstraction for object references, that allows us to provide explicit linguistic means for expressing and combining individual composition properties on-demand. The model is statically typed and allows the programmer to express a seamless spectrum of composition semantics in the interval between object composition and inheritance. The resulting programs are better understandable, due to explicity expressed design decisions, and less sensitive to requirement changes.
The architecture of a UML virtual machine
Authors: Riehle Dirk , Fraleigh Steven , Bucka-Lassen Dirk , Omorogbe Nosa
Published: November 2005

Current software development tools let developers model a software system and generate program code from the models to run the system. However, generating code and installing a non-trivial system induces a time delay between changing the model and executing it that makes rapid model prototyping awkard if not impossible. This paper presents the architecture of a virtual machine for UML that interprets UML models without any intermediate code-generation step. The paper shows how to embed UML in a metalevel architecture so that a key property of model-based systems, the casual connection between models and model instances, is guaranteed. With this architecture, changes to a model have immediate effects on its execution, providing users with rapid feedback about the model's structure and behavior. This approach supports model innovation better than today's code-generation approaches.
The denotation semantics of NIPL
Authors: Li Tao , Liu XiaoJie
Published: November 2005

With the neurons, neural networks and rules in NIPL encapsulated as a special object, the concepts of object-oriented programming, neural network computing and logic inference have been unified, therefore, the denotation semantics of NIPL based on the theory of object-oriented is given.
A fresh approach to representing syntax with static binders in functional programming
Authors: Pitts Andrew M.
Published: November 2005

Tell category theorists about the concept of abstract syntax for a language and they may say "that's just the initial algebra for a sum-of-products functor on the category of sets". Despite what you might think, they are trying to be helpful since the initiality property is the common denominator of both definitions by structural recursion and proofs by structural induction [5, Sect. 4.4]. In recent years we have learned how to extend this initial algebra view of abstract syntax to encompass languages with statically scoped binders. In the presence of such binders one wants to abstract away from the specific names of bound variables, either by quotienting parse trees by a suitable notion of alpha-equivalence, or by replacing conventional trees with ones containing de Bruijn indices [1]. By changing from the category of sets to other well-known, but still 'set-like' categories of sheaves or presheaves, one can regain an initial algebra view of this even more than normally abstract syntax---the pay-off being new and automatically generated forms of structural recursion and induction that respect alpha-equivalence [2, 3]. One good test of these new ideas is to see if they give rise to new forms of functional programming. In fact they do. The paper [6] sketches a functional programming language for representing and manipulating syntactical structure involving binders, based on the mathematical model of variable-binding in [3, 4]. In this ML-like language there are new forms of type for names and name-binding that come along with facilities for declaring fresh names, for binding names in abstractions and for pulling apart such name-abstractions via pattern-matching. The key idea is that properly abstract uses of names, i.e. ones that do not descend below the level of alpha-conversion, can be imposed on the user by a static type system that deduces information about the freshness of names. Even though we appear to be giving users a 'gensym' facility, the type system restricts the way it can be used to the extent that we keep within effect-free functional programming, in the sense that the usual laws of pure functional programming remain valid (augmented with new laws for names and name-abstractions). In this talk I will introduce this new approach to representing languages static binders in functional programming and discuss some of the difficulties we have had verifying its semantic properties.
Contification using dominators
Authors: Fluet Matthew , Weeks Stephen
Published: November 2005

Contification is a compiler optimization that turns a function that always returns to the same place into a continuation. Compilers for functional languages use contification to expose the control-flow information that is required by many optimizations, including traditional loop optimizations. This paper gives a formal presentation of contification in MLton, a whole-program optimizing Standard ML compiler. We present two existing algorithms for contification in our framework, as well as a new algorithm based on the dominator tree of a program's call graph. We prove that the dominator algorithm is optimal. We present benchmark results on realistic SML programs demonstrating that contification has minimal overhead on compile time and significantly improves run time.
Functioning without closure
Authors: Dimock Allyn , Westmacott Ian , Muller Robert , Turbak Franklyn , Wells J. B.
Published: November 2005

The CIL compiler for core Standard ML compiles whole ML programs using a novel typed intermediate language that supports the generation of type-safe customized data representations. In this paper, we present empirical data comparing the relative efficacy of several different flow-based customization strategies for function representations. We develop a cost model to interpret dynamic counts of operations required for each strategy. In this cost model, customizing the representation of closed functions gives a 12-17% improvement on average over uniform closure representations, depending on the layout of the closure. We also present data on the relative effectiveness of various strategies for reducing representation pollution, i.e., situations where flow constraints require the representation of a value to be less efficient than it would be in ideal circumstances. For the benchmarks tested and the types of representation pollution detected by our compiler, the pollution removal strategies we consider often cost more in overhead than they gain via enabled customizations. Notable exceptions are selective defunctionalization, a function representation strategy that often achieves significant customization benefits via aggressive pollution removal, and a simple form of flow-directed inlining, in which pollution removal allows multiple functions to be inlined at the same call site.
Optimizing pattern matching
Authors: Le Fessant Fabrice , Maranget Luc
Published: November 2005

We present improvements to the backtracking technique of pattern-matching compilation. Several optimizations are introduced, such as commutation of patterns, use of exhaustiveness information, and control flow optimization through the use of labeled static exceptions and context information. These optimizations have been integrated in the Objective-Caml compiler. They have shown good results in increasing the speed of pattern-matching intensive programs, without increasing final code size.
Down with Emacs Lisp
Authors: Neubauer Matthias , Sperber Michael
Published: November 2005

It is possible to translate code written in Emacs Lisp or another Lisp dialect which uses dynamic scoping to a more modern programming language with lexical scoping while largely preserving structure and readability of the code. The biggest obstacle to such an idiomatic translation from Emacs Lisp is the translation of dynamic binding into suitable instances of lexical binding: Many binding constructs in real programs in fact exhibit identical behavior under both dynamic and lexical binding. An idiomatic translation needs to detect as many of these binding constructs as possible and convert them into lexical binding constructs in the target language to achieve readability and efficiency of the target code. The basic prerequisite for such an idiomatic translation is thus a dynamic scope analysis which associates variable occurrences with binding constructs. We present such an analysis. It is an application of the Nielson/Nielson framework for flow analysis to a semantics for dynamic binding akin to Moreau's. Its implementation handles a substantial portion of Emacs Lisp, has been applied to realistic Emacs Lisp code, and is highly accurate and reasonably efficient in practice.
Recursive structures for standard ML
Authors: Russo Claudio V.
Published: November 2005

Standard ML is a statically typed programming language that is suited for the construction of both small and large programs. "Programming in the small" is captured by Standard ML's Core language. "Programming in the large" is captured by Standard ML's Modules language that provides constructs for organizing related Core language definitions into self-contained modules with descriptive interfaces. While the Core is used to express details of algorithms and data structures, Modules is used to express the overall architecture of a software system. In Standard ML, modular programs must have a strictly hierarchical structure: the dependency between modules can never be cyclic. In particular, definitions of mutually recursive Core types and values, that arise frequently in practice, can never span module boundaries. This limitation compromises modular programming, forcing the programmer to merge conceptually (i.e. architecturally) distinct modules. We propose a practical and simple extension of the Modules language that caters for cyclic dependencies between both types and terms defined in separate modules. Our design leverages existing features of the language, supports separate compilation of mutually recursive modules and is easy to implement.
Macros as multi-stage computations
Authors: Ganz Steven E. , Sabry Amr , Taha Walid
Published: November 2005

With few exceptions, macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed functional languages: static typing and static scoping. At a deeper level, there is a need for a simple, usable semantics for macros. This paper argues that these problems can be addressed by formally viewing macros as multi-stage computations. This view eliminates the need for freshness conditions and tests on variable names, and provides a compositional interpretation that can serve as a basis for designing a sound type system for languages supporting macros, or even for compilation. To illustrate our approach, we develop and present MacroML, an extension of ML that supports inlining, recursive macros, and the definition of new binding constructs. The latter is subtle, and is the most novel addition in a statically typed setting. The semantics of a core subset of MacroML is given by an interpretation into MetaML, a statically-typed multi-stage programming language. It is then easy to show that MacroML is stage- and type-safe: macro expansion does not depend on runtime evaluation, and both stages do not "go wrong.
A simple implementation technique for priority search queues
Authors: Hinze Ralf
Published: November 2005

This paper presents a new implementation technique for priority search queues. This abstract data type is an amazing blend of finite maps and priority queues. Our implementation supports logarithmic access to a binding with a given key and constant access to a binding with the minimum value. Priority search queues can be used, for instance, to give a simple, purely functional implementation of Dijkstra's single-source shortest-paths algorithm. A non-technical concern of the paper is to foster abstract data types and views. Priority search queues have been largely ignored by the functional programming community and we believe that they deserve to be known better. Views prove their worth both in defining a convenient interface to the abstract data type and in providing a readable implementation.
Real-time FRP
Authors: Wan Zhanyong , Taha Walid , Hudak Paul
Published: November 2005

Functional reactive programming (FRP) is a declarative programming paradigm where the basic notions are continuous, time-varying behaviors and discrete, event-based reactivity. FRP has been used successfully in many reactive programming domains such as animation, robotics, and graphical user interfaces. The success of FRP in these domains encourages us to consider its use in real-time applications, where it is crucial that the cost of running a program be bounded and known before run-time. But previous work on the semantics and implementation of FRP was not explicitly concerned about the issues of cost. In fact, the resource consumption of FRP programs in the current implementation is often hard to predict. As a first step towards addressing these concerns, this paper presents real-time FRP (RT-FRP), a statically-typed language where the time and space cost of each execution step for a given program is statically bounded. To take advantage of existing work on languages with bounded resources, we split RT-FRP into two parts: a reactive part that captures the essential ingredients of FRP programs, and a base language part that can be instantiated to any generic programming language that has been shown to be terminating and resource-bounded. This allows us to focus on the issues specific to RT-FRP, namely, two forms of recursion. After presenting the operational explanation of what can go wrong due to the presence of recursion, we show how the typed version of the language is terminating and resource-bounded. Most of our FRP programs are expressible directly in RT. The rest are expressible via a simple mechanism that integrates RT-FRP with the base language.
On regions and linear types (extended abstract)
Authors: Walker David , Watkins Kevin
Published: November 2005

We explore how two different mechanisms for reasoning about state,
linear typing and the type, region and effect discipline,
complement one another in the design of a strongly typed functional
programming language. The basis for our language is a simple lambda
calculus containing first-class memory regions, which are
explicitly passed as arguments to functions, returned as results
and stored in user-defined data structures. In order to ensure
appropriate memory safety properties, we draw upon the literature
on linear type systems to help control access to and deallocation
of regions. In fact, we use two different interpretations of linear
types, one in which multiple-use values are freely copied and
discarded and one in which multiple-use values are explicitly
reference-counted, and show that both interpretations give rise to
interesting invariants for manipulating regions. We also explore
new programming paradigms that arise by mixing first-class regions
and conventional linear data structures.
Extensible algebraic datatypes with defaults
Authors: Zenger Matthias , Odersky Martin
Published: November 2005

A major problem for writing extensible software arises when recursively defined datatypes and operations on these types have to be extended simultaneously without modifying existing code. This paper introduces Extensible Algebraic Datatypes with defaults, which promote a simple programming pattern to solve this well-known problem. We show that it is possible to encode extensible algebraic datatypes in an object-oriented language, using a new design pattern for extensible visitors. Extensible algebraic datatypes have been successfully applied in the implementation of an extensible Java compiler. Our technique allows for the reuse of existing components in compiler extensions without the need for any adaptations.
Cost-augmented narrowing-driven specialization
Authors: Vidal Germán
Published: November 2005

The aim of many program transformers is to improve efficiency while preserving program meaning. Correctness issues have been dealt with extensively. However, very little attention has been paid to formally establish the improvements achieved by these transformers. In this work, we introduce the scheme of a narrowing-driven partial evaluator enhanced with abstract costs. They are "abstract" in the sense that they measure the number of
basic
operations performed during a computation rather than actual execution times. Thus, we have available a setting in which one can discuss the effects of the program transformer in a precise framework and, moreover, to quantify these effects. Our scheme may serve as a basis to develop speedup analyses and cost-guided transformers. An implementation of the cost-augmented specializer has been undertaken, which demonstrates the practicality of our approach.
Staged compilation
Authors: Chambers Craig
Published: November 2005

Traditional compilers compile and optimize files separately, making worst-case assumptions about the program context in which a file is to be linked. More aggressive compilation architectures perform cross-file interprocedural or whole-program analyses, potentially producing much faster programs but substantially increasing the cost of compilation. Even more radical are systems that perform all compilation and optimization at run-time: such systems can optimize programs based on run-time program and system properties as well as static whole-program properties. However, run-time compilers (also called dynamic compilers or just-in-time compilers) suffer under severe constraints on allowable compilation time, since any time spent compiling steals from time spent running the program. None of these compilation models dominates the others: each has unique strengths and weaknesses not present in the other models.We are developing a new, staged compilation model which strives to combine high run-time code quality with low compilation overhead. Compilation is organized as a series of stages, with stages corresponding to, for example, separate compilation, library linking, program linking, and run-time execution. Any given optimization can be performed at any of these stages; to reduce compilation time while maintaining high effectiveness, an optimization should be performed at the earliest stage that provides the necessary program context information to carry out the optimization effectively. Moreover, a single optimization can itself be spread across multiple stages, with earlier stages performing preplanning work that enables the final stage to complete the optimization quickly. In this way, we hope to produce highly optimized programs, nearly as good as what could be done with a purely run-time compiler that had an unconstrained compilation time budget, but at a much more practical compile time cost.We are building the Whirlwind optimizing compiler as the concrete embodiment of this staged compilation model, initially targeting object-oriented languages. A key component of Whirlwind is a set of techniques for automatically constructing staged compilers from traditional unstaged compilers, including aggressive applications of specialization and other partial evaluation technology.
Implementation of automatic differentiation tools
Authors: Bischof Christian H. , Hovland Paul D. , Norris Boyana
Published: November 2005

Automatic differentiation is a semantic transformation that applies the rules of differential calculus to source code. It thus transforms a computer program that computes a mathematical function into a program that computes the function and its derivatives. Derivatives play an important role in a wide variety of scientific computing applications, including optimization, solution of nonlinear equations, sensitivity analysis, and nonlinear inverse problems. We describe a simple component architecture for developing tools for automatic differentiation and other mathematically oriented semantic transformations of scientific software. This architecture consists of a compiler-based, language-specific front-end for source transformation, loosely coupled with one or more language-independent "plug-in" transformation modules. The coupling mechanism between the front-end and transformation modules is provided by the XML Abstract Interface Form (XAIF). XAIF provides an abstract, language-independent representation of language constructs common in imperative languages, such as C and Fortran. We describe the use of this architecture in constructing tools for automatic differentiation of Fortran 77 and ANSI C, and we discuss how access to compiler optimization techniques can enable more efficient derivative augmentation.
Write barrier removal by static analysis
Authors: Zee Karen , Rinard Martin
Published: November 2005

We present a set of static analyses for removing write barriers in programs that use generational garbage collection. To our knowledge, these are the first analyses for this purpose. Our
Intraprocedural
analysis uses a flow-sensitive pointer analysis to locate variables that must point to the most recently allocated object, then eliminates write barriers on stores to objects accessed via one of these variables. The
Callee Type Extension
incorporates information about the types of objects allocated in invoked methods, while the
Caller Context Extension
incorporates information about the most recently allocated object at call sites that invoke the currently analyzed method. Results from our implemented system show that our
Full Interprocedural
analysis, which incorporates both extensions, can eliminate the majority of the write barriers in most of the programs in our benchmark set, producing modest performance improvements of up to 7% of the overall execution time. Moreover, by dynamically instrumenting the executable, we are able to show that for all but two of our nine benchmark programs, our analysis is close to optimal in the sense that it eliminates the write barriers for almost all store instructions observed not to create a reference from an older object to a younger object.
Smart proxies for Jini services
Authors: Ledru Pascal
Published: November 2005

Jini has been advertised as a self-healing infrastructure where both services and consumers of these services come and go. However, it does not explicitly address the issue of how to recover when a consumer communicates with a service, which suddenly fails. This paper presents how smart proxies can be implemented in a Jini environment, allowing a client to transparently reconnect to another instance of a service in case of a failure. An important feature of the Java language: dynamic proxy is used to allow this transparent reconnection scheme.
Good design principles in a compiler university course
Authors: Acebal César F. , Castanedo Raúl Izquierdo , Cueva Lovelle Juan M.
Published: November 2005

This paper presents what aims to be an example of good design principles applied to compiler construction. To be more specific, it presents an interpreter of a very simple object oriented language, called SmallScript, that has been designed to be taught in a Compiler University course. Our aim is not to develop a new, revolutionary language, neither to show a spectacular advance in some research field of compiler construction. Instead, as university teachers, we aim to offer both students and teachers an example of how a modern interpreter can be designed, focusing on object orientation and using modern tools like JavaCC and JJTrree.
GRAMOL
Authors: Genillard C. , Strohmeier A.
Published: November 2005

A language for defining the lexical and syntactic grammars of languages is presented. The same notation is used for the two grammar descriptions. We will show that the language is unstratified, that is it can be used as its own metalanguage. Automatic generation of lexical analysers and syntactic parsers has been achieved by means of Ada packages.
Grammars for FFP
Authors: Lang J. E.
Published: November 2005

In Backus's original paper on FP and FFP [1], the syntax of these language is described informally. Though a formal syntax for Berkeley FP has appeared in print [2], no formal representation of FFP syntax has yet appeared. It is desirable to have such a formal representation for implementation purposes, and such a representation may also be useful for specifying where the syntax of FFP ends and its semantics begins. In this paper, we will write down formal grammars for FFP based on the syntax as given by Backus [1] and Williams [3] and will discuss their semantic implications. A third grammar similar to that for FP is presented and it may be used for implementing the language.
ESP
Authors: Das Manuvir , Lerner Sorin , Seigle Mark
Published: November 2005

In this paper, we present a new algorithm for partial program verification that runs in polynomial time and space. We are interested in checking that a program satisfies a given temporal safety property. Our insight is that by accurately modeling only those branches in a program for which the property-related behavior differs along the arms of the branch, we can design an algorithm that is accurate enough to verify the program with respect to the given property, without paying the potentially exponential cost of full path-sensitive analysis.We have implemented this "property simulation" algorithm as part of a partial verification tool called ESP. We present the results of applying ESP to the problem of verifying the file I/O behavior of a version of the GNU C compiler (gcc, 140,000 LOC). We are able to prove that all of the 646 calls to
.fprintf
in the source code of gcc are guaranteed to print to valid, open files. Our results show that property simulation scales to large programs and is accurate enough to verify meaningful properties.
A system and language for building system-specific, static analyses
Authors: Hallem Seth , Chelf Benjamin , Xie Yichen , Engler Dawson
Published: November 2005

This paper presents a novel approach to bug-finding analysis and an implementation of that approach. Our goal is to find as many serious bugs as possible. To do so, we designed a flexible, easy-to-use extension language for specifying analyses and an efficent algorithm for executing these extensions. The language,
metal
, allows the users of our system to specify a broad class of analyses in terms that resemble the intuitive description of the rules that they check. The system,
xgcc
, executes these analyses efficiently using a context-sensitive, interprocedural analysis. Our prior work has shown that the approach described in this paper is effective: it has successfully found thousands of bugs in real systems code. This paper describes the underlying system used to achieve these results. We believe that our system is an effective framework for deploying new bug-finding analyses quickly and easily.
Post-pass binary adaptation for software-based speculative precomputation
Authors: Liao Steve S.W. , Wang Perry H. , Wang Hong , Hoflehner Gerolf , Lavery Daniel , Shen John P.
Published: November 2005

Recently, a number of thread-based prefetching techniques have been proposed. These techniques aim at improving the latency of single-threaded applications by leveraging multithreading resources to perform memory prefetching via speculative prefetch threads. Software-based speculative precomputation (SSP) is one such technique, proposed for multithreaded Itanium models. SSP does not require expensive hardware support-instead it relies on the compiler to adapt binaries to perform prefetching on otherwise idle hardware thread contexts at run time. This paper presents a post-pass compilation tool for generating SSP-enhanced binaries. The tool is able to: (1) analyze a single-threaded application to generate prefetch threads; (2) identify and embed trigger points in the original binary; and (3) produce a new binary that has the prefetch threads attached. The execution of the new binary spawns the speculative prefetch threads, which are executed concurrently with the main thread. Our results indicate that for a set of pointer-intensive benchmarks, the prefetching performed by the speculative threads achieves an average of 87% speedup on an in-order processor and 5% speedup on an out-of-order processor.
Beltway
Authors: Blackburn Stephen M , Jones Richard , McKinley Kathryn S. , Moss J Eliot B
Published: November 2005

We present the design and implementation of a new garbage collection framework that significantly generalizes existing copying collectors. The
Beltway
framework exploits and separates object age and incrementality. It groups objects in one or more increments on queues called
belts
, collects belts independently, and collects increments on a belt in first-in-first-out order. We show that Beltway configurations, selected by command line options, act and perform the same as semi-space, generational, and older-first collectors, and encompass all previous copying collectors of which we are aware. The increasing reliance on garbage collected languages such as Java requires that the collector perform well. We show that the generality of Beltway enables us to design and implement new collectors that are robust to variations in heap size and improve total execution time over the best generational copying collectors of which we are aware by up to 40%, and on average by 5 to 10%, for small to moderate heap sizes. New garbage collection algorithms are rare, and yet we define not just one, but a new family of collectors that subsumes previous work. This generality enables us to explore a larger design space and build better collectors.
Efficient discovery of regular stride patterns in irregular programs and its use in compiler prefetching
Authors: Wu Youfeng
Published: November 2005

Irregular data references are difficult to prefetch, as the future memory address of a load instruction is hard to anticipate by a compiler. However, recent studies as well as our experience indicate that some important load instructions in irregular programs contain stride access patterns. Although the load instructions with stride patterns are difficult to identify with static compiler techniques, we developed an efficient profiling method to discover these load instructions. The new profiling method integrates the profiling for stride information and the traditional profiling for edge frequency into a single profiling pass. The integrated profiling pass runs only 17% slower than the frequency profiling alone. The collected stride information helps the compiler to identify load instructions with stride patterns that can be prefetched efficiently and beneficially. We implemented the new profiling and prefetching techniques in a research compiler for Itanium Processor Family (IPF), and obtained significant performance improvement for the SPECINT2000 programs running on Itanium machines. For example, we achieved a 1.59x speedup for 181.mcf, 1.14x for 254.gap, and 1.08x for 197.parser. We also showed that the performance gain is stable across input data sets. These benefits make the new profiling and prefetching techniques suitable for production compilers.
Static load classification for improving the value predictability of data-cache misses
Authors: Burtscher Martin , Diwan Amer , Hauswirth Matthias
Published: November 2005

While caches are effective at avoiding most main-memory accesses, the few remaining memory references are still expensive. Even one cache miss per one hundred accesses can double a program's execution time. To better tolerate the data-cache miss latency, architects have proposed various speculation mechanisms, including load-value prediction. A load-value predictor guesses the result of a load so that the dependent instructions can immediately proceed without having to wait for the memory access to complete. To use the prediction resources most effectively, speculation should be restricted to loads that are likely to miss in the cache and that are likely to be predicted correctly. Prior work has considered hardware- and profile-based methods to make these decisions. Our work focuses on making these decisions at compile time. We show that a simple compiler classification is effective at separating the loads that should be speculated from the loads that should not. We present results for a number of C and Java programs and demonstrate that our results are consistent across programming languages and across program inputs.
Extended static checking for Java
Authors: Flanagan Cormac , Leino K. Rustan M. , Lillibridge Mark , Nelson Greg , Saxe James B. , Stata Raymie
Published: November 2005

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static Checker for Java (ESC/Java), an experimental compile-time program checker that finds common programming errors. The checker is powered by verification-condition generation and automatic theorem-proving techniques. It provides programmers with a simple annotation language with which programmer design decisions can be expressed formally. ESC/Java examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotations and the actual code, and also warns of potential runtime errors in the code. This paper gives an overview of the checker architecture and annotation language and describes our experience applying the checker to tens of thousands of lines of Java programs.
Using data groups to specify and check side effects
Authors: Leino K. Rustan M. , Poetzsch-Heffter Arnd , Zhou Yunhong
Published: November 2005

Reasoning precisely about the side effects of procedure calls is important to many program analyses. This paper introduces a technique for specifying and statically checking the side effects of methods in an object-oriented language. The technique uses
data groups
, which abstract over variables that are not in scope, and limits program behavior by two alias-confining restrictions,
pivot uniqueness
and
owner exclusion
. The technique is shown to achieve modular soundness and is simpler than previous attempts at solving this problem.
MaJIC
Authors: Almási George , Padua David
Published: November 2005

This paper presents and evaluates techniques to improve the execution performance of MATLAB. Previous efforts concentrated on source to source translation and batch compilation;
MaJIC
provides an interactive frontend that looks like MATLAB and compiles/optimizes code behind the scenes in real time, employing a combination of just-in-time and speculative ahead-of-time compilation. Performance results show that the proper mixture of these two techniques can yield near-zero response time as well as performance gains previously achieved only by batch compilers.
The embedded machine
Authors: Henzinger Thomas A. , Kirsch Christoph M.
Published: November 2005

The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first, platform-independent compiler phase generates E code (code executed by the Embedded Machine), which supervises the timing ---not the scheduling--- of application tasks relative to external events, such as clock ticks and sensor interrupts. E~code is portable and exhibits, given an input behavior, predictable (i.e., deterministic) timing and output behavior. The second, platform-dependent compiler phase checks the
time safety
of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter.
Bisimulation congruences in safe ambients
Authors: Merro Massimo , Hennessy Matthew
Published: November 2005

We study a variant of Levi and Sangiorgi's Safe Ambients (SA) enriched with
passwords
(SAP). In SAP by managing passwords, for example generating new ones and distributing them selectively, an ambient may now program who may migrate into its computation space, and when. Moreover in SAP an ambient may provide different services depending on the passwords exhibited by its incoming clients.We give an
lts
based operational semantics for SAP and a labelled
bisimulation
based equivalence which is proved to coincide with barbed congruence.Our notion of bisimulation is used to prove a set of algebraic laws which are subsequently exploited to prove more significant examples.
Bounding space usage of conservative garbage collectors
Authors: Boehm Hans-J.
Published: November 2005

Conservative garbage collectors can automatically reclaim unused memory in the absence of precise pointer location information. If a location can possibly contain a pointer, it is treated by the collector as though it contained a pointer. Although it is commonly assumed that this can lead to unbounded space use due to misidentified pointers, such extreme space use is rarely observed in practice, and then generally only if the number of misidentified pointers is itself unbounded.We show that if the program manipulates only data structures satisfying a simple
GC-robustness
criterion, then a bounded number of misidentified pointers can at most result in increasing space usage by a constant factor. We argue that nearly all common data structures are already GC-robust, and it is typically easy to identify and replace those that are not. Thus it becomes feasible to prove space bounds on programs collected by mildly conservative garbage collectors, such as the one in [2]. The worst-case space overhead introduced by such mild conservatism is comparable to the worst-case fragmentation overhead for inherent in any non-moving storage allocator.The same GC-robustness criterion also ensures the absence of temporary space leaks of the kind discussed in [13] for generational garbage collectors.
The hardness of cache conscious data placement
Authors: Petrank Erez , Rawitz Dror
Published: November 2005

The growing gap between the speed of memory access and cache access has made cache misses an influential factor in program efficiency. Much effort has been spent recently on reducing the number of cache misses during program run. This effort includes wise rearranging of program code, cache-conscious data placement, and algorithmic modifications that improve the program cache behavior. In this work we investigate the complexity of finding the optimal placement of objects (or code) in the memory, in the sense that this placement reduces the cache misses to the minimum. We show that this problem is one of the toughest amongst the interesting algorithmic problems in computer science. In particular, suppose one is given a sequence of memory accesses and one has to place the data in the memory so as to minimize the number of cache misses for this sequence. We show that if P ≠ NP, then one cannot efficiently approximate the optimal solution even up to a very liberal approximation ratio. Thus, this problem joins the small family of extremely inapproximable optimization problems. The other two famous members in this family are minimum coloring and maximum clique.
From POPL to the classroom and back
Authors: Felleisen Matthias
Published: November 2005

This invited talk presents an overview of the TeachScheme! and DrScheme projects. The former aims at bringing the principles of programming and programming languages into the introductory programming curriculum. The latter is a program development environment that supports the pedagogy and design principles of the TeachScheme! project. Carrying out these projects enriched our research life with many interesting programming language and system design problems.
CCured
Authors: Necula George C. , McPeak Scott , Weimer Westley
Published: November 2005

In this paper we propose a scheme that combines type inference and run-time checking to make existing C programs type safe. We describe the CCured type system, which extends that of C by separating pointer types according to their usage. This type system allows both pointers whose usage can be verified statically to be type safe, and pointers whose safety must be checked at run time. We prove a type soundness result and then we present a surprisingly simple type inference algorithm that is able to infer the appropriate pointer kinds for existing C programs.Our experience with the CCured system shows that the inference is very effective for many C programs, as it is able to infer that most or all of the pointers are statically verifiable to be type safe. The remaining pointers are instrumented with efficient run-time checks to ensure that they are used safely. The resulting performance loss due to run-time checks is 0-150%, which is several times better than comparable approaches that use only dynamic checking. Using CCured we have discovered programming bugs in established C programs such as several SPECINT95 benchmarks.
An efficient profile-analysis framework for data-layout optimizations
Authors: Rubin Shai , Bodík Rastislav , Chilimbi Trishul
Published: November 2005

Data-layout optimizations rearrange fields within objects, objects within objects, and objects within the heap, with the goal of increasing spatial locality. While the importance of data-layout optimizations has been growing, their deployment has been limited, partly because they lack a unifying framework. We propose a parameterizable framework for data-layout optimization of general-purpose applications. Acknowledging that finding an optimal layout is not only NP-hard, but also poorly approximable, our framework finds a good layout by searching the space of possible layouts, with the help of profile feedback. The search process iteratively prototypes candidate data layouts, evaluating them by "simulating" the program on a representative trace of memory accesses. To make the search process practical, we develop space-reduction heuristics and optimize the expensive simulation via memoization. Equipped with this iterative approach, we can synthesize layouts that outperform existing non-iterative heuristics, tune application-specific memory allocators, as well as compose multiple data-layout optimizations.
Stochastic lambda calculus and monads of probability distributions
Authors: Ramsey Norman , Pfeffer Avi
Published: November 2005

Probability distributions are useful for expressing the meanings of probabilistic languages, which support formal modeling of and reasoning about uncertainty. Probability distributions form a monad, and the monadic definition leads to a simple, natural semantics for a stochastic lambda calculus, as well as simple, clean implementations of common queries. But the monadic implementation of theexpectationquery can be much less efficient than current best practices in probabilistic modeling. We therefore present a language ofmeasure terms, which can not only denote discrete probability distributions but can also support the best known modeling techniques. We give a translation of stochastic lambda calculus into measure terms. Whether one translates into the probability monad or into measure terms, the results of the translations denote the same probability distribution.
The first-order theory of subtyping constraints
Authors: Su Zhendong , Aiken Alexander , Niehren Joachim , Priesnitz Tim , Treinen Ralf
Published: November 2005

We investigate the first-order of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and non-structural subtyping. The decidability results are shown by reduction to a decision problem on tree automata. This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.
Scalable formal design methods for asynchronous VLSI
Authors: Manohar Rajit
Published: November 2005

This lecture will provide an overview of the field of asynchronous VLSI, and show how formal methods have played a critical role in the design of complex asynchronous systems. In particular, I will talk about program transformations and their application to asynchronous VLSI, as well as describe a simple language that I developed to describe these circuits and aid in their validation.
Proving correctness of compiler optimizations by temporal logic
Authors: Lacey David , Jones Neil D. , Van Wyk Eric , Frederiksen Carl Christian
Published: November 2005

Many classical compiler optimizations can be elegantly expressed using rewrite rules of form:
I
⇒
I
′ if
φ
, where
I
,
I
′ are intermediate language instructions and
φ
is a property expressed in a temporal logic suitable for describing program data flow. Its reading: If the current program π contains an instruction of form
I
at some control point
p
, and if flow condition
φ
is satisfied at
p
, then replace
I
by
I
′.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations, dead code elimination, constant folding and code motion. The meaning of correctness is that for any program π, if
Rewrite
(π, π′,
p
,
I
⇒
I
′ if φ) then [[π]] = [[π′]], i.e. π and π′ have exactly the same semantics.