bluuebunny/crossref_metadata_2025 huggingface dataset:
Functional programming in C++
Authors: McNamara Brian , Smaragdakis Yannis
Published: November 2005

This paper describes FC++: a rich library supporting functional programming in C++. Prior approaches to encoding higher order functions in C++ have suffered with respect to polymorphic functions from either lack of expressiveness or high complexity. In contrast, FC++ offers full and concise support for higher-order polymorphic functions through a novel use of C++ type inference.Another new element in FC++ is that it implements a subtype polymorphism policy for functions, in addition to the more common parametric polymorphism facilities. Subtype polymorphism is common in object oriented languages and ensures that functions in FC++ fit well within the C++ object model.Apart from these conceptual differences, FC++ is also an improvement in technical terms over previous efforts in the literature. Our function objects are reference-counted and can be aliased without needing to be copied, resulting in an efficient implementation. The reference-counting mechanism is also exported to the user as a general-purpose replacement of native C++ pointers. Finally, we supply a number of useful functional operators (a large part of the Haskell Standard Prelude) to facilitate programming with FC++. The end result is a library that is usable and efficient, while requiring no extensions to the base C++ language.
Advanced module systems (invited talk)
Authors: Harper Robert , Pierce Benjamin C.
Published: November 2005

The past three decades have seen a plethora of language features for large-scale software composition. Some of these are fairly simple, others quite sophisticated. Each embodies an implicit claim that its particular combination of features is both necessary and sufficient for some problem domain. But there have been few attempts to
compare
module systems, or to explain the practical and theoretical issues that motivate the choices they embody. This can make it difficult to evaluate which features are really needed for a given setting, and which may be overkill.
Breadth-first numbering
Authors: Okasaki Chris
Published: November 2005

Every programmer has blind spots. Breadth-first numbering is an interesting toy problem that exposes a blind spot common to many---perhaps most---functional programmers.
An operational semantics for parallel lazy evaluation
Authors: Baker-Finch Clem , King David J. , Trinder Phil
Published: November 2005

We present an operational semantics for
parallel lazy evaluation
that accurately models the parallel behaviour of the non-strict parallel functional language GpH. Parallelism is modelled synchronously, that is, single reductions are carried out separately then combined before proceeding to the next set of reductions. Consequently the semantics has two levels, with transition rules for individual threads at one level and combining rules at the other. Each parallel thread is modelled by a binding labelled with an indication of its activity status. To the best of our knowledge this is the first semantics that models such thread states. A set of labelled bindings corresponds to a heap and is used to model sharing.The semantics is set at a higher level of abstraction than an abstract machine and is therefore more manageable for proofs about programs rather than implementations. At the same time, it is sufficiently low level to allow us to reason about programs in terms of
parallelism
(i.e. the number of processors used) as well as
work
and
run-time
with different numbers of processors.The framework used by the semantics is sufficiently flexible and general that it can easily be adapted to express other evaluation models such as sequential call-by-need, speculative evaluation, non-deterministic choice and others.
Deriving backtracking monad transformers
Authors: Hinze Ralf
Published: November 2005

In a paper about pretty printing J. Hughes introduced two fundamental techniques for deriving programs from their specification, where a specification consists of a signature and properties that the operations of the signature are required to satisfy. Briefly, the first technique, the term implementation, represents the operations by terms and works by defining a mapping from operations to observations --- this mapping can be seen as defining a simple interpreter. The second, the context-passing implementation, represents operations as functions from their calling context to observations. We apply both techniques to derive a backtracking monad transformer that adds backtracking to an arbitrary monad. In addition to the usual backtracking operations --- failure and nondeterministic choice --- the prolog cut and an operation for delimiting the effect of a cut are supported.
Syntactic accidents in program analysis
Authors: Damian Daniel , Danvy Olivier
Published: November 2005

We show that a non-duplicating CPS transformation has no effect on control-flow analysis and that it has a positive effect on binding-time analysis: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, and a monovariant binding-time analysis yields more precise results on a CPS program than on its direct-style counterpart. Our proof technique amounts to constructing the continuation-passing style (CPS) counterpart of flow information and of binding times.Our results confirm a folklore theorem about binding-time analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that this benefit holds even if contexts or continuations are not duplicated.The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.
Recursive subtyping revealed
Authors: Gapeyev Vladimir , Levin Michael Y. , Pierce Benjamin C.
Published: November 2005

Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler declarative specifications is not widely understood, due in part to the difficulty of the available introductions to the area. This tutorial paper offers an "end-to-end" introduction to recursive types and subtyping algorithms, from basic theory to efficient implementation, set in the unifying mathematical framework of coinduction.
The duality of computation
Authors: Curien Pierre-Louis , Herbelin Hugo
Published: November 2005

