bluuebunny/crossref_metadata_2025 huggingface dataset:
Testing for software reliability
Authors: Brown J. R. , Lipow M.
Published: November 2005

This paper presents a formulation of a novel methodology for evaluation of testing in support of operational reliability assessment and prediction. The methodology features an incremental evaluation of the representativeness of a set of development and validation test cases together with definition of additional test cases to enhance those qualities.

If test cases are derived in typical fashion (i.e., to find and remove bugs, to investigate software performance under off-nominal conditions, to exercise structural elements and functional capabilities of the software, and to demonstrate satisfaction of software requirements), then the complete set of test cases is not necessarily representative of anticipated operational usage. The paper reports on initial research into formulation of valid measures of testing representativeness.

Several techniques which permit specification of expected operational usage are described, and a technique for evaluating the correlation between actual testing accomplished and expected operational usage is defined. An unbiased estimator for operational usage reliability is proposed and justified as a function of a specified operational profile; confidence in the estimate is derived from a measure of the degree to which testing is representative of expected operational application.

An experimental application of the techniques to a small program is provided as an illustration of the proposed use of the methodology for operational software reliability estimation. The relationship between structural exercise testing thoroughness and operational usage representativeness is discussed; the specification of a quantified reliability requirement and an explicit, required representativeness measure (or confidence) is identified as integral to effective application of the proposed reliability testing methodology; efforts to extend, formalize and generalize the methodology are described; and expected benefits, as well as potential problems and limitations are identified.
Aspects of applicative programming for file systems (Preliminary Version)
Authors: Friedman Daniel P. , Wise David S.
Published: November 2005

This paper develops the implications of recent results in semantics for applicative programming. Applying suspended evaluation (call-by-need) to the arguments of file construction functions results in an implicit synchronization of computation and output. The programmer need not participate in the determination of the pace and the extent of the evaluation of his program. Problems concerning multiple input and multiple output files are considered: typical behavior is illustrated with an example of a rudimentary text editor written applicatively. As shown in the trace of this program, the driver of the program is the sequential output device(s). Implications of applicative languages for I/O bound operating systems are briefly considered.
Towards a discipline of real-time programming
Authors: Wirth N.
Published: November 2005

Programming is divided into three major categories with increasing complexity of reasoning in program validation: sequential programming,
multi
-programming, and
real-time
programming. By adhering to a strict programming
discipline
and by using a suitable high-level
language
molded after this discipline, we may drastically reduce the complexity of reasoning about concurrency and execution time constraints. This may be the only practical way to make real-time systems analytically verifyable and ultimately reliable. A possible discipline is outlined and expressed in terms of the language
Modula
.
Displaying IDL instances
Authors: Snodgrass Richard Thomas
Published: November 2005

Debugging a complex system can be aided by displaying the internal data structures manipulated by the system. We examine one generic Unix tool and four IDL-specific tools, focussing on their functionality and ability to handle large data structures gracefully.
IDL as a data description language for a programming environment database
Authors: Didriksen T. , Lie A. , Conradi R.
Published: November 2005

A programming environment (PE) consists of a multitude of different tools. The cooperation between the tools is crucial to the overall functionality and performance of the PE.This paper argues that a common underlying database can facilitate tool cooperation, and that IDL can be used to describe the interface between the tools and the database management system (DBMS).
C++ versus LISP: a case study
Authors: Trickey Howard
Published: November 2005

A large application program was simultaneously coded in both C++ and Lisp. This note compares the two implementations. The conclusion is that programming in the two languages takes roughly the same amount of time and effort, but C++ seems better for a number of reasons.
A standard for a graph representation for functional programs
Authors: Joy Mike , Axford Tom
Published: November 2005

The data structures used in the authors' functional language graph reduction implementations are described, together with a standard notation for representing the graphs in a textual format. The graphs employed are compatible with FLIC and with the functional languages in use at Birmingham and Warwick. The textual format is designed to be transmittable easily across networks.
Implementation of an optimizing compiler for VHDL
Authors: Bhasker J.
Published: November 2005

