bluuebunny/crossref_metadata_2025 huggingface dataset:
A type based sharing analysis for update avoidance and optimisation
Authors: Gustavsson Jörgen
Published: November 2005

Sharing of evaluation is crucial for the efficiency of lazy functional languages, but unfortunately the machinery to implement it carries an inherent overhead. In abstract machines this overhead shows up as the cost of performing updates, many of them actually unnecessary, and also in the cost of the associated bookkeeping, that is keeping track of when and where to update. In spineless abstract machines, such as the STG-machine and the TIM, this bookkeeping consists of pushing, checking for and popping update markers. Checking for update markers is a very frequent operation and indeed the implementation of the STG-machine has been optimised for fast update marker checks at the expense of making the pushing and popping of update markers more costly.In this paper we present a type based sharing analysis that can determine when updates can be safely omitted and marker checks bypassed. The type system is proved sound with respect to the lazy Krivine machine. We have implemented the analysis and the preliminary benchmarks seem very promising. Most notably, virtually all update marker checks can be avoided. This may make the tradeoffs of current implementations obsolete and calls for new abstract machine designs.
Taming effects with monadic typing
Authors: Kieburtz Richard B.
Published: November 2005

The familiar Hindley-Milner type system of the ML language family is extended with monad annotations to account for possible side effects of expression evaluation. This also allows effects to be effectively encapsulated by lexical scopes Γ with enforcement provided by type checking. A type-and-effects analysis supports type inference. Type soundness and completeness theorems establish the coherence of monadic type inference with the reference semantics of a small ML-style language.
A theory of core fudgets
Authors: Taylor Colin J.
Published: November 2005

The Fudgets system is a toolkit for developing graphical applications in the lazy functional programming language Haskell. In this paper we develop an operational semantics for a subset of this system, inspired by ideas from concurrency theory. A semantic theory based on bisimulation is defined and shown to be a congruence. We consider two applications of this theory: firstly, some equational rules useful for reasoning about Fudget programs are verified; secondly, we show how the operational semantics can be used to check the correctness of implementations of the Fudgets system.
PLAN
Authors: Hicks Michael , Kakkar Pankaj , Moore Jonathan T. , Gunter Carl A. , Nettles Scott
Published: November 2005

PLAN (Packet Language for Active Networks) is a new language for programs that form the packets of a programmable network. These programs replace the packet headers (which can be viewed as very rudimentary programs) used in current networks. As such, PLAN programs are lightweight and of restricted functionality. These limitations are mitigated by allowing PLAN code to call node-resident
service routines
written in other, more powerful languages. This two-level architecture, in which PLAN serves as a scripting or 'glue' language for more general services, is the primary contribution of this paper. We have successfully applied the PLAN programming environment to implement an IP-free internetwork.PLAN is based on the simply typed lambda calculus and provides a restricted set of primitives and datatypes. PLAN defines a special construct called a
chunk
used to describe the remote execution of PLAN programs on other nodes. Primitive operations on chunks are used to provide basic data transport in the network and to support layering of protocols. Remote execution can make debugging difficult, so PLAN provides strong static guarantees to the programmer, such as type safety. A more novel property aimed at protecting network availability is a guarantee that PLAN programs use a bounded amount of network resources.
Programming with variable functions
Authors: Odersky Martin
Published: November 2005

What is a good method to specify and derive imperative programs? This paper argues that a new form of functional programming fits the bill: where
variable functions
can be updated at specified points in their domain.Traditional algebraic specification and functional programming are a powerful pair of tools for specifying and implementing domains of discourse and operations on them. Recent work on evolving algebras has introduced the function update in algebraic specifications, and has applied it with good success in the modelling of reactive systems. We show that similar concepts allow one to derive efficient programs in a systematic way from functional specifications. The final outcome of such a derivation can be made as efficient as a traditional imperative program with pointers, but can still be reasoned about at a high level.Variable functions can also play an important role in the structuring of large systems. They can subsume object-oriented programming languages, without incurring the latter's problems with pointer aliasing and modularity.
Compiling standard ML to Java bytecodes
Authors: Benton Nick , Kennedy Andrew , Russell George
Published: November 2005

MLJ compiles SML'97 into verifier-compliant Java byte-codes. Its features include type-checked interlanguage working extensions which allow ML and Java code to call each other, automatic recompilation management, compact compiled code and runtime performance which, using a 'just in time' compiling Java virtual machine, usually exceeds that of existing specialised bytecode interpreters for ML. Notable features of the compiler itself include whole-program optimisation based on rewriting, compilation of polymorphism by specialisation, a novel monadic intermediate language which expresses effect information in the type system and some interesting data representation choices.
Typed cross-module compilation
Authors: Shao Zhong
Published: November 2005