We present the μ -calculus, a syntax for λ-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus
LK
, a key classical logical system in proof theory. Under the Curry-Howard correspondence between proofs and programs, we can see
LK
, or more precisely a formulation called

LK
μ

, as a syntax-directed system of simple types for μ -calculus. For μ -calculus, choosing a call-by-name or call-by-value discipline for reduction amounts to choosing one of the two possible symmetric orientations of a critical pair. Our analysis leads us to revisit the question of what is a natural syntax for call-by-value functional computation. We define a translation of λμ-calculus into μ -calculus and two dual translations back to λ-calculus, and we recover known CPS translations by composing these translations.
Understanding memory allocation of scheme programs
Authors: Serrano Manuel , Boehm Hans-J.
Published: November 2005

Memory is the performance bottleneck of modern architectures. Keeping memory consumption as low as possible enables fast and unobtrusive applications. But it is not easy to estimate the memory use of programs implemented in functional languages, due to both the complex translations of some high level constructs, and the use of automatic memory managers.To help understand memory allocation behavior of Scheme programs, we have designed two complementary tools. The first one reports on frequency of allocation, heap configurations and on memory reclamation. The second tracks down memory leaks
1
. We have applied these tools to our Scheme compiler, the largest Scheme program we have been developing. This has allowed us to drastically reduce the amount of memory consumed during its bootstrap process, without requiring much development time.Development tools will be neglected unless they are both conveniently accessible and easy to use. In order to avoid this pitfall, we have carefully designed the user interface of these two tools. Their integration into a real programming environment for Scheme is detailed in the paper.
Practicing JUDO
Authors: Cierniak Michał , Lueh Guei-Yuan , Stichnoth James M.
Published: November 2005

A high-performance implementation of a Java Virtual Machine (JVM) consists of efficient implementation of Just-In-Time (JIT) compilation, exception handling, synchronization mechanism, and garbage collection (GC). These components are tightly coupled to achieve high performance. In this paper, we present some
static
and
dynamic
techniques implemented in the JIT compilation and exception handling of the Microprocessor Research Lab Virtual Machine (MRL VM), i.e., lazy exceptions, lazy GC mapping, dynamic patching, and bounds checking elimination. Our experiments used IA-32 as the hardware platform, but the optimizations can be generalized to other architectures.
Unification-based pointer analysis with directional assignments
Authors: Das Manuvir
Published: November 2005

This paper describes a new algorithm for flow and context insensitive pointer analysis of C programs. Our studies show that the most common use of pointers in C programs is in passing the addresses of composite objects or updateable values as arguments to procedures. Therefore, we have designed a low-cost algorithm that handles this common case accurately. In terms of both precision and running time, this algorithm lies between Steensgaard's algorithm, which treats assignments bi-directionally using unification, and Andersen's algorithm, which treats assignments directionally using subtyping. Our “one level flow” algorithm uses a restricted form of subtyping to avoid unification of symbols at the top levels of pointer chains in the points-to graph, while using unification elsewhere in the graph. The method scales easily to large programs. For instance, we are able to analyze a 1.4 MLOC (million lines of code) program in two minutes, using less than 200MB of memory. At the same time, the precision of our algorithm is very close to that of Andersen's algorithm. On all of the integer benchmark programs from SPEC95, the one level flow algorithm and Andersen's algorithm produce either identical or essentially identical points-to information. Therefore, we claim that our algorithm provides a method for obtaining precise flow-insensitive points-to information for large C programs.
Off-line variable substitution for scaling points-to analysis
Authors: Rountev Atanas , Chandra Satish
Published: November 2005

Most compiler optimizations and software productivity tools rely on
information about the effects of pointer dereferences in a program.
The purpose of points-to analysis is to compute this information
safely, and as accurately as is practical. Unfortunately, accurate
points-to information is difficult to obtain for large programs,
because the time and space requirements of the analysis become
prohibitive.

We consider the problem of scaling flow- and context-insensitive
points-to analysis to large programs, perhaps containing hundreds of
thousands of lines of code. Our approach is based on a
variable substitution
transformation, which is performed off-line, i.e.,
before a standard points-to analysis is performed. The general idea of
variable substitution is that a set of variables in a program can be replaced by a single representative variable, thereby reducing the input size of the problem. Our main contribution is a linear-time algorithm which finds a particular variable substitution that maintains the precision of the standard analysis, and is also very effective in reducing the size of the problem.