We present techniques used to implement an optimizing compiler for the VHSIC hardware description language (VHDL). We present details about the LR parser used to parse the input program. An efficient intermediate representation, called a process graph, is constructed as a result of the parsing. This representation is chosen to facilitate the ease of data flow analyses and optimizations. The process graph is a reducible flow graph because of the restricted subset of VHDL that we work with. The various data flow analyses and optimization techniques that have been implemented are described. This optimizing compiler is being used as a front end for a tool that performs behavioral synthesis.
Bindings persistent programming languages
Authors: Morrison R. , Atkinson M. P. , Brown A. L. , Dearle A.
Published: November 2005

In designing and building persistent object systems we are attempting to regularise the activities on data that are traditional in programming languages, operating systems, database management systems and file systems. We hypothesise that regularity and simplicity may be achieved by regarding the exercise as one of designing a language powerful enough to allow for all our programming needs and using some principles in the design of the language to achieve this regularity and simplicity.In this paper we investigate the nature of binding mechanisms showing how some form of dynamic binding is necessary for persistence. The binding mechanisms of Ada, which has a traditional file based view of persistence, and of Napier, which has an object based view, are used as illustrations.
Implementing functional languages on a combinator-based reduction machine
Authors: Sarwar S. M. , Hahn S. J. , Davis J. A.
Published: November 2005

This paper describes the results of a study done at Iowa State University as part of a larger effort to develop a fine-grained parallel architecture [5]. The goal is to find most heavily used combinators using Turner's method of graph reduction for a wide range of programming styles. The study shows thai there are families and strings of combinators that are used frequently. Optimization of such combinators promises an efficient sequential reduction machine based upon the combinator model.
Concurrent programming language—LISPTALK
Authors: Li Chang
Published: November 2005

LISPTALK is a concurrent language which is based on both LISP and CSP. It is a process-oriented language. Besides the idea of pure LISP and CSP, its main features are COTALK, CHANNEL-PORT, and LINK. Within a process there may exist many LISP functions which can be defined by recursion. The communication among processes uses INPUT and OUTPUT function through CHANNEL-PORT. The LINK connects the CHANNEL-PORTS of processes staticlly and synchronizes the communication. LISPTALK can be used to object-oriented programming like SMALLTALK-80. The language is also suit for vision understanding and robotics. The most interesting is the similarity between LISPTALK's structure and human brain structure.
A common-LISP implementation of an extended Prolog system
Authors: Cattaneo Giuseppe , Loia Vincenzo
Published: November 2005

This paper presents an extended Common LISP implementation of a PROLOG interpreter named CL-Prolog, giving a detailed description of the major problems met and the principal data structures and algorithms used for their solution.A sort of PROLOG virtual processor has been implemented whose instructions are defined using LISP as microcode; particular attention is payed to the the Memory Management Unit and the basic Control Mechanism.The reader is supposed to be accustomed with PROLOG Programming and the evaluation of the first order Logic Predicates.The main characteristics of CL-Prolog are:- Clean separation from the host language.- Tail recursion handling and binding mechanism optimization.- Portability, flexibility, and extendibility of basic model.- Interaction between PROLOG code and host LISP interpreter.Interpreter's core is separated in three big modules in order to cut off the different issues :- the reader, the evaluator, and the resources manager -Finally the introduction of a double-stack recursion management has sped up the Backtracking mechanism; the resulting overall performances of this interpreter are really comparable to other commercial one even when they are implemented using procedural languages, supposed faster, confirming the possibility of using very high level languages as effective tools for real implementations.
Please: a language combining imperative and logic programming
Authors: Terwilliger Robert B.
Published: November 2005

PLEASE is an Ada®-based, executable specification language which supports a formal development method similar to VDM. Like ANNA, PLEASE allows software to be annotated with formulae written in predicate logic; annotations can be used in proofs of correctness and to generate run-time assertion checks. PLEASE differs from ANNA by restricting the logic used in annotations to Horn clauses; therefore, PLEASE specifications can also be transformed into prototypes which use Prolog to "execute" pre- and post-conditions. We believe the early production of executable prototypes will enhance the development process. We also believe the restriction to Horn clauses will allow us to build on the significant research being performed on logic-based programming languages and databases. In this paper we give an overview of PLEASE, present an example specification, describe the translation of PLEASE specifications into Prolog procedures, and discuss some of the techniques used to obtain acceptable efficiency in the resultant prototypes.
Portability of software
Authors: Kaindl Hermann
Published: November 2005