Higher-order modules are very effective in structuring large programs and defining generic, reusable software components. Unfortunately, many compilation techniques for the core languages do not work across the module boundaries. As a result, few optimizing compilers support these module facilities well.This paper exploits the semantic property of ML-style modules to support efficient cross-module compilation. More specifically, we present a type-directed translation of the MacQueen-Tofte higher-order modules into a predicative variant of the polymorphic λ-calculus F
ω
. Because modules can be compiled in the same way as ordinary polymorphic functions, standard type-based optimizations such as representation analysis immediately carry over to the module languages.We further show that the full-transparency property of the MacQueen-Tofte system yields a near optimal cross-module compilation framework. By propagating various static information through the module boundaries, many static program analyses for the core languages can be extended to work across higher-order modules.
The spineless tagless G-machine, naturally
Authors: Mountjoy Jon
Published: November 2005

The application of natural semantic specifications of lazy evaluation to areas such as usage analysis, formal profiling and abstract machine construction has shown it to be a useful formalism. This paper introduces several variants and extensions of this specification.The first variant is derived from observations of the Spineless Tagless G-machine (STG), used in the Glasgow Haskell compiler. We present a modified natural semantic specification which can be formally manipulated to derive an STG-like machine.The second variant is the development of a natural semantic specification which allows functions to be applied to more than one argument at once. The STG and TIM abstract machines both allow this kind of behaviour, and we illustrate a use of this semantics by again modifying this semantics following observations of the STG machine. The resulting semantics can be used to formally derive the STG machine. This effectively proves the STG machine correct with respect to Launchbury's semantics.En route, we also show that update markers in the STG machine are necessary for termination, and show how well-known abstract machine instructions, such as the
squeeze
operation, appear quite naturally as optimisations of the derived abstract machine.
Pragmatic subtyping in polymorphic languages
Authors: Nordlander Johan
Published: November 2005

We present a subtyping extension to the Hindley/Milner type system that is based on
name inequivalence
. This approach allows the subtype relation to be defined by incremental construction of polymorphic records and datatypes, in a way that subsumes the basic type systems of both languages like ML and Java. As the main contribution of the paper, we describe a partial type inference algorithm for the extended system which favours succinctness over generality, in the sense that it never infers types with subtype constraints. The algorithm is based on an efficient approximating constraint solver, and is able to type a wide range of programs that utilize subtyping and polymorphism in a non-trivial way. Since constrained types are not inferred, the algorithm cannot be complete; however, we provide a completeness result w.r.t. the Hindley/Milner type system as a form of characterizing lower bound.
Cayenne—a language with dependent types
Authors: Augustsson Lennart
Published: November 2005

Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the
result type
of a function may depend on the
argument value
, and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts.Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.
Fold and unfold for program semantics
Authors: Hutton Graham
Published: November 2005

In this paper we explain how recursion operators can be used to structure and reason about
program semantics
within a functional language. In particular, we show how the recursion operator
fold
can be used to structure denotational semantics, how the dual recursion operator
unfold
can be used to structure operational semantics, and how algebraic properties of these operators can be used to reason about program semantics. The techniques are explained with the aid of two main examples, the first concerning arithmetic expressions, and the second concerning Milner's concurrent language CCS. The aim of the paper is to give functional programmers new insights into recursion operators, program semantics, and the relationships between them.
Encoding types in ML-like languages
Authors: Yang Zhe
Published: November 2005

A Hindley-Milner type system such as ML's seems to prohibit type-indexed values,
i.e
., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different types. The goal of our work is to demonstrate how to program with type-indexed values within a Hindley-Milner type system.Our first approach is to interpret an input type as its corresponding value, recursively. This solution is type-safe, in the sense that the ML type system statically prevents any mismatch between the input type and function arguments that depend on this type.Such specific type interpretations, however, prevent us from combining different type-indexed values that share the same type. To meet this objection, we focus on finding a value-independent type encoding that can be shared by different functions. We propose and compare two solutions. One requires first-class and higher-order polymorphism, and, thus, is not implementable in the core language of ML, but it can be programmed using higher-order functors in Standard ML of New Jersey. Its usage, however, is clumsy. The other approach uses embedding/projection functions. It appears to be more practical.We demonstrate the usefulness of type-indexed values through examples including type-directed partial evaluation, C printf-like formatting, and subtype coercions. Finally, we discuss the tradeoffs between our approach and some other solutions based on more expressive typing disciplines.
Intensional polymorphism in type-erasure semantics
Authors: Crary Karl , Weirich Stephanie , Morrisett Greg
Published: November 2005

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion.We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.
Barrier techniques for incremental tracing
Authors: Pirinen Pekka P.
Published: November 2005

