bluuebunny/crossref_metadata_2025 huggingface dataset:
Formal online methods for voltage/frequency control in multiple clock domain microprocessors
Authors: Wu Qiang , Juang Philo , Martonosi Margaret , Clark Douglas W.
Published: November 2005

Multiple Clock Domain (MCD) processors are a promising future alternative to today's fully synchronous designs. Dynamic Voltage and Frequency Scaling (DVFS) in an MCD processor has the extra flexibility to adjust the voltage and frequency in each domain independently. Most existing DVFS approaches are profile-based offline schemes which are mainly suitable for applications whose execution char-acteristics are constrained and repeatable. While some work has been published about online DVFS schemes, the prior approaches are typically heuristic-based. In this paper, we present an effective online DVFS scheme for an MCD processor which takes a formal analytic approach, is driven by dynamic workloads, and is suitable for all applications. In our approach, we model an MCD processor as a queue-domain network and the online DVFS as a feedback control problem with issue queue occupancies as feedback signals. A dynamic stochastic queuing model is first proposed and linearized through an accu-rate linearization technique. A controller is then designed and verified by stability analysis. Finally we evaluate our DVFS scheme through a cycle-accurate simulation with a broad set of applications selected from MediaBench and SPEC2000 benchmark suites. Compared to the best-known prior approach, which is heuristic-based, the proposed online DVFS scheme is substantially more effective due to its automatic regulation ability. For example, we have achieved a 2-3 fold increase in efficiency in terms of energy-delay product improvement. In addition, our control theoretic technique is more resilient, requires less tuning effort, and has better scalability as compared to prior online DVFS schemes.We believe that the techniques and methodology described in this paper can be generalized for energy control in processors other than MCD, such as tiled stream processors.
Polymorphic bytecode
Authors: Ancona Davide , Damiani Ferruccio , Drossopoulou Sophia , Zucca Elena
Published: November 2005

We define
compositional compilation
as the ability to typecheck source code fragments in isolation, generate corresponding binaries,and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but also depends on the compilation context.We propose a way to obtain compositional compilation for Java, by introducing a
polymorphic form of bytecode
containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard) bytecode that can be obtained by replacing type variables with classes satisfying the associated constraints.We illustrate our proposal by developing a typing and a linking algorithm. The typing algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment and constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, linking a self-contained collection of fragments either fails, or produces standard bytecode (the same as would have been produced by standard compilation of all fragments).
A bisimulation for type abstraction and recursion
Authors: Sumii Eijiro , Pierce Benjamin C.
Published: November 2005

We present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary, using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and ΤΤ-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider
sets
of relations---instead of just relations---as bisimulations.
Transition predicate abstraction and fair termination
Authors: Podelski Andreas , Rybalchenko Andrey
Published: November 2005

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We extend predicate abstraction to
transition predicate
abstraction. Transition predicate abstraction goes beyond the idea of finite
abstract-state
programs (and checking the absence of loops). Instead, our abstraction algorithm transforms a program into a finite
abstract-transition
program. Then, a second algorithm checks fair termination. The two algorithms together yield an automated method for the verification of liveness properties under full fairness assumptions (justice and compassion). In summary, we exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of temporal properties.
Permission accounting in separation logic
Authors: Bornat Richard , Calcagno Cristiano , O'Hearn Peter , Parkinson Matthew
Published: November 2005

A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads, subdivision and combination of permission is discussed. The roots of the approach are in Boyland's [3] demonstration of the utility of fractional permissions in specifying non-interference between concurrent threads. We add the notion of counting permission, which mirrors the programming technique called permission counting. Both fractional and counting permissions permit passivity, the specification that a program can be permitted to access a heap cell yet prevented from altering it. Models of both mechanisms are described. The use of two different mechanisms is defended. Some interesting problems are acknowledged and some intriguing possibilities for future development, including the notion of resourcing as a step beyond typing, are paraded.
Precise interprocedural analysis using random interpretation
Authors: Gulwani Sumit , Necula George C.
Published: November 2005