We report our experience in performing points-to analysis on large
C programs, including some industrial-sized ones. Experiments show that
our algorithm can reduce the cost of Andersen's points-to analysis substantially: on average, it reduced the running time by 53% and the memory cost by 59%, relative to an efficient baseline implementation of the analysis.
Modular interprocedural pointer analysis using access paths
Authors: Cheng Ben-Chung , Hwu Wen-Mei W.
Published: November 2005

In this paper we present a modular interprocedural pointer analysis
algorithm based on access-paths for C programs. We argue that access paths can reduce the overhead of representing context-sensitive transfer functions and effectively distinguish non-recursive heap objects. And when the modular analysis paradigm is used together with other techniques to handle type casts and function pointers, we are able to handle significant programs like those in the SPECcint92 and SPECcint95 suites. We have implemented the algorithm and tested it on a Pentium II 450 PC running Linux. The observed resource consumption and performance improvement are very encouraging.
Optimal instruction scheduling using integer programming
Authors: Wilken Kent , Liu Jack , Heffernan Mark
Published: November 2005

This paper presents a new approach to local instruction scheduling based on integer programming that produces optimal instruction schedules in a reasonable time, even for very large basic blocks. The new approach first uses a set of graph transformations to simplify the data-dependency graph while preserving the optimality of the final schedule. The simplified graph results in a simplified integer program which can be solved much faster. A new integer-programming formulation is then applied to the simplified graph. Various techniques are used to simplify the formulation, resulting in fewer integer-program variables, fewer integer-program constraints and fewer terms in some of the remaining constraints, thus reducing integer-program solution time. The new formulation also uses certain adaptively added constraints (cuts) to reduce solution time. The proposed optimal instruction scheduler is built within the Gnu Compiler Collection (GCC) and is evaluated experimentally using the SPEC95 floating point benchmarks. Although optimal scheduling for the target processor is considered intractable, all of the benchmarks' basic blocks are optimally scheduled, including blocks with up to 1000 instructions, while total compile time increases by only 14%.
A framework for interprocedural optimization in the presence of dynamic class loading
Authors: Sreedhar Vugranam C. , Burke Michael , Choi Jong-Deok
Published: November 2005

Dynamic class loading during program execution in the Java Programming Language is an impediment for generating code that is as efficient as code generated using static whole-program analysis and optimization. Whole-program analysis and optimization is possible for languages, such as C++, that do not allow new classes and/or methods to be loaded during program execution. One solution for performing whole-program analysis and
avoiding incorrect execution after a new class is loaded is to invalidate and recompile affected methods. Runtime invalidation and recompilation mechanisms can be expensive in both space and time, and, therefore, generally restrict optimization.

To address these drawbacks, we propose a new framework, called the
extant analysis framework
, for interprocedural optimization of programs that support dynamic class (or method)loading. Given a set of classes comprising the
closed world
, we perform an offline static analysis
which partitions references into two categories:(1)
unconditionally extant
references which point only to objects whose runtime type is guaranteed to be in the closed world; and (2)
conditionally extant
references which point to objects whose runtime type is not guaranteed to be in the closed world. Optimizations solely dependent on the first categorycan be statically performed, and are guaranteed to be correct even with any future class/method loading. Optimizations dependent on the second category are guarded by dynamic tests, called
extant safety tests
, for correct execution behavior.We describe the properties for extant safety tests, and provide algorithms for their generation and placement.
Type-based race detection for Java
Authors: Flanagan Cormac , Freund Stephen N.
Published: November 2005

This paper presents a static race detection analysis for multithreaded Java programs. Our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. These patterns include classes with internal synchronization, classes thatrequire client-side synchronization, and thread-local classes. Experience checking over 40,000 lines of Java code with the type system demonstrates that it is an effective approach for eliminating races conditions. On large examples, fewer than 20 additional type annotations per 1000 lines of code were required by the type checker, and we found a number of races in the standard Java libraries and other test programs.
Machine-independent virtual memory management for paged uniprocessor and multiprocessor architectures
Authors: Rashid Richard , Tevanian Avadis , Young Michael , Golub David , Baron Robert , Black David , Bolosky William , Chew Jonathan
Published: November 2005