This paper presents a classification of barrier techniques for interleaving tracing with mutator operation during an incremental garbage collection. The two useful tricolour invariants are derived from more elementary considerations of graph traversal. Barrier techniques for maintaining these invariants are classified according to the action taken at the barrier (such as scanning an object or changing its colour), and it is shown that the algorithms described in the literature cover all the possibilities except one. Unfortunately, the new technique is impractical. Ways of combining barrier techniques are also discussed.
Using generational garbage collection to implement cache-conscious data placement
Authors: Chilimbi Trishul M. , Larus James R.
Published: November 2005

The cost of accessing main memory is increasing. Machine designers have tried to mitigate the consequences of the processor and memory technology trends underlying this increasing gap with a variety of techniques to reduce or tolerate memory latency. These techniques, unfortunately, are only occasionally successful for pointer-manipulating programs. Recent research has demonstrated the value of a complementary approach, in which pointer-based data structures are reorganized to improve cache locality.This paper studies a technique for using a generational garbage collector to reorganize data structures to produce a cache-conscious data layout, in which objects with high temporal affinity are placed next to each other, so that they are likely to reside in the same cache block. The paper explains how to collect, with low overhead, real-time profiling information about data access patterns in object-oriented languages, and describes a new copying algorithm that utilizes this information to produce a cache-conscious object layout.Preliminary results show that this technique reduces cache miss rates by 21--42%, and improves program performance by 14--37% over Cheney's algorithm. We also compare our layouts against those produced by the Wilson-Lam-Moher algorithm, which attempts to improve program locality at the page level. Our cache-conscious object layouts reduces cache miss rates by 20--41% and improves program performance by 18--31% over their algorithm, indicating that improving locality at the page level is not necessarily beneficial at the cache level.
Memory management for Prolog with tabling
Authors: Demoen Bart , Sagonas Konstantinos
Published: November 2005

Tabling can be implemented in a (WAM-based) Prolog system by means of SLG-WAM: consumers suspend and their state is preserved by freezing the execution stacks. XSB is a system that currently implements tabling based on the SLG-WAM. The memory model is quite complex and attempts to understand the notion of usefulness of data in XSB well enough to build a precise garbage collector have failed in the past. CAT is a recent alternative to SLG-WAM: it suspends consumers by copying parts of the execution stacks. The memory model is simpler and the design of a more precise garbage collector became feasible. CAT also provided the necessary insights in the usefulness of data in the context of the SLG-WAM. This paper describes the memory management of tabled logic programming systems, whether based on the SLG-WAM or on CAT. Since CAT can perform arbitrarily worse than SLG-WAM space-wise, a minor garbage collection on creation of the CAT areas is proposed as a remedy; its effectiveness is discussed.
The bits between the lambdas
Authors: Wallace Malcolm , Runciman Colin
Published: November 2005

For the programmer, storage media are usually assumed to have a minimum atomic unit of transfer of one byte. However, sometimes it is useful to have an even finer storage granularity of one bit, for instance in order to compress data.This paper describes an API in the lazy functional language Haskell for treating storage media as arbitrary-length streams of bits without byte-alignment constraints. So far as possible, storage media are treated uniformly. In particular, bit-stream memory and binary files share the same API -- a new and useful abstraction over memory management and file management. This uniformity of access leads to a novel technique for lazy random-access to files in a purely functional manner. We also describe a technique for automatically deriving compressed binary representations of user-defined data structures, whose operations provide both in-heap data compression and convenient high-level binary I/O.Of many possible applications, we illustrate the processing of Huffman-encoded image data, and a bibliographic information system which uses lazy B-trees for efficient storage management.
Portable run-time type description for conventional compilers
Authors: Kakkad Sheetal V. , Johnstone Mark S. , Wilson Paul R.
Published: November 2005