This paper is based on experiences with several ports of large programs written in modern high-level languages. Even today, porting software is very often problematic and costly in practice. Thus it seems important to find out what can be learned from such experiences in order to solve these problems better in the future and consequently to reduce the related costs. First, a definition of the term
port
is given to clarify the important relationships of a program with the
environments
involved. A
layered model
is built around the
standard
of a programming language, and based on this model "rules" for writing portable programs are stated. It appears that both the layered model and the rules are principally valid for many important languages, in particular also Ada®. While this language will bring us a large step closer to portable software, we will have to face portability problems also in the future.
OPG: an optimizing parser generator
Authors: Roberts George H.
Published: November 2005

A
source program-target program
pair is to a compiler as a
grammar-parser
pair is to a parser generator.This analogy reflects the belief that because optimizing compilers exist, optimizing parser generators should exist. This paper shows that they do exist, and how one was constructed.
FLIC—a functional language intermediate code
Authors: Jones S. L. Peyton
Published: November 2005

FLIC is a Functional Language Intermediate Code, intended to provide a common intermediate language between diverse implementations of functional languages, including parallel ones. This paper gives a formal definition of FLIC's syntax and semantics, in the hope that its existence may encourage greater exchange of programs and benchmarks between research groups.
A note on the speed of Prolog
Authors: Paakki J.
Published: November 2005

Based on an experiment in compiler writing methods, we discuss the speed of Prolog programs of modest size when compared with operationally equivalent Pascal programs. We have produced three versions of a compiler for the programming language Edison using three different tools: Pascal, Prolog, and a compiler writing system (GAG). The Prolog and Pascal programs analyzed in this case are the semantic analysis and the code transformation phases of the Edison compiler. Our analysis shows that it is possible to write Prolog programs that are able to compete in speed with the corresponding programs written in Pascal.
New developments in Pascal-SC
Authors: Bohlender G. , Ullrich Ch. , von Gudenberg J. Wolff
Published: November 2005

PASCAL-SC is an efficient programming language for scientific computation which was developed at the beginning of the eighties as an extension of standard PASCAL. It provides arithmetical operations with controlled rounding and an optimal scalar product. Functions with arbitrary result type and an operator concept permit the realization of higher arithmetical operations, such as matrix-vector operations. The application of PASCAL-SC for the development of reliable numerical software raised several wishes for further extension. These extensions have been incorporated in the language.A new data type dotprecision together with arithmetic operations is introduced permitting scalar product expressions to be evaluated with maximum accuracy in a convenient manner. Dynamic arrays and a module concept support the definition of numeric libraries. Over loading of functions and procedures improve the readability of scientific programs. A program for the verified solution of linear systems illustrates the strength of the new language.
Using dynamic programming to generate optimized code in a Graham-Glanville style code generator
Authors: Christopher Thomas W. , Hatcher Philip J. , Kukuk Ronald C.
Published: November 2005

We have performed an investigation of using a dynamic programming to generate optimized code in a Graham-Glanville style code generator We use Earley's algorithm rather than an IR algorithm for parsing in the code generator Not only does the use of Earley's algorithm make the construction of the code generator very easy it allows the selection of optimal code by dynamic programming (using a modification of the technique developed by Lvon) We compare two implementations of this technique to conventional hand-coded code generators using a subset of BASIC as the source language Further we discuss the use of this technique in an experimental C compiler.
Attribute coupled grammars
Authors: Ganzinger Harald , Giegerich Robert
Published: November 2005

In this paper, attribute grammars are viewed as specifying translations from source language terms into target language terms. The terms are constructed over a hierarchical signature consisting of a semantic and a syntactic part. Attribute grammars are redefined to become morphisms in the category of such signatures, called attribute coupled grammars, such that they come with an associative composition operation. The composition allows for a new kind of modularity in compiler specifications. The paper also discusses properties of the concept with respect to attribute evaluation and application as a tree transformation device.
Inline routines in VAXELN Pascal
Authors: MacLaren M. Donald
Published: November 2005

This paper describes the implementation of inline procedures and functions inthe VAXELN Pascal compiler. Inline expansion translates the reverse Polish text produced by the parser into an intermediate language like that used in the VAX-11 PL/I and C compilers. The paper gives detailed descriptions of the front end's organization as it relates to inline routines and of the symbol substitutions made during inline expansion. The paper also discusses global optimization and the compiler's treatment of dynamically sized data, which is based on parametric types.
A portable optimizing compiler for Modula-2
Authors: Powell Michael L.
Published: November 2005