This paper describes the design and implementation of virtual memory management within the CMU Mach Operating System and the experiences gained by the Mach kernel group in porting that system to a variety of architectures. As of this writing, Mach runs on more than half a dozen uniprocessors and multiprocessors including the VAX family of uniprocessors and multiprocessors, the IBM RT PC, the SUN 3, the Encore MultiMax, the Sequent Balance 21000 and several experimental computers. Although these systems vary considerably in the kind of hardware support for memory management they provide, the machine-dependent portion of Mach virtual memory consists of a single code module and its related header file. This separation of software memory management from hardware support has been accomplished without sacrificing system performance. In addition to improving portability, it makes possible a relatively unbiased examination of the pros and cons of various hardware memory management schemes, especially as they apply to the support of multiprocessors.
Coherency for multiprocessor virtual address caches
Authors: Goodman James R.
Published: November 2005

A multiprocessor cache memory system is described that supplies data to the processor based on virtual addresses, but maintains consistency in the main memory, both across caches and across virtual address spaces. Pages in the same or different address spaces may be mapped to share a single physical page. The same hardware is used for maintaining consistency both among caches and among virtual addresses. Three different notions of a cache "block" are defined: (1) the unit for transferring data to/from main storage, (2) the unit over which tag information is maintained, and (3) the unit over which consistency is maintained. The relation among these block sizes is explored, and it is shown that they can be optimized independently. It is shown that the use of large address blocks results in low overhead for the virtual address cache.
A study of scalar compilation techniques for pipelined supercomputers
Authors: Weiss Shlomo , Smith James E.
Published: November 2005

This paper studies two compilation techniques for enhancing scalar performance in high-speed scientific processors: software pipelining and loop unrolling. We study the impact of the architecture (size of the register file) and of the hardware (size of instruction buffer) on the efficiency of loop unrolling. We also develop a methodology for classifying software pipelining techniques. For loop unrolling, a straightforward scheduling algorithm is shown to produce near-optimal results when not inhibited by recurrences or memory hazards. Software pipelining requires less hardware but also achieves less speedup. Finally, we show that the performance produced with a modified CRAY-1S scalar architecture and a code scheduler utilizing loop unrolling is comparable to the performance achieved by the CRAY-1S with a vector unit and the CFT vectorizing compiler.
How many addressing modes are enough?
Authors: Chow F. , Correll S. , Himelstein M. , Killian E. , Weber L.
Published: November 2005

Programs naturally require a variety of memory-addressing modes. It isn't necessary to provide them in hardware, however, if a compiler can synthesize them from a few primitive modes. This not only simplifies the hardware, but also permits the compiler to use its understanding of the program to economize on the modes which it uses. We present some compilation techniques that allow the compiler to deal effectively with a single addressing mode in a target RISC processor. We also give measurements to show the benefits of such techniques, and to support our assertion that a single addressing mode is adequate for a general purpose processor, provided that mode incorporates both a pointer and an offset.
RISCs vs. CISCs for Prolog: a case study
Authors: Borriello Gaetano , Cherenson Andrew R. , Danzig Peter B. , Nelson Michael N.
Published: November 2005

This paper compares the performance of executing compiled Prolog code on two different architectures under development at U. C. Berkeley. The first is the PLM, a special-purpose CISC architecture intended as a coprocessor for a host machine. The second is SPUR, a general-purpose RISC architecture that supports tagged data. Fourteen standard benchmark programs were run on both the PLM and SPUR simulators. The compiled code for SPUR was obtained by simple macro-expansion of PLM code generated by the PLM Prolog compiler. The two implementations are compared with regard to static and dynamic program size, execution speed, and memory system performance. On average, the macrocoded SPUR implementation has a static code size 14 times larger than the PLM, executes 16 times more instructions, yet requires only 2.3 times the number of machine cycles (or has the performance of 0.43 PLMs). When memory system performance is taken into account, SPUR is equivalent to 0.29 PLMs. Optimizations of the macro-expanded code and minor architectural changes to SPUR would increase this ratio to 0.53, or 0.60 for the largest benchmarks. Thus a tagged RISC architecture can execute Prolog at least half as fast as a special-purpose CISC architecture for Prolog.
Firefly: a multiprocessor workstation
Authors: Thacker Charles P. , Stewart Lawrence C.
Published: November 2005