Many useful programming language extensions and system support libraries require knowledge of the locations of fields within objects at run time. Examples include orthogonal persistent object stores, precise garbage collectors, data structure picklers, and parameter marshaling schemes.For clean and efficient implementation as libraries, these systems require run-time knowledge of in-memory layouts of data objects, which is unavailable in most traditionally compiled and linked programming languages, such as C, C++, and Ada. Even the recently standardized
run-time type identification
(RTTI) feature in C++ is insufficient, because it describes only language-level features of the type hierarchy and not the compiler-dependent object layout decisions.We present a facility for
run-time type description
, or RTTD, which extracts low-level layout information from debugging information generated by conventional compilers, and makes it available to user programs. We believe this to be the simplest and most portable approach to run-time type description, requiring no changes to existing compilers. In this paper, we describe the basic strategies and present details of our implementation for C++. We also sketch some extensions that we have implemented, including special treatment of C++'s virtual function table pointers to match persistent or foreign data objects with the actual code in a particular application.Our implementation of run-time type description is freely available. It is in regular use with multiple operating systems and compilers, in both free and commercial products, including a high-performance persistent object storage system for C++ and a real-time garbage collector.
Memory allocation for long-running server applications
Authors: Larson Per-Åke , Krishnan Murali
Published: November 2005

Prior work on dynamic memory allocation has largely neglected long-running server applications, for example, web servers and mail servers. Their requirements differ from those of one-shot applications like compilers or text editors. We investigated how to build an allocator that is not only fast and memory efficient but also scales well on SMP machines. We found that it is not sufficient to focus on reducing lock contention - higher speedups require a reduction in cache misses and bus traffic. We then designed and prototyped a new allocator, called LKmalloc, targeted for both traditional applications and server applications. LKmalloc uses several subheaps, each one with a separate set of free lists and memory arena. A thread always allocates from the same subheap but can free a block belonging to any subheap. A thread is assigned to a subheap by hashing on its thread ID. WC compared its performance with several other allocators on a server-like, simulated workload and found that it indeed scales well and is quite fast hut memory more efficiently.
Load-reuse analysis
Authors: Bodík Rastislav , Gupta Rajiv , Soffa Mary Lou
Published: November 2005

Load-reuse analysis finds instructions that repeatedly access the same memory location. This location can be promoted to a register, eliminating redundant loads by reusing the results of prior memory accesses. This paper develops a load-reuse analysis and designs a method for evaluating its precision.In designing the analysis, we aspire for
completeness
---the goal of exposing all reuse that can be harvested by a subsequent program transformation. For register promotion, a suitable transformation is partial redundancy elimination (PRE). To approach the ideal goal of PRE-completeness, the load-reuse analysis is phrased as a data-flow problem on a program representation that is
path-sensitive
, as it detects reuse even when it originates in a different instruction along each control flow path. Furthermore, the analysis is
comprehensive
, as it treats scalar, array and pointer-based loads uniformly.In evaluating the analysis, we compare it with an ideal analysis. By observing the run-time stream of memory references, we collect all PRE-exploitable reuse and treat it as the ideal analysis performance. To compare the (static) load-reuse analysis with the (dynamic) ideal reuse, we use an
estimator
algorithm that computes, given a data-flow solution and a program profile, the dynamic amount of reuse detected by the analysis. We developed a family of estimators that differ in how well they bound the profiling error inherent in the
edge
profile. By bounding the error, the estimators offer a precise and practical method for determining the run-time optimization benefit.Our experiments show that about 55% of loads executed in Spec95 exhibit reuse. Of those, our analysis exposes about 80%.
Using node merging to enhance graph coloring
Authors: Vegdahl Steven R.
Published: November 2005

A Chaitin-style register allocator often blocks during its simplification phase because no node in the interference graph has a degree that is sufficiently small. Typically, this is handled by node-splitting, or by optimistically continuing---and hoping that a legal N-coloring will still be found. We observe that the merging of two nodes in a graph causes a reduction in the degree of any node that had been adjacent to both. We have enhanced Chaitin's coloring algorithm so that it attempts node-merging during graph simplification; this often allows simplification to continue, while still guaranteeing a coloring for the graph. We have tested this algorithm using Appel's database of register-coloring graphs, and have compared it with Chaitin's algorithm. The merge-enhanced algorithm yields a better coloring about 8% of the time, and a worse coloring less than 0.1% of the time.
A fast Fourier transform compiler
Authors: Frigo Matteo
Published: November 2005