A portable compiler for the Modula-2 programming language has been implemented with a simple, machine independent optimizer. The front end of the compiler generates a dialect of P-code, and the back end translates the P-code into machine language. The compiler fits well in the Unix environment.The design philosophy of the compiler "best simple". Whenever possible, design decisions were made to favor the simplest alternative that got us most of what we wanted. Benchmark results show that the code quality is comparable to or better than other good compilers.
Points-to analysis for Java using annotated constraints
Authors: Rountev Atanas , Milanova Ana , Ryder Barbara G.
Published: November 2005

The goal of point-to analysis for Java is to determine the set of objects pointed by a reference variable or a reference object field. This information has a wide variety of client applications in optimizing compilers and software engineering tools. In this paper we present a point-to analysis for Java based on Andersen's point-to analysis for C [5]. We implement the analysis by using a constraint-based approach which employs
annotated inclusion constraints.
Constraint annotations allow us model precisely and efficiently the semantics of virtual calls and the flow of values through object fields. By solving systems of annotated inclusion constraints, we have been albe to perform practical and precies points-to analysis for Java
Regression test selection for Java software
Authors: Harrold Mary Jean , Jones James A. , Li Tongyu , Liang Donglin , Orso Alessandro , Pennings Maikel , Sinha Saurabh , Spoon S. Alexander , Gujarathi Ashish
Published: November 2005

Regression testing is applied to modified software to provide confidence that the changed parts behave as intended and that the unchanged parts have not been adversely affected by the modifications. To reduce the cost of regression testing, test cases are selected from the test suite that was used to test the original version of the software---this process is called regression test selection. A
safe
regression-test-selection algorithm selects every test case in the test suite that may reveal a fault in the modified software. Safe regression-test-selection technique that, based on the use of a suitable representation, handles the features of the Java language. Unlike other safe regression test selection techniques, the presented technique also handles incomplete programs. The technique can thus be safely applied in the (very common) case of Java software that uses external libraries of components; the analysis of the external code is note required for the technique to select test cases for such software. The paper also describes RETEST, a regression-test-selection algorithm can be effective in reducing the size of the test suite.
Pretenuring for Java
Authors: Blackburn Stephen M. , Singhai Sharad , Hertz Matthew , McKinely Kathryn S. , Moss J. Eliot B.
Published: November 2005

Pretenuring can reduce copying costs in garbage collectors by allocating long-lived objects into regions that the garbage collector with rarely, if ever, collect. We extend previous work on pretenuring as follows. (1) We produce pretenuring advice that is neutral with respect to the garbage collector algorithm and configuration. We thus can and do combine advice from different applications. We find that predictions using object lifetimes at each allocation site in Java prgroams are accurate, which simplifies the pretenuring implementation. (2) We gather and apply advice to applications and the Jalapeño JVM, a compiler and run-time system for Java written in Java. Our results demonstrate that building combined advice into Jalapeño from different application executions improves performance regardless of the application Jalapeño is compiling and executing. This
build-time
advice thus gives user applications some benefits of pretenuring without any application profiling. No previous work pretenures in the run-time system. (3) We find that application-only advice also improves performance, but that the combination of build-time and application-specific advice is almost always noticeably better. (4) Our same advice improves the performance of generational and Older First colleciton, illustrating that it is
collector neutral
.
From Pascal to Delphi to Object Pascal-2000
Authors: Gofen Alexander
Published: November 2005

The evolution of Pascal to Delphi, the powerful and elegant features of that language and RAD environment are discussed. Yet the evolution was not smooth, some inconsistencies and glitches built up. So the next version of the language named Object Pascal 2000 is suggested. It eliminates the inconsistencies, improves the language and sets the fundamentals for standardizing it.
Class-is-type is inadequate for object reuse
Authors: Yu Sheng
Published: November 2005