Firefly is a shared-memory multiprocessor workstation that contains from one to seven MicroVAX 78032 processors, each with a floating point unit and a sixteen kilobyte cache. The caches are coherent, so that all processors see a consistent view of main memory. A system may contain from four to sixteen megabytes of storage. Input-output is done via a standard DEC QBus. Input-output devices are an Ethernet controller, fixed disks, and a monochrome 1024 x 768 display with keyboard and mouse. Optional hardware includes a high resolution color display and a controller for high capacity disks. Figure 1 is a system block diagram.The Firefly runs a software system that emulates the Ultrix system call interface. It also supports medium- and coarse-grained multiprocessing through multiple threads of control in a single address space. Communications are implemented uniformly through the use of remote procedure calls.This paper describes the goals, architecture, implementation and performance analysis of the Firefly. It then presents some measurements of hardware performance, and discusses the degree to which SRC has been successful in producing software to take advantage of multiprocessing.
Parallel computers for graphics applications
Authors: Levinthal Adam , Hanrahan Pat , Paquette Mike , Lawson Jim
Published: November 2005

Specialized computer architectures can provide better price/performance for executing image processing and graphics applications than general purpose designs. Two processors are presented that use parallel SIMD data paths to support common graphics data structures as primitive operands in arithmetic expressions. A variant of the C language has been implemented to allow high level language coding of user applications on these processors. High level programming support is designed into the processor architecture that implements parallel object data typing and parallel conditional evaluation in hardware.
The ZS-1 central processor
Authors: Smith J. E. , Dermer G. E. , Vanderwarn B. D. , Klinger S. D. , Rozewski C. M. , Fowler D. L. , Scidmore K. R. , Laudon J. P.
Published: November 2005

The Astronautics ZS-1 is a high speed, 64-bit computer system designed for scientific and engineering applications. The ZS-1 central processor uses a decoupled architecture, which splits instructions into two streams---one for fixed point/memory address computation and the other for floating point operations. The two instruction streams are then processed in parallel. Pipelining is also used extensively throughout the ZS-1.This paper describes the architecture and implementation of the ZS-1 central processor, beginning with some of the basic design objectives. Descriptions of the instruction set, pipeline structure, and virtual memory implementation demonstrate the methods used to satisfy the objectives. High performance is achieved through a combination of static (compile-time) instruction scheduling and dynamic (run-time) scheduling. Both types of scheduling are illustrated with examples.
A region-based memory manager for prolog
Authors: Makholm Henning
Published: November 2005

We extend Tofte and Talpin's region-based model for memory management to support backtracking and cuts, which makes it suitable for use with Prolog and other logic programming languages. We describe how the extended model can be implemented and report on the performance of a prototype implementation. The prototype implementation performs well when compared to a garbage-collecting Prolog implementation using comparable technology for non-memory-management issues.
Compact garbage collection tables
Authors: Tarditi David
Published: November 2005

Garbage collection tables for finding pointers on the stack can be represented in 20-25% of the space previously reported. Live pointer information is often the same at many call sites because there are few pointers live across most call sites. This allows live pointer information to be represented compactly by a small index into a table of descriptions of pointer locations. The mapping from program counter values to those small indexes can be represented compactly using several techniques. The techniques a assign numbers to call sites and use those numbers to index an array of small indexes. One technique is to represent an array of return addresses by using a two-level table with 16-bit off-sets. Another technique is to use a sparse array of return addresses and interpolate the exact number via disassembly of the executable code.
Dynamic adaptive pre-tenuring
Authors: Harris Timothy L.
Published: November 2005

In a generational garbage collector, a
pre-tenured
object is one that is allocated directly in the old generation. Pre-tenuring long-lived objects reduces the number of times that they are scanned or copied during garbage collection. Previous work has investigated pre-tenuring based on off-line analysis of execution traces. This paper builds on that work by presenting a
dynamic
technique in which the decision to pre-tenure a particular kind of object is taken at run-time. This allows decisions to depend on the inputs of a particular application run and also allows decisions to be changed as the application enters different phases. An implementation is presented for the Research VM Java Virtual Machine.
Programming language methods in computer security
Authors: Mitchell John C.
Published: November 2005

This invited talk will give a personal view of the field of computer security and summarize some ways that methods from the study of programming language principles can be applied to problems in computer security. Some background information is provided here in this short document.
The size-change principle for program termination
Authors: Lee Chin Soon , Jones Neil D. , Ben-Amram Amir M.
Published: November 2005