The FFTW library for computing the discrete Fourier transform (DFT) has gained a wide acceptance in both academia and industry, because it provides excellent performance on a variety of machines (even competitive with or faster than equivalent libraries supplied by vendors). In FFTW, most of the performance-critical code was generated automatically by a special-purpose compiler, called genfft, that outputs C code. Written in Objective Caml, genfft can produce DFT programs for any input length, and it can specialize the DFT program for the common case where the input data are real instead of complex. Unexpectedly, genfft "discovered" algorithms that were previously unknown, and it was able to reduce the arithmetic complexity of some other existing algorithms. This paper describes the internals of this special-purpose compiler in some detail, and it argues that a specialized compiler is a valuable tool.
A new framework for debugging globally optimized code
Authors: Wu Le-Chun , Mirani Rajiv , Patil Harish , Olsen Bruce , Hwu Wen-mei W.
Published: November 2005

With an increasing number of executable binaries generated by optimizing compilers today, providing a clear and correct source-level debugger for programmers to debug optimized code has become a necessity. In this paper, a new framework for debugging globally optimized code is proposed. This framework consists of a new code location mapping scheme, a data location tracking scheme, and an emulation-based forward recovery model. By taking over the control early and emulating instructions selectively, the debugger can preserve and gather the required program state for the recovery of expected variable values at source breakpoints. The framework has been prototyped in the IMPACT compiler and GDB-4.16. Preliminary experiments conducted on several SPEC95 integer programs have yielded encouraging results. The extra time needed for the debugger to calculate the limits of the emulated region and to emulate instructions is hardly noticeable, while the increase in executable file size due to the extra debug information is on average 76% of that of the executable file with no debug information.
A theory of type qualifiers
Authors: Foster Jeffrey S. , Fähndrich Manuel , Aiken Alexander
Published: November 2005

We describe a framework for adding type qualifiers to a language. Type qualifiers encode a simple but highly useful form of subtyping. Our framework extends standard type rules to model the flow of qualifiers through a program, where each qualifier or set of qualifiers comes with additional rules that capture its semantics. Our framework allows types to be polymorphic in the type qualifiers. We present a const-inference system for C as an example application of the framework. We show that for a set of real C programs, many more consts can be used than are actually present in the original code.
Static single assignment form for machine code
Authors: Leung Allen , George Lal
Published: November 2005

Static Single Assignment (SSA) is an effective intermediate representation in optimizing compilers. However, traditional SSA form and optimizations are not applicable to programs represented as native machine instructions because the use of dedicated registers imposed by calling conventions, the runtime system, and target architecture must be made explicit. We present a simple scheme for converting between programs in machine code and in SSA, such that references to dedicated physical registers in machine code are preserved. Our scheme ignores all output- and anti-dependences imposed by physical registers while a program is in SSA form, but inserts compensation code during machine code reconstruction if any naming requirements have been violated. By resolving all mismatches between the two representations in separate phases, we are able to utilize existing SSA algorithms unaltered to perform machine code optimizations.
Automatic inference of models for statistical code compression
Authors: Fraser Christopher W.
Published: November 2005

This paper describes experiments that apply machine learning to compress computer programs, formalizing and automating decisions about instruction encoding that have traditionally been made by humans in a more ad hoc manner. A program accepts a large training set of program material in a conventional compiler intermediate representation (IR) and automatically infers a decision tree that separates IR code into streams that compress much better than the undifferentiated whole. Driving a conventional arithmetic compressor with this model yields code 30% smaller than the previous record for IR code compression, and 24% smaller than an ambitious optimizing compiler feeding an ambitious general-purpose data compressor.
Compressing Java class files
Authors: Pugh William
Published: November 2005

Java class files are often distributed as jar files, which are collections of individually compressed class files (and possibility other files). Jar files are typically about 1/2 the size of the original class files due to compression. I have developed a wire-code format for collections of Java class files. This format is typically 1/2 to 1/5 of the size of the corresponding compressed jar file (1/4 to 1/10 the size of the original class files).
EQL — the query language you never heard of
Authors: Havener Charles D.
Published: November 2005

This paper describes a novel but unknown query language for large parallel database applications. EQL is compiled to C++, the new universal assembly language. Using YACC and CO techniques, EQL is representative of projects students of compiler design might implement in the business world.
Java's insecure parallelism
Authors: Hansen Per Brinch
Published: November 2005

The author examines the synchronization features of Java and finds that they are insecure variants of his earliest ideas in parallel programming published in 1972-73. The claim that Java supports monitors is shown to be false. The author concludes that Java ignores the last twenty-five years of research in parallel programming languages.
Early storage reclamation in a tracing garbage collector
Authors: Harris Timothy
Published: November 2005