We describe a unified framework for random interpretation that generalizes previous randomized intraprocedural analyses, and also extends naturally to efficient interprocedural analyses. There is no such natural extension known for deterministic algorithms. We present a general technique for extending any intraprocedural random interpreter to perform a context-sensitive interprocedural analysis with only polynomial increase in running time. This technique involves computing
random
summaries of procedures, which are complete and probabilistically sound.As an instantiation of this general technique, we obtain the first polynomial-time randomized algorithm that discovers all linear relationships interprocedurally in a linear program. We also obtain the first polynomial-time randomized algorithm for precise interprocedural value numbering over a program with unary uninterpreted functions.We present experimental evidence that quantifies the precision and relative speed of the analysis for discovering linear relationships along two dimensions: intraprocedural vs. interprocedural, and deterministic vs. randomized. We also present results that show the variation of the error probability in the randomized analysis with changes in algorithm parameters. These results suggest that the error probability is much lower than the existing conservative theoretical bounds.
Automated soundness proofs for dataflow analyses and transformations via local rules
Authors: Lerner Sorin , Millstein Todd , Rice Erika , Chambers Craig
Published: November 2005

We present Rhodium, a new language for writing compiler optimizations that can be automatically proved sound. Unlike our previous work on Cobalt, Rhodium expresses optimizations using explicit dataflow facts manipulated by local propagation and transformation rules. This new style allows Rhodium optimizations to be mutually recursively defined, to be automatically composed, to be interpreted in both flow-sensitive and -insensitive ways, and to be applied interprocedurally given a separate context-sensitivity strategy, all while retaining soundness. Rhodium also supports infinite analysis domains while guaranteeing termination of analysis. We have implemented a soundness checker for Rhodium and have specified and automatically proven the soundness of all of Cobalt's optimizations plus a variety of optimizations not expressible in Cobalt, including Andersen's points-to analysis, arithmetic-invariant detection, loop-induction-variable strength reduction, and redundant array load elimination.
The Java memory model
Authors: Manson Jeremy , Pugh William , Adve Sarita V.
Published: November 2005

This paper describes the new Java memory model, which has been revised as part of Java 5.0. The model specifies the legal behaviors for a multithreaded program; it defines the semantics of multithreaded Java programs and partially determines legal implementations of Java virtual machines and compilers.The new Java model provides a simple interface for correctly synchronized programs -- it guarantees sequential consistency to data-race-free programs. Its novel contribution is requiring that the behavior of incorrectly synchronized programs be bounded by a well defined notion of causality. The causality requirement is strong enough to respect the safety and security properties of Java and weak enough to allow standard compiler and hardware optimizations. To our knowledge, other models are either too weak because they do not provide for sufficient safety/security, or are too strong because they rely on a strong notion of data and control dependences that precludes some standard compiler transformations.Although the majority of what is currently done in compilers is legal, the new model introduces significant differences, and clearly defines the boundaries of legal transformations. For example, the commonly accepted definition for control dependence is incorrect for Java, and transformations based on it may be invalid.In addition to providing the official memory model for Java, we believe the model described here could prove to be a useful basis for other programming languages that currently lack well-defined models, such as C++ and C#.
Adaptable Java Agents (AJA)
Authors: Badjonski Mihal , Ivanovic Mirjana , Budimac Zoran
Published: November 2005

Agent-building tools have an important role in popularizing agent technology. This paper describes a new agent-programming tool AJA. AJA consists of two programming languages: HADL for defining of higher-level agent constructs and Java+ for low-level programming of these constructs. Among other interesting features AJA presents an original approach of incorporating artificial intelligence techniques, such as artificial neural nets, into a programming language.
Loop-dead optimization
Authors: Shaw Sachin , Kumar Pawan
Published: November 2005

A loop is a critical part of any program. A loop is normally executed a large number of times, hence if any statement can be moved outside the loop then computation can speed-up. Loop invariant computations have been studied in great detail [1, 2]. Here a computation, which does not change inside the loop (on successive execution of the loop), is done before the loop. Such a computation involves only the loop invariant variables. These are variables, whose value does not change inside the loop.Here we talk about a variable, which changes inside the loop, but only the last value is useful. The computation needed in the definition of this variable can be moved outside the loop (after the loop).Formally a loop-dead variable is that which is defined in the loop but not used in the loop. Later we extend this definition as follows: A loop-dead variable is that which is not used inside the loop except in the definition of the other loop dead variables.
Forth and AI revisited
Authors: Frenger Paul
Published: November 2005

Six years ago in this journal we discussed the work of Arthur T. Murray, who endeavored to explore artificial intelligence using the Forth programming language [1]. His creation, which he called MIND.FORTH, was interesting in its ability to understand English sentences in the form: subject-verb-object. It also had the capacity to learn new things and to form mental associations between recent experiences and older memories. In the intervening years, Mr. Murray has continued to develop his MIND.FORTH: he has translated it into Visual BASIC, PERL and Javascript, he has written a book [2] on the subject, and he maintains a wiki web site where anyone may suggest changes or extensions to his design [3]. MIND.FORTH is necessarily complex and opaque by virtue of its functionality; therefore it may be challenging for a newcomer to grasp. However, the more dedicated student will find much of value in this code. Murray himself has become quite a controversial figure.
Parametric polymorphism for Java
Authors: Cabana Brian , Alagić Suad , Faulkner Jeff
Published: November 2005