It is well known that class and type are two different concepts in object-oriented programming languages (OOPLs). However, in many popular OOPLs, classes are used as types. In this paper, we argue that the class-is-type principle is a major obstacle to software reuse, especially to object reuse. The concepts of the basic entities, i.e., objects, object classes, object types, and object kinds, in the type hierarchy of OOPLs are revisited. The notion of object reuse is defined and elaborated. In addition, we show that parameterized types and generic functions are better served by used kind-bounded quantification than universal quantification and other mechanisms.
Type-based hot swapping of running modules (extended abstract)
Authors: Duggan Dominic
Published: November 2005

While dynamic linking has become an integral part of the run-time execution of modem programming languages, there is increasing recognition of the need for support for hot swapping of running modules, particularly in long-lived server applications. The interesting challenge for such a facility is to allow the new module to change the types exported by the original module, while preserving type safety. This paper describes a type-based approach to hot swapping running modules. The approach is based on a reflective mechanism for dynamically adding type sharing constraints to the type system, realized by programmer-defined version adapters in the run-time.
Charting patterns on price history
Authors: Anand Saswat , Chin Wei-Ngan , Khoo Siau-Cheng
Published: November 2005

It is an established notion among financial analysts that price moves in patterns and these patterns can be used to forecast future price. As the definitions of these patterns are often subjective, every analyst has a need to define and search meaningful patterns from historical time series quickly and efficiently. However, such discovery process can be extremely laborious and technically challenging in the absence of a high-level pattern definition language. In this paper, we propose a chart-pattern language (CPL for short) to facilitate pattern discovery process. Our language enables financial analysts to (1) define patterns with subjective criteria, through introduction of fuzzy constraints, and (2) incrementally compose complex patterns from simpler patterns. We demonstrate through an array of examples how real life patterns can be expressed in CPL. In short, CPL provides a high-level platform upon which analysts can define and search patterns easily and without any programming expertise. CPL is a domain-specific language embedded in Haskell. We show how various features of a functional language, such as pattern matching, higher-order functions, lazy evaluation, facilitate pattern definitions and implementation. Furthermore Haskell's type system frees the Programmers from annotating the programs with types.
A new notation for arrows
Authors: Paterson Ross
Published: November 2005

The categorical notion of monad, used by Moggi to structure denotational descriptions, has proved to be a powerful tool for structuring combinator libraries. Moreover, the monadic programming style provides a convenient syntax for many kinds of computation, so that each library defines a new sublanguage. Recently, several workers have proposed a generalization of monads, called variously "arrows" or Freyd-categories. The extra generality promises to increase the power, expressiveness and efficiency of the embedded approach, but does not mesh as well with the native abstraction and application. Definitions are typically given in a point-free style, which is useful for proving general properties, but can be awkward for programming specific instances. In this paper we define a simple extension to the functional language Haskell that makes these new notions of computation more convenient to use. Our language is similar to the monadic style, and has similar reasoning properties. Moreover, it is extensible, in the sense that new combining forms can be defined as expressions in the host language.
Growing languages with metamorphic syntax macros
Authors: Brabrand Claus , Schwartzbach Michael I.
Published: November 2005

"From now on, a main goal in designing a language should be to plan for growth." Guy Steele: Growing a Language, OOPSLA '98 invited talk
.We present our experiences with a syntax macro language which we claim forms a general abstraction mechanism for growing (domain-specific) extensions of programming languages. Our syntax macro language is designed to guarantee
type safety
and
termination
.A concept of
metamorphisms
allows the arguments of a macro to be inductively defined in a
meta
level grammar and
morphed
into the host language. We also show how the metamorphisms can be made to operate simultaneously on multiple parse trees at once. The result is a highly flexible mechanism for growing new language constructs without resorting to compile-time programming. In fact, whole new languages can be defined at surprisingly low cost.This work is fully implemented as part of the
bigwig
system for defining interactive Web services, but could find use in many other languages.
Forth report
Authors: Frenger Paul
Published: November 2005