This article presents a novel technique for allowing the early recovery of storage space occupied by garbage data. The idea is similar to that of generational garbage collection, except that heap is partitioned based on a static analysis of data type definitions rather than on the approximate age of allocated objects. A prototype implementation is presented, along with initial results and ideas for future work.
Effective exploitation of a zero overhead loop buffer
Authors: Uh Gang-Ryung , Wang Yuhong , Whalley David , Jinturkar Sanjay , Burns Chris , Cao Vincent
Published: November 2005

A Zero Overhead Loop Buffer (ZOLB) is an architectural feature that is commonly found in DSP processors. This buffer can be viewed as a compiler managed cache that contains a sequence of instructions that will be executed a specified number of times. Unlike techniques such as loop unrolling, a loop buffer is a hardware technique that can be used to minimize loop overhead without the penalty of increasing code size. In addition, a ZOLB also requires relatively little space and power, which are both important considerations for most DSP applications. This paper describes strategies for generating code to effectively use a ZOLB. The authors have found that many common improving transformations used by optimizing compilers to improve code on conventional architectures are shown (1) to allow more loops to be placed in a ZOLB and (2) to further reduce loop overhead of the loops placed in a ZOLB. The results given in this paper demonstrate that this architectural feature can often be exploited with substantial improvements in execution time and slight reductions in code size.
Live memory analysis for garbage collection in embedded systems
Authors: Persson Patrik
Published: November 2005

Real-time garbage collection is essential if object-oriented languages (in particular, Java) are to become predictable enough for real-time embedded systems. Although techniques for hard real-time garbage collection exist, they are based on estimations of the maximum amount of referenced (live) memory. Such estimations may be difficult to derive manually for complex programs.We present techniques for predicting the maximum amount of live memory in object-oriented languages with inheritance and virtual methods. Annotations are used to bound recursively defined data structures. The annotations may also be used for timing analysis of code traversing annotated structures.A prototype live memory analysis tool has been developed. The tool interactively provides predictions of the maximum amount of live memory referenced from an arbitrary reference or block in an object-oriented program.
Scheduling garbage collector for embedded real-time systems
Authors: Kim Taehyoun , Chang Naehyuck , Kim Namyun , Shin Heonshik
Published: November 2005

This paper proposes a new scheduling method for multiple mutators and a garbage collector running on embedded real-time systems with a single processor and no virtual memory. The hard real-time tasks should reserve a certain amount of heap memory to prevent memory starvation and/or deadline miss. Since the memory requirement depends on the worst-case response time of a garbage collector, the traditional approach in which garbage collection is performed in the background demands large memory space. The proposed scheduling algorithm is based on an aperiodic scheduling technique,
sporadic server
. This paper also presents a modified copying garbage collection algorithm with hardware support. In order to minimize the worst-case response time of a garbage collector thus reducing the memory requirement, the garbage collector runs as the highest priority task with a preset bandwidth. This paper also investigates the schedulability of a garbage collector and mutator tasks as well as the worst-case memory requirement. Performance analysis shows that the proposed algorithm can provide a considerable reduction in the worst-case memory requirement compared with the background policy. Simulation results demonstrate that the proposed algorithm can produce the
feasible
memory requirement comparable to the complex on-line scheduling algorithm such as slack stealing.
Table-based QoS control for embedded real-time systems
Authors: Tomoyoshi Sugawara , Kosuke Tatsukawa
Published: November 2005

This paper proposes a new QoS control scheme that is suited for embedded real-time systems. Our scheme focused on real-time systems where both device control and multimedia processing are required. Such systems needs to keep timing constraints of control tasks while providing the highest possible quality of service(QoS) to multimedia processing tasks. Although many QoS control schemes are proposed and used in distributed multimedia systems, they are not suited for such real-time systems. Their QoS control policies cannot exactly keep the timing constraints of control tasks.To overcome this problem we chose a scheme which uses a table describing resource requirements of all tasks. Resource allocations for tasks and total resource utilization in a system can be calculated from the table. Using our scheme, any QoS control policies, such as a fair-share policy or a priority based policy, can be implemented. In other words, it has become possible for the first time to allow the intention of system designers to be directly reflected on QoS control.We have implemented a CPU time QoS control mechanism based on our proposed scheme and evaluated it on a μ-ITRON Ver. 3.0 based real-time OS. The evaluation results demonstrate that the QoS control scheme can keep deadline misses low and CPU utilization high under an overloaded state. The results also show that overhead of the QoS control mechanism is small enough to support both multimedia and control applications.
Performance re-engineering of embedded real-time systems
Authors: Ryu Minsoo , Park Jungkeun , Kim Kimoon , Seo Yangmin , Hong Seongsoo
Published: November 2005