In spite of years of research toward a solution for the problem of extending Java with parametric polymorphism (genericity) the officially accepted solution already in its beta release allows violation of the Java type system and turns a type safe language into an unsafe one. The run-time type information in this release is incorrect which leads to major problems for the programmers relying on the Java reflective capabilities. We show that there are two basic reasons for these problems. The first one is that the idiom underlying this solution is provably incorrect. The second one is that the problem of extending Java with parametric polymorphism does not have a correct solution unless the Java Virtual Machine is extended to handle it properly. This paper elaborates the subtleties required by a correct implementation technique that includes representation of parametric classes in the standard Java class file format, representation of the instantiated parametric class objects, extensions of the Java Core Reflection to report type information about (instantiated) parametric classes, and the loading techniques required by this solution for extending Java with generics. Previous solutions for this problem are analyzed as well.
Checking spelling in source code
Authors: Hughes Elliott
Published: November 2005

Word processors have long been able to check spelling as a special pass over the whole document, but the feature really came into its own with "check as you type". So useful is this feature (and so well within the capabilities of modern computers) that we now find it in other text-handling applications such as mailers and web browsers. Mac OS offers it on all text components for no extra programming effort. Programs that don't check what you're typing as you type it are becoming increasingly annoying and the surprising number of programs that won't check your spelling at all are even worse.Despite this, the editors and other tools used by programmers are least likely to offer spelling checking. This article looks at why this is, and describes the addition of spelling checking to a programmer's editor.
Methodology work is ontology work
Authors: Marick Brian
Published: November 2005

I argue that a successful switch from one methodology to another requires a switch from one
ontology
to another. Large-scale adoption of a new methodology means "infecting" people with new ideas about what sorts of things there are in the (software development) world and how those things hang together. The paper ends with some suggestions to methodology creators about how to design methodologies that encourage the needed "gestalt switch".
Finding bugs is easy
Authors: Hovemeyer David , Pugh William
Published: November 2005

Many techniques have been developed over the years to automatically find bugs in software. Often, these techniques rely on formal methods and sophisticated program analysis. While these techniques are valuable, they can be difficult to apply, and they aren't always effective in finding real bugs.
Bug patterns
are code idioms that are often errors. We have implemented automatic detectors for a variety of bug patterns found in Java programs. In this paper, we describe how we have used bug pattern detectors to find serious bugs in several widely used Java applications and libraries. We have found that the effort required to implement a bug pattern detector tends to be low, and that even extremely simple detectors find bugs in real applications.From our experience applying bug pattern detectors to real programs, we have drawn several interesting conclusions. First, we have found that even well tested code written by experts contains a surprising number of obvious bugs. Second, Java (and similar languages) have many language features and APIs which are prone to misuse. Finally, that simple automatic techniques can be effective at countering the impact of both ordinary mistakes and misunderstood language features.
Axiomatic computational model
Authors: Mueller Conrad
Published: November 2005

A new model of computation is explored based on axiomatic logic. The significant difference from other models is how reasoning about variables is expressed. The computation is described only by defining variables in terms of other variables. The benefit is the simplicity of the semantics of the axiomatic logic. The model is described in the form of a tutorial using a simple language to illustrate how a program can be expressed in this model.
Dominance analysis of irreducible CFGs by reduction
Authors: Saitou Tetsuo , Suzuki Mitsugu , Watanabe Tan
Published: November 2005

This paper presents a simple and fast algorithm with proof of correctness for analyzing dominance relations of control flow graphs (CFGs). A dominator tree and dominance frontiers are obtained by reducing a DAG, which is obtained by adding dummy vertexes to the original CFG to transmit dominance relation of irreducible loops to the resultant DAG. A specific order of stacking vertexes eliminates the necessity to search for reduction candidates. The computational complexity of the algorithm for a real-world CFG with

M

edges is O(

M

), which is also confirmed by analyzing about 1700 CFGs extracted from real programs.
Analysis of the limitations of multiple client handling in a Java server environment
Authors: Beloglavec Simon , Heričko Marjan , Jurič Matjaž B. , Rozman Ivan
Published: November 2005