Human progress advances in many ways. One method obvious to all is to take something, a bicycle for instance, and make a multitude of small changes to the design over time. Each iteration of the refinement process gives us something newer and nicer to appreciate. That's how you start out with a $50 Schwinn bike and end up with a $10,000 Lotus racing bicycle.Another method is to add another layer of complexity onto the original design, some new technology never expected by the inventors of the product or device, to prevent natural obsolescence. An example here might be the internal combustion engine, invented in the pre-smog 1800's. Many layers of complexity have been applied to this product over the decades. Take fuel management for instance: we have gone from simple mechanical carburetion, to computerized electronic fuel injection, then added forced induction by supercharging / turbocharging. Each layer builds upon (and sometimes replaces) one or more older layers underneath itself.My homemade terminology for adding another layer of complexity or sophistication onto something where it wasn't found before is "strap-on technology". Where does the "strap-on" part come in? It's like in the movie,
Six Days, Seven Nights
by Touchstone Pictures, 1998 [1]. During an in-flight emergency, Harrison Ford crashes his tourist airplane on the beach of a small Pacific island, incidentally breaking the wheels of his landing gear in the process and stranding himself and Ann Heche there. He later finds two usable pontoons from a derelict 1940-era Japanese seaplane in the jungle. He uses vines and ropes to "strap-on" these pontoons over his broken wheels, thus enabling an essential water takeoff to escape from the tiny beach of that island. Ford "layered" the more advanced technology (pontoons for water takeoffs and landings) over the less advanced wheeled gear, in making his escape. The "strap-on" pontoons advance this movie's plot while, incidentally, illustrating my point about adding new technology to an older product.The remainder of this essay will give additional examples of "strap-on technology", finishing up with cases where the advanced layer which was applied involved the Forth programming language (hence the "strap-on Forth" terminology). As added zest for the reader, I will include some remarks on this subject by my friends at the comp.lang.forth newsgroup, who were invited to contribute examples or commentary of their own.
An expert system for a retargetable peephole optimizer
Authors: Warfield J. W. , Bauer H. R.
Published: November 2005

Peephole optimization is the process of improving object code produced by a compiler. The optimizer replaces one or several computer instructions with an instruction which is faster or shorter. Retargetable peephole optimizers work on different machines with minor changes. Previous work has automated the process of developing retargetable peephole optimizers given descriptions of machine instructions. Techniques presented here use an expert system for the task of learning which instructions may be optimized using the descriptions of the computer instructions. The expert system simplifies the task of combining and searching instructions. This project was successful in demonstrating that an expert system may be used for a retargetable peephole optimizer. The expert system may be retargeted to another computer by changing the descriptions of the instructions and the descriptions of the addressing modes. The expert system can also handle pairs of branch instructions and special addressing modes with side effects. The amount of work required for a programmer to build and maintain a retargetable peephole optimizer is reduced using an expert system.
Flow-sensitive type qualifiers
Authors: Foster Jeffrey S. , Terauchi Tachio , Aiken Alex
Published: November 2005

We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively---the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.
Adoption and focus
Authors: Fahndrich Manuel , DeLine Robert
Published: November 2005

A type system with linearity is useful for checking software protocols andresource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an object imposes aliasing restrictions on any data structure that directly or indirectly points to the object. We propose a new type system that reduces these restrictions with the adoption and focus constructs. Adoption safely allows a programmer to alias objects on which she is checking protocols, and focus allows the reverse. A programmer can alias data structures that point to linear objects and use focus for safe access to those objects. We discuss how we implemented these ideas in the Vault programming language.
Deriving specialized program analyses for certifying component-client conformance
Authors: Ramalingam G. , Warshavsky Alex , Field John , Goyal Deepak , Sagiv Mooly
Published: November 2005

We are concerned with the problem of statically
certifying
(verifying) whether the client of a software component conforms to the component's constraints for correct usage. We show how conformance certification can be efficiently carried out in a
staged
fashion for certain classes of
first-order safety
(FOS) specifications, which can express relationship requirements among potentially unbounded collections of runtime objects. In the first stage of the certification process, we systematically derive an abstraction that is used to model the component state during analysis of arbitrary clients. In general, the derived abstraction will utilize first-order
predicates
, rather than the propositions often used by model checkers. In the second stage, the generated abstraction is incorporated into a static analysis engine to produce a
certifier
. In the final stage, the resulting certifier is applied to a client to conservatively determine whether the client violates the component's constraints. Unlike verification approaches that analyze a specification and client code together, our technique can take advantage of computationally-intensive symbolic techniques during the abstraction generation phase, without affecting the performance of client analysis. Using as a running example the
Concurrent Modification Problem
(CMP), which arises when certain classes defined by the Java Collections Framework are misused, we describe several different classes of certifiers with varying time/space/precision tradeoffs. Of particular note are precise, polynomial-time, flow- and context-sensitive certifiers for certain classes of FOS specifications and client programs. Finally, we evaluate a prototype implementation of a certifier for CMP on a variety of test programs. The results of the evaluation show that our approach, though conservative, yields very few "false alarms," with acceptable performance.
Profile-guided code compression
Authors: Debray Saumya , Evans William
Published: November 2005