This paper formulates a problem of embedded real-time system re-engineering, and presents its solution approach. The re-engineering of an embedded system is defined as a development task of meeting newly imposed performance requirements after its hardware and software have been fully implemented. The performance requirements may include a real-time throughput and an input-to-output latency. The proposed solution approach is based on a bottleneck analysis and nonlinear optimization. Inputs to the approach include a system design specified with a process network and a set of task graphs, task allocation and scheduling, and a new real-time throughput requirement specified as a system's period constraint.The solution approach works in two steps. In the first step, it determines bottleneck processes in the process network via estimation of process latencies. In the second step, it derives a system of constraints with performance scaling factors of processing elements being variables. It then solves the constraints for the performance scaling factors with an objective of minimizing the total hardware cost of the resultant system. These scaling factors suggest the minimal cost hardware upgrade to meet the new performance requirements. Since this approach does not modify carefully designed software structures, it helps reduce the reengineering cycle.
A software synthesis tool for distributed embedded system design
Authors: Kang D.-I. , Gerber R. , Golubchik L. , Hollingsworth J. K. , Saksena M.
Published: November 2005

We present a design tool for automated synthesis of embedded systems on distributed COTS-based platforms. Our synthesis tool consists of (1) a graphical user interface for input of software layouts, which maps tasks to resources and (2) a constraints solving engine, which allocates local resources to tasks, all with the goal of meeting specified performance criteria. Our tool differs from previous work in that it allows (a) use of stochastic (rather than worst-case) models of resource usage and (b) resource sharing among components. Our approach uses analytical approximate solutions for quick estimates of the desired performance measures. These estimates permit an efficient search of the possible design space. Once candidate designs are determined, they are validated through a simulation model. We demonstrate the efficiency and robustness of this tool on a synthetic aperture radar benchmark.
Issues and challenges in developing embedded software for information appliances and telecommunication terminals
Authors: Ryu In
Published: November 2005

Information appliances are emerging in the consumer electronics market with the convergence of disparate technologies including internet access, wireless connectivity, digital audio/video support, and platform independent middleware services. This presents a great deal of new challenges to developers in the consumer electronics industry due to extremely diverse hardware components and increased software complexity.This presentation will raise a variety of technical issues we have encountered during the development of various commercial products such as digital TVs, web video phones, wireless handsets, and CDMA terminals. We will discuss in detail about proliferation of the types of consumer devices, diversity in hardware and component software technologies, and newly emerging data storage technologies for embedded systems. We will also touch upon other essential issues for embedded systems development such as quality assurance, fault isolation, power management, and optimal system design based on functional partitioning.
Trampolined style
Authors: Ganz Steven E. , Friedman Daniel P. , Wand Mitchell
Published: November 2005

A trampolined program is organized as a single loop in which computations are scheduled and their execution allowed to proceed in discrete steps. Writing programs in trampolined style supports primitives for multithreading without language support for continuations. Various forms of trampolining allow for different degrees of interaction between threads. We present two architectures based on an only mildly intrusive trampolined style. Concurrency can be supported at multiple levels of granularity by performing the trampolining transformation multiple times.
Tracing piece by piece
Authors: Nilsson Henrik
Published: November 2005

The advantage of lazy functional languages is that programs may be written declaratively without specifying the exact evaluation order. The ensuing order of evaluation can however be quite involved which makes it difficult to debug such programs using traditional, operational techniques. A solution is to trace the computation in a way which focuses on the declarative aspects and hides irrelevant operational details. The main problem with this approach is the immense cost in time and space of tracing large computations. Dealing with these performance issues is thus the key to practical, general purpose debuggers for lazy functional languages. In this paper we show that computing partial traces on demand by re-executing the traced program is a viable way to overcome these difficulties. This allows any program to be traced using only a fixed amount of extra storage. Since it takes a lot of time to build a complete trace, most of which is wasted since only a fraction of a typical trace is investigated during debugging, partial tracing and repeated re-execution is also attractive from a time perspective. Performance figures are presented to substantiate our claims.
Atomic heap transactions and fine-grain interrupts
Authors: Shivers Olin , Clark James W. , McGrath Roland
Published: November 2005