The "size-change termination" principle for a first-order functional language with well-founded data is: a program terminates on all inputs if
every infinite call sequence
(following program control flow) would cause an infinite descent in some data values.Size-change analysis is based only on local approximations to parameter size changes derivable from program syntax. The set of infinite call sequences that follow program flow and can be recognized as causing infinite descent is an
ω
-regular set, representable by a Büchi automaton. Algorithms for such automata can be used to decide size-change termination. We also give a direct algorithm operating on "size-change graphs" (without the passage to automata).Compared to other results in the literature, termination analysis based on the size-change principle is surprisingly simple and general: lexical orders (also called lexicographic orders), indirect function calls and permuted arguments (descent that is not
in-situ
) are all handled
automatically and without special treatment
, with no need for manually supplied argument orders, or theorem-proving methods not certain to terminate at analysis time.We establish the problem's
intrinsic complexity
. This turns out to be surprisingly high, complete for PSPACE, in spite of the simplicity of the principle. PSPACE hardness is proved by a reduction from Boolean program termination. An ineresting consequence: the same hardness result applies to many other analyses found in the termination and quasitermination literature.
Oracle-based checking of untrusted software
Authors: Necula George C. , Rahul S. P.
Published: November 2005

We present a variant of Proof-Carrying Code (PCC) in which the trusted inference rules are represented as a higherorder logic program, the proof checker is replaced by a nondeterministic higher-order logic interpreter and the proof by an oracle implemented as a stream of bits that resolve the nondeterministic interpretation choices. In this setting, Proof-Carrying Code allows the receiver of the code the luxury of using nondeterminism in constructing a simple yet powerful checking procedure.This oracle-based variant of PCC is able to adapt quite naturally to situations when the property being checked is simple or there is a fairly directed search procedure for it. As an example, we demonstrate that if PCC is used to verify type safety of assembly language programs compiled from Java source programs, the oracles that are needed are on the average just 12% of the size of the code, which represents an improvement of a factor of 30 over previous syntactic representations of PCC proofs.
Type-preserving garbage collectors
Authors: Wang Daniel C. , Appel Andrew W.
Published: November 2005

By combining existing type systems with standard type-based compilation techniques, we describe how to write strongly typed programs that include a function that acts as a t racing garbage collector for the program. Since the garbage collector is an explicit function, we do not need to provide a t rusted garbage collector as a runtime service to manage memory.Since our language is strongly typed, the standard type soundness guarantee "Well typed programs do not go wrong" is extended to include the collector. Our type safety guarantee is non-trivial since not only does it guarantee the type safety of the garbage collector, but it guarantees that the collector preservers the type safety of the program being garbage collected. We describe the technique in detail and report performance measurements for a few microbench-marks as well as sketch the proofs of type soundness for our system.
Secure safe ambients
Authors: Bugliesi Michele , Castagna Giuseppe
Published: November 2005