As computers are increasingly used in contexts where the amount of available memory is limited, it becomes important to devise techniques that reduce the memory footprint of application programs while leaving them in an executable form. This paper describes an approach to applying data compression techniques to reduce the size of infrequently executed portions of a program. The compressed code is decompressed dynamically (via software) if needed, prior to execution. The use of data compression techniques increases the amount of code size reduction that can be achieved; their application to infrequently executed code limits the runtime overhead due to dynamic decompression; and the use of software decompression renders the approach generally applicable, without requiring specialized hardware. The code size reductions obtained depend on the threshold used to determine what code is "infrequently executed" and hence should be compressed: for low thresholds, we see size reductions of 13.7% to 18.8%, on average, for a set of embedded applications, without excessive runtime overhead.
Profile-directed optimization of event-based programs
Authors: Rajagopalan Mohan , Debray Saumya K. , Hiltunen Matti A. , Schlichting Richard D.
Published: November 2005

Events are used as a fundamental abstraction in programs ranging from graphical user interfaces (GUIs) to systems for building customized network protocols. While providing a flexible structuring and execution paradigm, events have the potentially serious drawback of extra execution overhead due to the indirection between modules that raise events and those that handle them. This paper describes an approach to addressing this issue using static optimization techniques. This approach, which exploits the underlying predictability often exhibited by event-based programs, is based on first profiling the program to identify commonly occurring event sequences. A variety of techniques that use the resulting profile information are then applied to the program to reduce the overheads associated with such mechanisms as indirect function calls and argument marshaling. In addition to describing the overall approach, experimental results are given that demonstrate the effectiveness of the techniques. These results are from event-based programs written for X Windows, a system for building GUIs, and Cactus, a system for constructing highly configurable distributed services and network protocols.
Effective sign extension elimination
Authors: Kawahito Motohiro , Komatsu Hideaki , Nakatani Toshio
Published: November 2005

Computer designs are shifting from 32-bit architectures to 64-bit architectures, while most of the programs available today are still designed for 32-bit architectures. Java™, for example, specifies the frequently used int" as a 32-bit data type. If such Java programs are executed on a 64-bit architecture, many 32-bit values must be sign-extended to 64-bit values for integer operations. This causes serious performance overhead. In this paper, we present a fast and effective algorithm for eliminating sign extensions. We implemented this algorithm in the IBM Java Just-in-Time (JIT) compiler for IA-64™. Our experimental results show that our algorithm effectively eliminates the majority of sign extensions. They also show that it significantly improves performance, while it increases JIT compilation time by only 0.11%. We implemented our algorithm for programs in Java, but it can be applied to any language requiring sign extensions.
Denali
Authors: Joshi Rajeev , Nelson Greg , Randall Keith
Published: November 2005

This paper provides a preliminary report on a new research project that aims to construct a code generator that uses an automatic theorem prover to produce very high-quality (in fact, nearly mathematically optimal) machine code for modern architectures. The code generator is not intended for use in an ordinary compiler, but is intended to be used for inner loops and critical subroutines in those cases where peak performance is required, no available compiler generates adequately efficient code, and where current engineering practice is to use hand-coded machine language. The paper describes the design of the superoptimizer, and presents some encouraging preliminary results.
The SLAMproject
Authors: Ball Thomas , Rajamani Sriram K.
Published: November 2005

The goal of the SLAMproject is to check whether or not a program obeys "API usage rules" that specify what it means to be a good client of an API. The SLAMtoolkit statically analyzes a C program to determine whether or not it violates given usage rules. The toolkit has two unique aspects: it does not require the programmer to annotate the source program (invariants are inferred); it minimizes noise (false error messages) through a process known as "counterexample-driven refinement". SLAMexploits and extends results from program analysis, model checking and automated deduction. We have successfully applied the SLAMtoolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.
Role analysis
Authors: Kuncak Viktor , Lam Patrick , Rinard Martin
Published: November 2005