Languages such as Java, ML, Scheme, and Haskell provide automatic storage management, that is, garbage collection. The two fundamental operations performed on a garbage-collected heap are "allocate" and "collect." Because the heap is in an inconsistent state during these operations, they must be performed atomically. Otherwise, a heap client might access the heap during a time when its fundamental invariants do not hold, corrupting the heap.Standard techniques for providing this atomicity guarantee have large latencies and other performance problems that impede their application in high-performance, interruptladen, thread-based systems applications. In particular, the standard techniques prevent thread schedulers from switching threads on VM page faults.We cast the space of possible implementations into a general taxonomy, and describe a new technique that provides a simple, low-overhead, low-latency interlock. We have implemented this technique in a version of SML/NJ, and, because of its applicability to thread-based systems, are currently implementing it in the scheduler of our raw-hardware SML-based kernel, ML/OS. Our technique can be extended to provide other atomic sequences besides storage allocation.
A simple proof technique for certain parametricity results
Authors: Crary Karl
Published: November 2005

Many properties of parametric, polymorphic functions can be determined simply by inspection of their types. Such results are usually proven using Reynolds's parametricity theorem. However, Reynolds's theorem can be difficult to show in some settings, particularly ones involving computational effects. I present an alternative technique for proving some parametricity results. This technique is considerably simpler and easily generalizes to effectful settings. It works by instantiating polymorphic functions with singleton types that fully specify the behavior of the functions. Using this technique, I show that callers' stacks are protected from corruption during function calls in Typed Assembly Language programs.
Relating typability and expressiveness in finite-rank intersection type systems (extended abstract)
Authors: Kfoury Assaf J. , Mairson Harry G. , Turbak Franklyn A. , Wells J. B.
Published: November 2005

We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ
1
Λ τ
2
to be used in some places at type τ
1
and in other places at type τ
2
. A
finite-rank
intersection type system bounds how deeply the Λ can appear in type expressions. Such type systems enjoy strong normalization, subject reduction, and computable type inference, and they support a pragmatics for implementing parametric polymorphism. As a consequence, they provide a conceptually simple and tractable alternative to the impredicative polymorphism of System F and its extensions, while typing many more programs than the Hindley-Milner type system found in ML and Haskell.While type inference is computable at every rank, we show that its complexity grows exponentially as rank increases. Let
K
(0,
n
) =
n
and
K
(
t
+ 1,
n
) = 2

K
(
t,n
)

; we prove that recognizing the pure λ-terms of size
n
that are typable at rank
k
is complete for
DTIME
[
K
(
k
−1,
n
)]. We then consider the problem of deciding whether two λ-terms typable at rank
k
have the same normal form, generalizing a well-known result of Statman from simple types to finite-rank intersection types. We show that the equivalence problem is
DTIME
[
K
(
K
(
k
− 1,
n
), 2)]-complete. This relationship between the complexity of typability and expressiveness is identical in wellknown decidable type systems such as simple types and Hindley-Milner types, but seems to fail for System F and its generalizations. The correspondence gives rise to a conjecture that if Τ is a predicative type system where typability has complexity
t
(
n
) and expressiveness has complexity
e
(
n
), then
t
(
n
) = Ω(log*
e
(
n
)).
Type fixpoints
Authors: Spławski Zdzisław , Urzyczyn Paweł
Published: November 2005

Positive recursive (fixpoint) types can be added to the polymorphic (Church-style) lambda calculus λ2 (System
F
) in several different ways, depending on the choice of the elimination operator. We compare several such definitions and we show that they fall into two equivalence classes with respect to mutual interpretability by means of beta-eta reductions. Elimination operators for fixpoint types are thus classified as either "iterators" or "recursors". This classification has an interpretation in terms of the Curry-Howard correspondence: types of iterators and recursors can be seen as images of induction axioms under different dependency-erasing maps. Systems with recursors are beta-eta equivalent to a calculus λ2U of recursive types with the operators
Fold
: σ[μα.σ/α]←μα.σ and
Unfold
: μα.σ←σ[μα.σ/α], where the composition
Unfold
or
Fold
reduces to identity.It is known that systems with iterators can be defined within λ2, by means of beta reductions. We conjecture that systems with recursors can not. In this paper we show that the system λ2U does not have such a property. For this we study the notion of polymorphic type embeddability (via (beta) left-invertible terms) and we show that if a type σ is embedded into another type τ then τ must be of depth at least equal to the depth of σ.