A server infrastructure in web servers, message servers and other parallel systems use a variation of two software architectures for providing concurrency: threaded or event-driven. This paper analyzes the performance limitations of concurrent applications implemented in Java. Both architectures have been evaluated and compared with various design patterns, which combine the best practices from both architectures. For each architecture the suitability for handling a large volume of client requests, the efficient management of a server load, the influence of client request structures, and the physical size of a client request, have been studied. The discussed Java APIs are core technologies for high-level APIs, used in developing web and distributed applications. The research also includes performance comparison on various platforms and discusses performance variation on various versions of a Java runtime. The paper contributes to the understanding of Java-based server architecture capabilities. Core server software architectures and required Java libraries are compared, the reasons for the limitations are identified and guidelines for choosing proper combinations are given.
An efficient way to filter out data dependences with a sufficiently large distance between memory references
Authors: Bulić Patricio , Guštin Veselko
Published: November 2005

There are a number of data dependence tests that have been proposed in the literature. The most widely used approximate data dependence tests are the Banerjee inequality and the GCD test. In this paper we consider parallelization for microprocessors with the multimedia extensions. For the short SIMD parallelism extraction it is essential that, if dependency exists, then the distance between memory references is greater than or equal to the number of data processed in the SIMD register. This implies that some loops that could not be vectorized on traditional vector processors can still be parallelized for the short SIMD execution. In this paper we present an accurate and simple method that can filter out data dependences with a sufficiently large distance between memory references for linear array references within a nested loop. The presented method is suitable for use in a dependence analyzer that is organized as a series of tests, progressively increasing in accuracy, as a replacement for the GCD or Banerjee tests.
VYRD
Authors: Elmas Tayfun , Tasiran Serdar , Qadeer Shaz
Published: November 2005

We present a runtime technique for checking that a concurrently-accessed data structure implementation, such as a file system or the storage management module of a database, conforms to an executable specification that contains an atomic method per data structure operation. The specification can be provided separately or a non-concurrent, "atomized" interpretation of the implementation can serve as the specification. The technique consists of two phases. In the first phase, the implementation is instrumented in order to record information into a log during execution. In the second, a separate verification thread uses the logged information to drive an instance of the specification and to check whether the logged execution conforms to it. We paid special attention to the general applicability and scalability of the techniques and to minimizing their concurrency and performance impact. The result is a lightweight verification method that provides a significant improvement over testing for concurrent programs.We formalize conformance to a specification using the notion of refinement: Each trace of the implementation must be equivalent to some trace of the specification. Among the novel features of our work are two variations on the definition of refinement appropriate for runtime checking: I/O and "view" refinement. These definitions were motivated by our experience with two industrial-scale concurrent data structure implementations: the Boxwood project, a B-link tree data structure built on a novel storage infrastructure [10] and the Scan file system [9]. I/O and view refinement checking were implemented as a verification tool named VRYD (VerifYing concurrent programs by Runtime Refinement-violation Detection). VYRD was applied to the verification of Boxwood, Java class libraries, and, previously, to the Scan filesystem. It was able to detect previously unnoticed subtle concurrency bugs in Boxwood and the Scan file system, and the known bugs in the Java class libraries and manually constructed examples. Experimental results indicate that our techniques have modest computational cost.
Path slicing
Authors: Jhala Ranjit , Majumdar Rupak
Published: November 2005

We present a new technique,
path slicing
, that takes as input a possibly infeasible path to a target location, and eliminates all the operations that are irrelevant towards the reachability of the target location. A path slice is a subsequence of the original path whose infeasibility guarantees the infeasibility of the original path, and whose feasibility guarantees the existence of some feasible variant of the given path that reaches the target location even though the given path may itself be infeasible. Our method combines the ability of program slicing to look at several program paths, with the precision that dynamic slicing enjoys by focusing on a single path. We have implemented Path Slicing to analyze possible counterexamples returned by the software model checker
Blast
. We show its effectiveness in drastically reducing the size of the counterexamples to less than 1% of their original size. This enables the precise verification of application programs (upto 100KLOC), by allowing the analysis to focus on the part of the counterexample that is relevant to the property being checked.
Register allocation for software pipelined multi-dimensional loops
Authors: Rong Hongbo , Douillet Alban , Gao Guang R.
Published: November 2005