We present a new
role system
in which the type (or
role
) of each object depends on its referencing relationships with other objects, with the role changing as these relationships change. Roles capture important object and data structure properties and provide useful information about how the actions of the program interact with these properties. Our role system enables the programmer to specify the legal aliasing relationships that define the set of roles that objects may play, the roles of procedure parameters and object fields, and the role changes that procedures perform while manipulating objects. We present an interprocedural, compositional, and context-sensitive role analysis algorithm that verifies that a program maintains role constraints.
Analyzing security protocols with secrecy types and logic programs
Authors: Abadi Martín , Blanchet Bruno
Published: November 2005

We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques.
A uniform type structure for secure information flow
Authors: Honda Kohei , Yoshida Nobuko
Published: November 2005

The π-calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/affine typed π-calculus for the analysis and development of type systems of programming languages, focussing on secure information flow analysis. After presenting a basic typed calculus for secrecy, we demonstrate its usage by a sound embedding of the dependency core calculus (DCC) and by the development of a novel type discipline for imperative programs which extends both a secure multi-threaded imperative language by Smith and Volpano and (a call-by-value version of) DCC. In each case, the embedding gives a simple proof of noninterference.
Towards automatic construction of staged compilers
Authors: Philipose Matthai , Chambers Craig , Eggers Susan J.
Published: November 2005

Some compilation systems, such as offline partial evaluators and selective dynamic compilation systems, support staged optimizations. A staged optimization is one where a logically single optimization is broken up into stages, with the early stage(s) performing preplanning set-up work, given any available partial knowledge about the program to be compiled, and the final stage completing the optimization. The final stage can be much faster than the original optimization by having much of its work performed by the early stages. A key limitation of current staged optimizers is that they are written by hand, sometimes in an
ad hoc
manner. We have developed a framework called the
Staged Compilation Framework
(SCF) for systematically and automatically converting single-stage optimizations into staged versions. The framework is based on a combination of aggressive partial evaluation and dead-assignment elimination. We have implemented SCF in Standard ML. A preliminary evaluation shows that SCF can speed up classical optimization of some commonly used C functions by up to 12× (and typically between 4.5× and 5.5×).
Representation independence, confinement and access control [extended abstract]
Authors: Banerjee Anindya , Naumann David A.
Published: November 2005

Denotational semantics is given for a Java-like language with pointers, subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods, and privilege-based access control. Representation independence (relational parametricity) is proved, using a semantic notion of confinement similar to ones for which static disciplines have been recently proposed.
Systematic design of program transformation frameworks by abstract interpretation
Authors: Cousot Patrick , Cousot Radhia
Published: November 2005

We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.
Composing dataflow analyses and transformations
Authors: Lerner Sorin , Grove David , Chambers Craig
Published: November 2005

Dataflow analyses can have mutually beneficial interactions. Previous efforts to exploit these interactions have either (1) iteratively performed each individual analysis until no further improvements are discovered or (2) developed "super-analyses" that manually combine conceptually separate analyses. We have devised a new approach that allows analyses to be defined independently while still enabling them to be combined automatically and profitably. Our approach avoids the loss of precision associated with iterating individual analyses and the implementation difficulties of manually writing a super-analysis. The key to our approach is a novel method of implicit communication between the individual components of a super-analysis based on graph transformations. In this paper, we precisely define our approach; we demonstrate that it is sound and it terminates; finally we give experimental results showing that in practice (1) our framework produces results at least as precise as iterating the individual analyses while compiling at least 5 times faster, and (2) our framework achieves the same precision as a manually written super-analysis while incurring a compile-time overhead of less than 20%.
Profile guided selection of ARM and thumb instructions
Authors: Krishnaswamy Arvind , Gupta Rajiv
Published: November 2005

The ARM processor core is a leading processor design for the embedded domain. In the embedded domain, both memory and energy are important concerns. For this reason the 32 bit ARM processor also supports the 16 bit Thumb instruction set. For a given program, typically the Thumb code is smaller than the ARM code. Therefore by using Thumb code the I-cache activity, and hence the energy consumed by the I-cache, can be reduced. However, the limitations of the Thumb instruction set, in comparison to the ARM instruction set, can often lead to generation of poorer quality code. Thus, while Thumb code may be smaller than ARM code, it may perform poorly and thus may not lead to overall energy savings.