Secure Safe Ambients
(SSA) are a typed variant of
Safe Ambients
[9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture
both
explicit
and
implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as
Trojan Horses
and other combinations of malicious agents.We study the type system of SSA, define algorithms for type checking and type reconstruction, define powerful languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.
Combining subsumption and binary methods
Authors: Vouillon Jérôme
Published: November 2005

We presen t an object-oriented calculus whic hallows arbitrary hiding of methods in protot ypes, even in the presence of binary methods and friend functions. This combination of features permits complete control of the in terface a class exposes to the remainder of a program (which is of key importance for program readability, security and ease of maintenance), while still allowing complex in teractions with other classes belonging to the same module or softw are component.This result is made possible by the use of views. A view is a name that specifies an in terface to an object. A set of views is attached to each object and a method can be invoked either directly or via a view of the object.
Extensionality and intensionality of the ambient logics
Authors: Sangiorgi Davide
Published: November 2005

The
ambient logic
has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. To understand the extensionality and the intensionality of the logic, the equivalence on MA processes induced by the logic (=

L

) iscompared with the standard MA behavioural equivalence and with structural congruence (an intensional equivalence, used as an auxiliary relation in thedefinition of satisfaction of the logic). The main contributions include a co-inductive characterisation of <=

L

as a form of labelled bisimilarity, and axiomatisations of <=

L

on the synchronous and asynchronous (finite) calculus. The study shows that, surprisingly, the logic allows us to observe the internal structure of the processes at a very finegrained detail, much in the same way as structural congruence does. A spin-off of the study is a better understanding of behavioural equivalence in Ambient-like calculi. For instance, behavioural equivalence is shown to be insensitive to
stuttering
phenomena originated by processes that may repeatedly enter and exit an ambient.
BI as an assertion language for mutable data structures
Authors: Ishtiaq Samin S. , O'Hearn Peter W.
Published: November 2005

Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O'Hearnand Pym. We begin by giving a model in which the law of the excluded middleholds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI's spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triplesthat allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.
Design and implementation of generics for the .NET Common language runtime
Authors: Kennedy Andrew , Syme Don
Published: November 2005

The Microsoft.NET Common Language Runtime provides a shared type system, intermediate language and dynamic execution environment for the implementation and inter-operation of multiple source languages. In this paper we extend it with direct support for parametric polymorphism (also known as generics), describing the design through examples written in an extended version of the C# programming language, and explaining aspects of implementation by reference to a prototype extension to the runtime.

Our design is very expressive, supporting parameterized types, polymorphic static, instance and virtual methods, “F-bounded” type parameters, instantiation at pointer and value types, polymorphic recursion, and exact run-time types. The implementation takes advantage of the dynamic nature of the runtime, performing just-in-time type specialization, representation-based code sharing and novel techniques for efficient creation and use of run-time types.

Early performance results are encouraging and suggest that programmers will not need to pay an overhead for using generics, achieving performance almost matching hand-specialized code.
Demand-driven pointer analysis
Authors: Heintze Nevin , Tardieu Olivier
Published: November 2005

Known algorithms for pointer analysis are “global” in the sense that they perform an exhaustive analysis of a program or program component. In this paper we introduce a demand-driven approach for pointer analysis. Specifically, we describe a
demand-driven
flow-insensitive, subset-based, con text-insensitive points-to analysis. Given a list of pointer variables (a query), our analysis performs just enough computation to determine the points-to sets for these query variables. Using deductive reachability formulations of both the exhaustive and the demand-driven analyses, we prove that our algorithm is correct. We also show that our analysis is optimal in the sense that it does not do more work than necessary. We illustrate the feasibility and efficiency of our analysis with an implementation of demand-driven points-to analysis for computing the call-graphs of C programs with function pointers. The performance of our system varies substantially across benchmarks - the main factor is how much of the points-to graph must be computed to determine the call-graph. For some benchmarks, only a small part of the points-to graph is needed (e.g
pouray emacs
and
gcc
), and here we see more than a 10x speedup. For other benchmarks (e.g.
burlap
and
gimp
), we need to compute most (> 95%) of the points-to graph, and here the demand-driven algorithm is considerably slower, because using the demand-driven algorithm is a slow method of computing the full points-to graph.
On the importance of points-to analysis and other memory disambiguation methods for C programs
Authors: Ghiya Rakesh , Lavery Daniel , Sehr David
Published: November 2005

In this paper, we evaluate the benefits achievable from pointer analysis and other memory disambiguation techniques for C/C++ programs, using the framework of the production compiler for the Intel® Itanium™ processor. Most of the prior work on memory disambiguation has primarily focused on pointer analysis, and either presents only static estimates of the accuracy of the analysis (such as average points-to set size), or provides performance data in the context of certain individual optimizations. In contrast, our study is based on a complete memory disambiguation framework that uses a whole set of techniques including pointer analysis. Further, it presents how various compiler analyses and optimizations interact with the memory disambiguator, evaluates how much they benefit from disambiguation, and measures the eventual impact on the performance of the program. The paper also analyzes the types of disambiguation queries that are typically received by the disambiguator, which disambiguation techniques prove most effective in resolving them, and what type of queries prove difficult to be resolved. The study is based on empirical data collected for the SPEC CINT2000 C/C++ programs, running on the Itanium processor.
Language support for regions
Authors: Gay David , Aiken Alex
Published: November 2005

Region-based memory management systems structure memory by grouping objects in regions under program control. Memory is reclaimed by deleting regions, freeing all objects stored therein. Our compiler for C with regions, RC, prevents unsafe region deletions by keeping a count of references to each region. Using type annotations that make the structure of a program's regions more explicit, we reduce the overhead of reference counting from a maximum of 27% to a maximum of 11% on a suite of realistic benchmarks. We generalise these annotations in a region type system whose main novelty is the use of existentially quantified abstract regions to represent pointers to objects whose region is partially or totally unknown. A distribution of RC is available at http://www.cs.berkeley.edu/~dgay/rc.tar.gz.
A parallel, real-time garbage collector
Authors: Cheng Perry , Blelloch Guy E.
Published: November 2005

We describe a parallel, real-time garbage collector and present experimental results that demonstrate good scalability and good real-time bounds. The collector is designed for shared-memory multiprocessors and is based on an earlier collector algorithm [2], which provided fixed bounds on the time any thread must pause for collection. However, since our earlier algorithm was designed for simple analysis, it had some impractical features. This paper presents the extensions necessary for a practical implementation: reducing excessive interleaving, handling stacks and global variables, reducing double allocation, and special treatment of large and small objects. An implementation based on the modified algorithm is evaluated on a set of 15 SML benchmarks on a Sun Enterprise 10000, a 64-way UltraSparc-II multiprocessor. To the best of our knowledge, this is the first implementation of a parallel, real-time garbage collector.

The average collector speedup is 7.5 at 8 processors and 17.7 at 32 processors. Maximum pause times range from 3 ms to 5 ms. In contrast, a non-incremental collector (whether generational or not) has maximum pause times from 10 ms to 650 ms. Compared to a non-parallel, stop-copy collector, parallelism has a 39% overhead, while real-time behavior adds an additional 12% overhead. Since the collector takes about 15% of total execution time, these features have an overall time costs of 6% and 2%.
Using annotations to reduce dynamic optimization time
Authors: Krintz Chandra , Calder Brad
Published: November 2005

Dynamic compilation and optimization are widely used in heterogenous computing environments, in which an intermediate form of the code is compiled to native code during execution. An important trade off exists between the amount of time spent dynamically optimizing the program and the running time of the program. The time to perform dynamic optimizations can cause significant delays during execution and also prohibit performance gains that result from more complex optimization.

In this research, we present an annotation framework that substantially reduces compilation overhead of Java programs. Annotations consist of analysis information collected off-line and are incorporated into Java programs. The annotations are then used by dynamic compilers to guide optimization. The annotations we present reduce compilation overhead incurred at all stages of compilation and optimization as well as enable complex optimizations to be performed dynamically. On average, our annotation optimizations reduce optimized compilation overhead by 78% and enable speedups of 7% on average for the programs examined.
Timestamped whole program path representation and its applications
Authors: Zhang Youtao , Gupta Rajiv
Published: November 2005

A
whole program path
(WPP) is a complete control flow trace of a program's execution. Recently Larus [18] showed that although WPP is expected to be very large (100's of MBytes), it can be greatly compressed (to 10's of MBytes) and therefore saved for future analysis. While the compression algorithm proposed by Larus is highly effective, the compression is accompanied with a loss in the ease with which subsets of information can be accessed. In particular, path traces pertaining to a particular function cannot generally be obtained without examining the entire compressed WPP representation. To solve this problem we advocate the application of
compaction
techniques aimed at providing easy access to path traces on a per function basis.

We present a WPP compaction algorithm in which the WPP is broken in to
path traces
corresponding to individual function calls. All of the path traces for a given function are stored together as a block. Ability to construct the complete WPP from individual path traces is preserved by maintaining a
dynamic call graph
. The compaction is achieved by eliminating
redundant path traces
that result from different calls to a function and by replacing a sequence of static basic block ids that correspond to a
dynamic basic block
by a single id. We transform a compacted WPP representation into a
timestamped
WPP (TWPP) representation in which the path traces are organized from the perspective of dynamic basic blocks. TWPP representation also offers additional opportunities for compaction.

Experiments show that our algorithm compacts the WPPs by factors ranging from 7 to 64. At the same time information is organized in a highly accessible form which speeds up the responses to queries requesting the path traces of a given function by over 3 orders of magnitude.
ESP
Authors: Kumar Sanjeev , Mandelbaum Yitzhak , Yu Xiang , Li Kai
Published: November 2005

This paper presents the design and implementation of Event-driven State-machines Programming (ESP)—a language for programmable devices. In traditional languages, like C, using event-driven state-machine forces a tradeoff that requires giving up ease of development and reliability to achieve high performance. ESP is designed to provide all of these three properties simultaneously.

ESP provides a comprehensive set of features to support development of compact and modular programs. The ESP compiler compiles the programs into two targets—a C file that can be used to generate efficient firmware for the device; and a specification that can be used by a verifier like SPlN to extensively test the firmware.

As a case study, we reimplemented VMMC firmware that runs on Myrinet network interface cards using ESP. We found that ESP simplifies the task of programming with event-driven state machines. It required an order of magnitude fewer lines of code than the previous implementation. We also found that model-checking verifiers like SPIN can be used to effectively debug the firmware. Finally, our measurements indicate that the performance overhead of using ESP is relatively small.
Some comments on “the priority-based coloring approach to register allocation”
Authors: Sorkin Arthur
Published: November 2005

There is a problem with the definition of constrained live range and unconstrained live range in Chow and Hennessy's paper on priority-based register allocation that unnecessarily pessimizes the performance of the register allocator. Some corrections to the algorithm are suggested. Some problems with Chow and Hennessy's analysis of caller-save vs. callee-save are also discussed.