Software pipelining of a multi-dimensional loop is an important optimization that overlaps the execution of successive outermost loop iterations to explore instruction-level parallelism from the entire n-dimensional iteration space. This paper investigates register allocation for software pipelined multi-dimensional loops.For single loop software pipelining, the lifetime instances of a loop variant in successive iterations of the loop form a repetitive pattern. An effective register allocation method is to represent the pattern as a vector of lifetimes (or a
vector lifetime
using Rau's terminology) and map it to rotating registers. Unfortunately, the software pipelined schedule of a multi-dimensional loop is considerably more complex, and so are the vector lifetimes in it.In this paper, we develop a way to normalize and represent vector lifetimes in multi-dimensional loop software pipelining, which capture their complexity, while exposing their regularity that enables us to develop a simple, yet powerful solution. Our algorithm is based on the development of a metric, called
distance
, that quantitatively determines the degree of potential overlapping (conflicts) between two vector lifetimes. We show how to calculate and use the distance, conservatively or aggressively, to guide the register allocation of the vector lifetimes under a bin-packing algorithm framework. The classical register allocation for software pipelined single loops is subsumed by our method as a special case.The method has been implemented in the ORC compiler and produced code for the Itanium architecture. We report the effectiveness of our method on 134 loop nests with 348 loop levels. Several strategies for register allocation are compared and analyzed.
Pin
Authors: Luk Chi-Keung , Cohn Robert , Muth Robert , Patil Harish , Klauser Artur , Lowney Geoff , Wallace Steven , Reddi Vijay Janapa , Hazelwood Kim
Published: November 2005

Robust and powerful software instrumentation tools are essential for program analysis tasks such as profiling, performance evaluation, and bug detection. To meet this need, we have developed a new instrumentation system called
Pin
. Our goals are to provide
easy-to-use, portable, transparent
, and
efficient
instrumentation. Instrumentation tools (called
Pintools
) are written in C/C++ using Pin's rich API. Pin follows the model of ATOM, allowing the tool writer to analyze an application at the instruction level without the need for detailed knowledge of the underlying instruction set. The API is designed to be
architecture independent
whenever possible, making Pintools source compatible across different architectures. However, a Pintool can access architecture-specific details when necessary. Instrumentation with Pin is mostly
transparent
as the application and Pintool observe the application's original, uninstrumented behavior. Pin uses
dynamic compilation
to instrument executables while they are running. For efficiency, Pin uses several techniques, including inlining, register re-allocation, liveness analysis, and instruction scheduling to optimize instrumentation. This fully automated approach delivers significantly better instrumentation performance than similar tools. For example, Pin is 3.3x faster than Valgrind and 2x faster than DynamoRIO for basic-block counting. To illustrate Pin's versatility, we describe two Pintools in daily use to analyze production software. Pin is publicly available for Linux platforms on four architectures: IA32 (32-bit x86), EM64T (64-bit x86), Itanium®, and ARM. In the ten months since Pin 2 was released in July 2004, there have been over 3000 downloads from its website.
TraceBack
Authors: Ayers Andrew , Schooler Richard , Metcalf Chris , Agarwal Anant , Rhee Junghwan , Witchel Emmett
Published: November 2005

Faults that occur in production systems are the most important faults to fix, but most production systems lack the debugging facilities present in development environments. TraceBack provides debugging information for production systems by providing execution history data about program problems (such as crashes, hangs, and exceptions). TraceBack supports features commonly found in production environments such as multiple threads, dynamically loaded modules, multiple source languages (e.g., Java applications running with JNI modules written in C++), and distributed execution across multiple computers. TraceBack supports
first fault diagnosis
-discovering what went wrong the first time a fault is encountered. The user can see how the program reached the fault state without having to re-run the computation; in effect enabling a limited form of a debugger in production code.TraceBack uses static, binary program analysis to inject low-overhead runtime instrumentation at control-flow block granularity. Post-facto reconstruction of the records written by the instrumentation code produces a source-statement trace for user diagnosis. The trace shows the dynamic instruction sequence leading up to the fault state, even when the program took exceptions or terminated abruptly (e.g., kill -9).We have implemented TraceBack on a variety of architectures and operating systems, and present examples from a variety of platforms. Performance overhead is variable, from 5% for Apache running SPECweb99, to 16%-25% for the Java SPECJbb benchmark, to 60% average for SPECint2000. We show examples of TraceBack's cross-language and cross-machine abilities, and report its use in diagnosing problems in production software.
Programming by sketching for bit-streaming programs
Authors: Solar-Lezama Armando , Rabbah Rodric , Bodík Rastislav , Ebcioğlu Kemal
Published: November 2005

This paper introduces the concept of
programming with sketches
, an approach for the rapid development of high-performance applications. This approach allows a programmer to write clean and portable reference code, and then obtain a high-quality implementation by simply
sketching
the outlines of the desired implementation. Subsequently, a compiler automatically fills in the missing details while also ensuring that a completed sketch is faithful to the input reference code. In this paper, we develop StreamBit as a sketching methodology for the important class of bit-streaming programs (e.g., coding and cryptography).A sketch is a
partial
specification of the implementation, and as such, it affords several benefits to programmer in terms of productivity and code robustness. First, a sketch is easier to write compared to a complete implementation. Second, sketching allows the programmer to focus on exploiting algorithmic properties rather than on orchestrating low-level details. Third, a sketch-aware compiler rejects "buggy" sketches, thus improving reliability while allowing the programmer to quickly evaluate sophisticated implementation ideas.We evaluated the productivity and performance benefits of our programming methodology in a user-study, where a group of novice StreamBit programmers competed with a group of experienced C programmers on implementing a cipher. We learned that, given the same time budget, the ciphers developed in StreamBit ran 2.5x faster than ciphers coded in C. We also produced implementations of DES and Serpent that were competitive with hand optimized implementations available in the public domain.
Formal loop merging for signal transforms
Authors: Franchetti Franz , Voronenko Yevgen , Püschel Markus
Published: November 2005

A critical optimization in the domain of linear signal transforms, such as the discrete Fourier transform (DFT), is loop merging, which increases data locality and reuse and thus performance. In particular, this includes the conversion of shuffle operations into array reindexings. To date, loop merging is well understood only for the DFT, and only for Cooley-Tukey FFT based algorithms, which excludes DFT sizes divisible by large primes. In this paper, we present a formal loop merging framework for general signal transforms and its implementation within the SPIRAL code generator. The framework consists of Ε-SPL, a mathematical language to express loops and index mappings; a rewriting system to merge loops in Ε-SPL and a compiler that translates Ε-SPL into code. We apply the framework to DFT sizes that cannot be handled using only the Cooley-Tukey FFT and compare our method to FFTW 3.0.1 and the vendor library Intel MKL 7.2.1. Compared to FFTW our generated code is a factor of 2--4 faster under equal implementation conditions (same algorithms, same unrolling threshold). For some sizes we show a speed-up of a factor of 9 using Bluestein's algorithm. Further, we give a detailed comparison against the Intel vendor library MKL; our generated code is between 2 times faster and 4.5 times slower.
Nonintrusive precision instrumentation of microcontroller software
Authors: Titzer Ben L. , Palsberg Jens
Published: November 2005

Debugging, testing, and profiling microcontroller programs are notoriously difficult. The lack of supporting software such as an operating system, a narrow interface to the hardware chip, and delicately timed sequences of code present significant challenges which can be exacerbated by the presence of additional debugging or profiling code. In this paper we present a solution to the precision instrumentation problem for microcontroller code that is based upon our open, flexible simulator framework, Avrora. Our simulator preserves all timing and behavior of the instrumented program while allowing precision measurement of application-specific quantities.
ACME
Authors: Cooper Keith D. , Grosul Alexander , Harvey Timothy J. , Reeves Steven , Subramanian Devika , Torczon Linda , Waterman Todd
Published: November 2005

Research over the past five years has shown significant performance improvements using a technique called
adaptive compilation
. An adaptive compiler uses a compile-execute-analyze feedback loop to find the combination of optimizations and parameters that minimizes some performance goal, such as code size or execution time.Despite its ability to improve performance, adaptive compilation has not seen widespread use because of two obstacles: the large amounts of time that such systems have used to perform the many compilations and executions prohibits most users from adopting these systems, and the complexity inherent in a feedback-driven adaptive system has made it difficult to build and hard to use.A significant portion of the adaptive compilation process is devoted to multiple executions of the code being compiled. We have developed a technique called
virtual execution
to address this problem. Virtual execution runs the program a single time and preserves information that allows us to accurately predict the performance of different optimization sequences without running the code again. Our prototype implementation of this technique significantly reduces the time required by our adaptive compiler.In conjunction with this performance boost, we have developed a graphical-user interface (GUI) that provides a controlled view of the compilation process. By providing appropriate defaults, the interface limits the amount of information that the user must provide to get started. At the same time, it lets the experienced user exert fine-grained control over the parameters that control the system.
On the design of the local variable cache in a hardware translation-based java virtual machine
Authors: Oi Hitoshi
Published: November 2005

Hardware bytecode translation is a technique to improve the performance of the Java Virtual Machine (JVM), especially on the portable devices for which dynamic compilation is infeasible. However, since the translation is done on a single bytecode basis, it is likely to generate frequent memory accesses for local variables which can be a performance bottleneck.In this paper, we propose to add a small register file to the datapath of the hardware-translation based JVM and use it as a local variable cache. We evaluate the effectiveness of the local variable cache against the size of the local variable cache which determines the chip area overhead and the operating speed. We also discuss the mechanisms for the efficient parameter passing and the on-the-fly profiling.With two types of exceptions, a 16-entry local variable cache achieved hit ratios of 60 to 98%. The first type of exceptions is represented by the FFT, which accesses more than 16 local variables. In this case, on-the-fly profiling was effective. The hit ratio of 16-entry cache for the FFT was increased from 44 to 83%. The second type of exception is represented by the SAXON XSLT processor for which cold misses were significant. The proposed parameter passing mechanism turned 6.4 to 13.3% of total accesses from miss to hit to the local variable cache.
A dictionary construction technique for code compression systems with echo instructions
Authors: Brisk Philip , Macbeth Jamie , Nahapetian Ani , Sarrafzadeh Majid
Published: November 2005

Dictionary compression
mechanisms identify redundant sequences of instructions that occur in a program. The sequences are extracted and copied to a dictionary. Each sequence is then replaced with a codeword that acts as an index into the dictionary, thereby enabling decompression of the program at runtime. The problem of optimally organizing a dictionary consisting solely of redundant sequences in order to maximize compression has long been known to be NP-Complete [23]. This paper addresses the problem of dictionary construction when redundant code fragments are represented as
Data Flow Graphs
(
DFGs
) rather than linear sequences of instructions. Since there are generally multiple legal schedules for a given DFG
G
, a compiler must determine a schedule for G so that other DFGs that are subgraphs of
G
can reference some substring of
G
's final code sequence. This reduces the size of the dictionary, and in turn, the size of the compressed program. Our experiments with 10 MediaBench [18] applications yielded reductions in dictionary size ranging from 21.14% to 29.76% compared to a naïve approach.
Complementing software pipelining with software thread integration
Authors: So Won , Dean Alexander G.
Published: November 2005

Software pipelining is a critical optimization for producing efficient code for VLIW/EPIC and superscalar processors in high-performance embedded applications such as digital signal processing. Software thread integration (STI) can often improve the performance of looping code in cases where software pipelining performs poorly or fails. This paper examines both situations, presenting methods to determine what and when to integrate.We evaluate our methods on C-language image and digital signal processing libraries and synthetic loop kernels. We compile them for a very long instruction word (VLIW) digital signal processor (DSP) -- the Texas Instruments (TI) C64x architecture. Loops which benefit little from software pipelining (SWP-Poor) speed up by 26% (harmonic mean, HM). Loops for which software pipelining fails (SWP-Fail) due to conditionals and calls speed up by 16% (HM). Combining SWP-Good and SWP-Poor loops leads to a speedup of 55% (HM).
A sample-based cache mapping scheme
Authors: Xu Rong , Li Zhiyuan
Published: November 2005

Applications running on the StrongARM SA-1110 or XScale processor cores can specify cache mapping for each virtual page to achieve better cache utilization. In this work, we describe a method to efficiently perform cache mapping. Under this scheme, we select a number of loops for sampling. These loops are selected automatically based on clock profiling information. We formulate the optimal cache mapping problem as an Integer Linear Programming (ILP) problem. Experiments performed on 14 test programs show speedups in 13 of them (over the default mapping) after applying our sample-based cache mapping scheme. The geometric mean of program speedups for all the 14 test programs is 1.098. Furthermore, compared with a previous heuristic method which uses the full memory trace, the sample-based method performs cache mapping faster by an order of magnitude without sacrificing the quality of mapping.
Upper bound for defragmenting buddy heaps
Authors: Defoe Delvin C. , Cholleti Sharath R. , Cytron Ron K.
Published: November 2005

Knuth's buddy system is an attractive algorithm for managing storage allocation, and it can be made to operate in real-time. At some point, storage-management systems must either over-provide storage or else confront the issue of defragmentation. Because storage conservation is important to embedded systems, we investigate the issue of defragmentation for heaps that are managed by the buddy system. In this paper, we present tight bounds for the amount of storage necessary to avoid defragmentation. These bounds turn out to be too high for embedded systems, so defragmentation becomes necessary.We then present an algorithm for defragmenting buddy heaps and present experiments from applying that algorithm to real and synthetic benchmarks. Our algorithm relocates less than twice the space relocated by an optimal algorithm to defragment the heap so as to respond to a single allocation request. Our experiments show our algorithm to be much more efficient than extant defragmentation algorithms.
Realization of multimethods in single dispatch object oriented languages
Authors: Kumar Rajeev , Agrawal Vikram , Mangolia Anil
Published: November 2005

The need for multimethods is preeminent in the domain of object-oriented programming. However, multimethods are far from universally acknowledged. Commonly used languages - C++, Java & C# - are single dispatching languages. In this paper, we demonstrate the alternatives for multimethods in such languages. The techniques discussed, in this paper, include double dispatching (a well known technique), technique of message dispatching using RTTI (explored in detail by us in this paper), and reflection (a feature provided by some compilers). We implement these techniques for C++, Java and C# languages and discuss issues associated with encapsulating multimethods in single dispatch languages. We also compare techniques in terms of their efficiency, ease of (re)use and type safety.
The specification language
T
Authors: Sunik Boris
Published: November 2005

The non-executable language

T

belongs to the class of open languages initially defined in [Sunik 1,2]. Open languages are artificial human languages with the grammar of OO programming languages. Similar to a natural language, an open language is not confined to any particular representation domain and may be applied in any tasks requiring explicit informing.

T

can be used for producing OO specifications of various entities representing software, hardware, technical appliances, biology systems, knowledge representation systems, etc. It also allows explicit representation of semantics of programming languages and produces executable code compliant with the semantics represented.
Towards a simpler method of operational semantics for language definition
Authors: Derk M. D.
Published: November 2005

One of the needs of the computer science community is a simple, clear and generally accepted method of defining programming language semantics. Towards this end, the author presents a new approach to operational semantics based on binding, which is dubbed relational semantics. By grouping bound elements in tuples, the primary language functions are defined in a clear and concise manner. Relational semantics may be used together with BNF for a more complete yet simple language definition tool.
Z
0
- a tiny experimental language
Authors: Greiner Saso , Rebernak Damijan , Brest Janez , Zumer Viljem
Published: November 2005

Z
0
is a tiny experimental class-based pure object-oriented programming language. Its key features include syntactic simplicity, similarity with Java [8], strong static typing, pure object abstraction, and some dynamic mechanism which are normally only found in dynamic languages.
Z
0
provides a unified, object-oriented treatment of all values, primitive, user-defined, and even control structures. In a nutshell, everything is an object. As far as object "purity" is concerned,
Z
0
looks to Smalltalk [6] and Self [20,17].
Z
0
uses a clean and strict method-based model. There are no explicit instance variables, only methods. A dynamic, compile-time checkable method update mechanism is provided to make methods manipulable at run time. Inheritance model is simple and straightforward. Variant type system and dynamic typing with Self enable a high degree of typing flexibility that is statically safe and can be efficiently implemented. Because
Z
0
is compiled for a virtual machine (JVM-like [13]), it is much more efficient in execution than interpreted languages.
Generative programming for C#
Authors: Draheim Dirk , Lutteroth Christof , Weber Gerald
Published: November 2005

This article describes how we extended the C# language by new constructs that provide means for generative programming. Those constructs make it possible to handle problems like the generation of user interfaces and certain crosscutting concerns in a less error prone and elegant way without affecting the overall language integrity.
Witnessing side-effects
Authors: Terauchi Tachio , Aiken Alex
Published: November 2005

We present a new approach to the old problem of adding side effects to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a static checking algorithm that makes use of a network flow property equivalent to the semantic condition.
High-level views on low-level representations
Authors: Diatchki Iavor S. , Jones Mark P. , Leslie Rebekah
Published: November 2005

This paper explains how the high-level treatment of datatypes in functional languages—using features like constructor functions and pattern matching—can be made to coexist with
bitdata
. We use this term to describe the bit- level representations of data that are required in the construction of many different applications, including operating systems, device drivers, and assemblers. We explain our approach as a combination of two language extensions, each of which could potentially be adapted to any modern functional language. The first adds simple and elegant constructs for
manipulating
raw bitfield values, while the second provides a view-like mechanism for defining distinct new bitdata types with fine-control over the underlying
representation
. Our design leverages polymorphic type inference, as well as techniques for improvement of qualified types, to track both the type and the width of bitdata structures. We have implemented our extensions in a small functional language interpreter, and used it to show that our approach can handle a wide range of practical bitdata types.
Associated type synonyms
Authors: Chakravarty Manuel M. T. , Keller Gabriele , Jones Simon Peyton
Published: November 2005

Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, they express the programmer's intent somewhat indirectly. Developing earlier work on
associated data types
, we propose to add functionally dependent types as type synonyms to type-class bodies. These
associated type synonyms
constitute an interesting new alternative to explicit functional dependencies.