bluuebunny/crossref_metadata_2025 huggingface dataset:
Static specification inference using predicate mining
Authors: Ramanathan Murali Krishna , Grama Ananth , Jagannathan Suresh
Published: September 2007

The reliability and correctness of complex software systems can be significantly enhanced through well-defined specifications that dictate the use of various units of abstraction (e.g., modules, or procedures). Often times, however, specifications are either missing, imprecise, or simply too complex to encode within a signature, necessitating specification inference. The process of inferring specifications from complex software systems forms the focus of this paper. We describe a static inference mechanism for identifying the preconditions that must hold whenever a procedure is called. These preconditions may reflect both data flow properties (e.g., whenever
p
is called, variable
x
must be non-null) as well as control-flow properties (e.g., every call to
p
must bepreceded by a call to
q
). We derive these preconditions using a ninter-procedural path-sensitive dataflow analysis that gathers predicates at each program point. We apply mining techniques to these predicates to make specification inference robust to errors. This technique also allows us to derive higher-level specifications that abstract structural similarities among predicates (e.g., procedure
p
is called immediately after a conditional test that checks whether some variable
v
is non-null.) We describe an implementation of these techniques, and validate the effectiveness of the approach on a number of large open-source benchmarks. Experimental results confirm that our mining algorithms are efficient, and that the specifications derived are both precise and useful-the implementation discovers several critical, yet previously, undocumented preconditions for well-tested libraries.
Automatic inference of optimizer flow functions from semantic meanings
Authors: Scherpelz Erika Rice , Lerner Sorin , Chambers Craig
Published: September 2007

Previous work presented a language called Rhodium for writing program analyses and transformations, in the form of declarative flow functions that propagate instances of user-defined dataflow fact schemas. Each dataflow fact schema specifies a semantic meaning, which allows the Rhodium system to automatically verify the correctness of the user's flow functions. In this work, we have reversed the roles of the flow functions and semantic meanings: rather than
checking
the correctness of the user-written flow functions using the facts' semantic meanings, we automatically
infer
correct flow functions solely from the meanings of the dataflow fact schemas. We have implemented our algorithm for inferring flow functions from fact schemas in the context of the Whirlwind compiler, and have used this implementation to infer flow functions for a variety of fact schemas. The automatically generated flow functions cover most of the situations covered by an earlier suite of handwritten rules.
EXOCHI
Authors: Wang Perry H. , Collins Jamison D. , Chinya Gautham N. , Jiang Hong , Tian Xinmin , Girkar Milind , Yang Nick Y. , Lueh Guei-Yuan , Wang Hong
Published: September 2007

Future mainstream microprocessors will likely integrate specialized accelerators, such as GPUs, onto a single die to achieve better performance and power efficiency. However, it remains a keen challenge to program such a heterogeneous multicore platform, since these specialized accelerators feature ISAs and functionality that are significantly different from the general purpose CPU cores. In this paper, we present EXOCHI: (1)
Exoskeleton Sequencer
(EXO), an architecture to represent heterogeneous acceleratorsas ISA-based MIMD architecture resources, and a shared virtual memory heterogeneous multithreaded program execution model that tightly couples specialized accelerator cores with generalpurpose CPU cores, and (2)
C for Heterogeneous Integration
(CHI), an integrated C/C++ programming environment that supports accelerator-specific inline assembly and domain-specific languages. The CHI compiler extends the OpenMP pragma for heterogeneous multithreading programming, and produces a single fat binary with code sections corresponding to different instruction sets. The runtime can judiciously spread parallel computation across the heterogeneous cores to optimize performance and power.

We have prototyped the EXO architecture on a physical heterogeneous platform consisting of an Intel® Core™ 2 Duo processor and an 8-core 32-thread Intel® Graphics Media Accelerator X3000. In addition, we have implemented the CHI integrated programming environment with the Intel® C++ Compiler, runtime toolset, and debugger. On the EXO prototype system, we have enhanced a suite of production-quality media kernels for video and image processing to utilize the accelerator through the CHI programming interface, achieving significant speedup (1.41X to10.97X) over execution on the IA32 CPU alone.
Goldilocks
Authors: Elmas Tayfun , Qadeer Shaz , Tasiran Serdar
Published: September 2007

Data races often result in unexpected and erroneous behavior. In addition to causing data corruption and leading programs to crash, the presence of data races complicates the semantics of an execution which might no longer be sequentially consistent. Motivated by these observations, we have designed and implemented a Java runtime system that monitors program executions and throws a DataRaceException when a data race is about to occur. Analogous to other runtime exceptions, the DataRaceException provides two key benefits. First, accesses causing race conditions are interruptedand handled before they cause errors that may be difficult to diagnose later. Second, if no DataRaceException is thrown in an execution, it is guaranteed to be sequentially consistent. This strong guarantee helps to rule out many concurrency-related possibilities as the cause of erroneous behavior. When a DataRaceException is caught, the operation, thread, or program causing it can be terminated gracefully. Alternatively, the DataRaceException can serve as a conflict-detection mechanism inoptimistic uses of concurrency.

We start with the definition of data-race-free executions in the Java memory model. We generalize this definition to executions that use transactions in addition to locks and volatile variables for synchronization. We present a precise and efficient algorithm for dynamically verifying that an execution is free of data races. This algorithm generalizes the Goldilocks algorithm for data-race detectionby handling transactions and providing the ability to distinguish between read and write accesses. We have implemented our algorithm and the DataRaceException in the Kaffe Java Virtual Machine. We have evaluated our system on a variety of publicly available Java benchmarks and a few microbenchmarks that combine lock-based and transaction-based synchronization. Our experiments indicate that our implementation has reasonable overhead. Therefore, we believe that inaddition to being a debugging tool, the DataRaceException may be a viable mechanism to enforce the safety of executions of multithreaded Java programs.
Shape analysis with inductive recursion synthesis
Authors: Guo Bolei , Vachharajani Neil , August David I.
Published: September 2007

Separation logic with recursively defined predicates allows for concise yet precise description of the shapes of data structures. However, most uses of separation logic for program analysis rely on pre-defined recursive predicates, limiting the class of programs analyzable to those that manipulate only a priori data structures. This paper describes a general algorithm based on
inductive program synthesis
that automatically infers recursive shape invariants, yielding a shape analysis based on separation logic that can be applied to any program.

A key strength of separation logic is that it facilitates, via explicit expression of structural separation, local reasoning about heap where the effects of altering one part of a data structure are analyzed in isolation from the rest. The interaction between local reasoning and the global invariants given by recursive predicates is a difficult area, especially in the presence of complex internal sharing in the data structures. Existing approaches, using logic rules specifically designed for the list predicate to unfold and fold linked-lists, again require a priori knowledge about the shapes of the data structures and do not easily generalize to more complex data structures. We introduce a notion of "truncation points" in a recursive predicate, which gives rise to generic algorithms for unfolding and folding arbitrary data structures.
Thread-modular shape analysis
Authors: Gotsman Alexey , Berdine Josh , Cook Byron , Sagiv Mooly
Published: September 2007

We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.
Path invariants
Authors: Beyer Dirk , Henzinger Thomas A. , Majumdar Rupak , Rybalchenko Andrey
Published: September 2007

The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm -the
spurious counterexample
- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such
path programs
as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs-so-called
path invariants
. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.
DITTO
Authors: Shankar Ajeet , Bodík Rastislav
Published: September 2007

We present DITTO, an automatic incrementalizer for dynamic, side-effect-free data structure invariant checks. Incrementalization speeds up the execution of a check by reusing its previous executions, checking the invariant anew only the changed parts of the data structure. DITTO exploits properties specific to the domain of invariant checks to automate and simplify the process without restricting what mutations the program can perform. Our incrementalizer works for modern imperative languages such as Java and C#. It can incrementalize,for example, verification of red-black tree properties and the consistency of the hash code in a hash table bucket. Our source-to-source implementation for Java is automatic, portable, and efficient. DITTO provides speedups on data structures with as few as 100 elements; on larger data structures, its speedups are characteristic of non-automatic incrementalizers: roughly 5-fold at 5,000 elements,and growing linearly with data structure size.
Regularly annotated set constraints
Authors: Kodumal John , Aiken Alex
Published: September 2007

A general class of program analyses area combination of context-free and regular language reachability. We define
regularly annotated set constraints
, a constraint formalism that captures this class. Our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.
UCC
Authors: Li Weijia , Zhang Youtao , Yang Jun , Zheng Jiang
Published: September 2007

Wireless sensor networks (WSN), composed of a large number of low-cost, battery-powered sensors, have recently emerged as promising computing platforms for many non-traditional applications. The preloaded code on remote sensors often needs to be updated after deployment in order for the WSN to adapt to the changing demands from the users. Post-deployment code dissemination is challenging as the data are transmitted via battery-powered wireless communication. Recent studies show that the energy for sending a single bit is about the same as executing 1000 instructions in aWSN. Therefore it is important to achieve energy efficiency in code dissemination.

In this paper, we propose novel
update-conscious compilation(UCC)
techniques for energy-efficient code dissemination in WSNs. An update-conscious compiler, when compiling the modified code, includes the compilation decisions that were made when generating the old binary. The compiler employs a detailed energy model and strives to match the old decisions for a more energy-efficient result. In most cases, matching the previous decisions improves the binary code similarity, reduces the amount of data to be transmitted to remote sensors, and thus, consumes less energy. In this paper, we develop update-conscious register allocation and data layout algorithms. Our experimental results show that they can achieve great improvements over the traditional, update-oblivious approaches.
Profile-driven energy reduction in network-on-chips
Authors: Li Feihui , Chen Guangyu , Kandemir Mahmut , Kolcu Ibrahim
Published: September 2007

Reducing energy consumption of a Network-on-Chip (NoC) is a critical design goal, especially for power-constrained embedded systems.In response, prior research has proposed several circuit/architectural level mechanisms to reduce NoC power consumption. This paper considers the problem from a different perspective and demonstrates that compiler analysis can be very helpful for enhancing the effectiveness of a hardware-based link power management mechanism by increasing the duration of communication links' idle periods. The proposed profile-based approach achieves its goal by maximizing the communication link reuse through compiler-directed, static message re-routing. That is, it clusters the required data communications into a small set of communication links at any given time, which increases the idle periods for the remaining communication links in the network. This helps hardware shut down more communication links and their corresponding buffers to reduce leakage power. The current experimental evaluation, with twelve data-intensive embedded applications, shows that the proposed profile-driven compiler approach reduces leakage energy by more than 35% (on average) as compared to a pure hardware-based link power management scheme.
Parameterized tiled loops for free
Authors: Renganarayanan Lakshminarayanan , Kim DaeGon , Rajopadhye Sanjay , Strout Michelle Mills
Published: September 2007

Parameterized tiled loops-where the tile sizes are not fixed at compile time, but remain symbolic parameters until later--are quite useful for iterative compilers and "auto-tuners" that produce highly optimized libraries and codes. Tile size parameterization could also enable optimizations such as register tiling to become dynamic optimizations. Although it is easy to generate such loops for (hyper) rectangular iteration spaces tiled with (hyper) rectangular tiles, many important computations do not fall into this restricted domain. Parameterized tile code generation for the general case of convex iteration spaces being tiled by (hyper) rectangular tiles has in the past been solved with bounding box approaches or symbolic Fourier Motzkin approaches. However, both approaches have less than ideal code generation efficiency and resulting code quality. We present the theoretical foundations, implementation, and experimental validation of a simple, unified technique for generating parameterized tiled code. Our code generation efficiency is comparable to all existing code generation techniques including those for fixed tile sizes, and the resulting code is as efficient as, if not more than, all previous techniques. Thus the technique provides parameterized tiled loops for free! Our "one-size-fits-all" solution, which is available as open source software can be adapted for use in production compilers.
Towards locating execution omission errors
Authors: Zhang Xiangyu , Tallam Sriraman , Gupta Neelam , Gupta Rajiv
Published: September 2007

Execution omission errors are known to be difficult to locate using dynamic analysis. These errors lead to a failure at runtime because of the omission of execution of some statements that would have been executed if the program had no errors. Since dynamic analysis is typically designed to focus on dynamic information arising from executed statements, and statements whose execution is omitted do not produce dynamic information, detection of execution omission errors becomes a challenging task. For example, while dynamic slices are very effective in capturing faulty code for other types of errors, they fail to capture faulty code in presence of execution omission errors. To address this issue relevant slices have been defined to consider certain static dependences (called potential dependences) in addition to dynamic dependences. However, due to the conservative nature of static analysis, overly large slices are produced. In this paper, we propose a
fully dynamic
solution to locating execution omission errors using dynamic slices. We introduce the notion of
implicit dependences
which are dependences that are normally invisible to dynamic slicing due to the omission of execution of some statements. We design a dynamic method that forces the execution of the omitted code by switching outcomes of relevant predicates such that those implicit dependences are exposed and become available for dynamic slicing. Dynamic slices can be computed and effectively pruned to produce fault candidate sets containing the execution omission errors. We solve two main problems: verifying the existence of a single implicit dependence through predicate switching, and recovering the implicit dependences in a demand driven manner such that a small number of verifications are required before the root cause is captured. Our experiments show that the proposed technique is highly effective in capturing execution omission errors.
Searching for type-error messages
Authors: Lerner Benjamin S. , Flower Matthew , Grossman Dan , Chambers Craig
Published: September 2007

Advanced type systems often need some form of type inference to reduce the burden of explicit typing, but type inference often leads to poor error messages for ill-typed programs. This work pursues a new approach to constructing compilers and presenting type-error messages in which the type-checker itself does not produce the messages. Instead, it is an oracle for a search procedure that finds similar programs that do type-check. Our two-fold goal is to improve error messages while simplifying compiler construction. Our primary implementation and evaluation is for Caml, a language with full type inference. We also present a prototype for C++ template functions, where type instantiation is implicit. A key extension is making our approach robust even when the program has multiple independent type errors.
Iterative context bounding for systematic testing of multithreaded programs
Authors: Musuvathi Madanlal , Qadeer Shaz
Published: September 2007

Multithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the development cycle and post-deployment. Model checking or systematic exploration of program behavior is a promising alternative to traditional testing methods. However, it is difficult to perform systematic search on large programs as the number of possible program behaviors grows exponentially with the program size. Confronted with this state-explosion problem, traditional model checkers perform iterative depth-bounded search. Although effective for message-passing software, iterative depth-bounding is inadequate for multithreaded software.

This paper proposes iterative context-bounding, a new search algorithm that systematically explores the executions of a multithreaded program in an order that prioritizes executions with fewer
context switches
. We distinguish between preempting and nonpreempting context switches, and show that bounding the number of preempting context switches to a small number significantly alleviates the state explosion, without limiting the depth of explored executions. We show both theoretically and empirically that context-bounded search is an effective method for exploring the behaviors of multithreaded programs. We have implemented our algorithmin two model checkers and applied it to a number of real-world multithreaded programs. Our implementation uncovered 9 previously unknown bugs in our benchmarks, each of which was exposed by an execution with at most 2 preempting context switches. Our initial experience with the technique is encouraging and demonstrates that iterative context-bounding is a significant improvement over existing techniques for testing multithreaded programs.
CGCExplorer
Authors: Vechev Martin T. , Yahav Eran , Bacon David F. , Rinetzky Noam
Published: September 2007

Concurrent garbage collectors are notoriously hard to design, implement, and verify. We present a framework for the automatic exploration of a space of concurrent mark-and-sweep collectors. In our framework, the designer specifies a set of "building blocks" from which algorithms can be constructed. These blocks reflect the designer's insights about the coordination between the collector and the mutator. Given a set of building blocks, our framework automatically explores a space of algorithms, using model checking with abstraction to verify algorithms in the space.

We capture the intuition behind some common mark-and-sweep algorithms using a set of building blocks. We utilize our framework to automatically explore a space of more than 1,600,000 algorithms built from these blocks, and derive over 100 correct fine-grained algorithms with various space, synchronization, and precision tradeoffs.
A general framework for certifying garbage collectors and their mutators
Authors: McCreight Andrew , Shao Zhong , Lin Chunxiao , Li Long
Published: September 2007

Garbage-collected languages such as Java and C# are becoming more and more widely used in both high-end software and real-time embedded applications. The correctness of the GC implementation is essential to the reliability and security of a large portion of the world's mission-critical software. Unfortunately, garbage collectors--especially incremental and concurrent ones--are extremely hard to implement correctly. In this paper, we present a new uniform approach to verifying the safety of both a mutator and its garbage collector in Hoare-style logic. We define a formal garbage collector interface general enough to reason about a variety of algorithms while allowing the mutator to ignore implementation-specific details of the collector. Our approach supports collectors that require read and write barriers. We have used our approach to mechanically verify assembly implementations of mark-sweep, copying and incremental copying GCs in Coq, as well as sample mutator programs that can be linked with any of the GCs to produce a fully-verified garbage-collected program. Our work provides a foundation for reasoning about complex mutator-collector interaction and makes an important advance toward building fully certified production-quality GCs.
Practical memory leak detection using guarded value-flow analysis
Authors: Cherem Sigmund , Princehouse Lonnie , Rugina Radu
Published: September 2007

This paper presents a practical inter-procedural analysis algorithm for detecting memory leaks in C programs. Our algorithm tracks the flow of values from allocation points to deallocation points using a sparse representation of the program consisting of a value flow graph that captures def-use relations and value flows via program assignments. Edges in the graph are annotated with guards that describe branch conditions in the program. The memory leak analysis is reduced to a reachability problem over the guarded value flowgraph. Our implemented tool has been effective at detecting more than 60 memory leaks in the SPEC2000 benchmarks and in two open-source applications, bash and sshd, while keeping the false positive rate below 20%. The sparse program representation makes the tool efficient in practice, and allows it to report concise error messages.
A type system for preventing data races and deadlocks in the java virtual machine language
Authors: Permandla Pratibha , Roberson Michael , Boyapati Chandrasekhar
Published: September 2007

In previous work on SafeJava we presented a type system extension to the Java source language that statically prevents data races and deadlocks in multithreaded programs. SafeJava is expressive enough to support common programming patterns, its type checking is fast and scalable, and it requires little programming overhead. SafeJava thus offers a promising approach for making multithreaded programs more reliable. This paper presents a corresponding type system extension for the Java virtual machine language (JVML). We call the resulting language SafeJVML. Well-typed SafeJVML programs are guaranteed to be free of data races and deadlocks. Designing a corresponding type system for JVML is important because most Java code is shipped in the JVML format. Designing acorresponding type system for JVML is nontrivial because of important differences between Java and JVML. In particular, the absence of block structure in JVML programs and the fact that they do not use named local variables the way Java programs do make the type systems for Java and JVML significantly different. For example, verifying absence of races and deadlocks in JVML programs requires performing an alias analysis, something that was not necessary for verifying absence of races and deadlocks in Java programs. This paper presents static and dynamic semantics for Safe JVML. It also includes a proof that the SafeJVML type system is sound and that it prevents data races and deadlocks. To the best of our knowledge, this is the first type system for JVML that statically ensures absence of synchronization errors.
Automated fault localization with statistically suspicious program states
Authors: Huang Tai-Yi , Chou Pin-Chuan , Tsai Cheng-Han , Chen Hsin-An
Published: September 2007

A number of fault localization techniques have been developed to reduce the time in manually debugging a faulty program. The technique of code coverage [8] has been recognized by its effectiveness in identifying suspicious statements that may contain the fault. However, a programmer still needs to manually examine each variable referenced in a suspicious statement and such a process can become extremely time-consuming if this suspicious statement is part of a loop. In this paper, we propose a novel technique called state coverage to significantly reduce the time in examining variables. We first insert a set of checkpoints to record the state of each variable referenced in a branching statement. We next execute the faulty program by a test suite consisting of both passed and failed cases. A state is statistically considered to be more suspicious if it appears more in failed cases and less in passed cases. We implemented both code coverage and state coverage in a debugging tool and used a commonly-used benchmark consisting of 58 faulty programs to evaluate their performance. For 34% of these programs, their faults are within 20 statement steps of the most suspicious statement identified by code coverage. By adding state coverage and breaking at the most suspicious state, we increase this ratio to 64%, an 88% performance improvement. Finally, we also explain a few cases in which both state coverage and code coverage cannot perform well.
Frequency-aware energy optimization for real-time periodic and aperiodic tasks
Authors: Zhong Xiliang , Xu Cheng-Zhong
Published: September 2007

Energy efficiency is an important factor in embedded systems design. We consider an embedded system with a dynamic voltage scaling (DVS) capable processor and its system-wide power consumption is dominated by the processor and memory. We present speed assignment polices for a set of periodic/aperiodic tasks that minimize the overall system energy consumption including active and idle power of CPU and other components. A limitation of most DVS-based system-wide energy optimization techniques is that they assume the number of worst-case execution cycles (WCEC) of a task is a constant, independent of CPU frequency. This is not the case when other system components such as memory are taken into account. In this paper, we decompose task execution time into two parts: on-chip inside CPU and off-chip outside the CPU. We propose a frequency-aware system-wide energy minimization approach and establish necessary and sufficient conditions for the optimality. By exploiting properties of the conditions, we derive a bisection algorithm that finds the optimal solution to offline periodict asks in a linear time complexity. We apply a similar analytical approach to online aperiodic tasks scheduling and devise an iterative speed assignment algorithm in the complexity of
O
(
n
2
). We prove it is optimal among all online algorithms without assumptions about future task releases.
DVSleak
Authors: Zhu Yifan , Mueller Frank
Published: September 2007

Recent trends in CMOS fabrication have the demand to conserve power of processors. While dynamic voltage scaling (DVS) is effective in reducing dynamic power, microprocessors produced in ever smaller fabrication processes are increasingly dominated bystatic power. For such processors, voltage/frequency pairs below acritical speed result in higher energy per cycle than entering a processor sleep mode. Yet, computational demand above this critical speed is best met by DVS techniques while still conserving power.

We develop a novel combined leakage and DVS scheduling algorithm forreal-time systems, DVS leak, based on earliest-deadline-first scheduling (EDF). Our method trades off DVS with leakage, where the former slows down execution while the latter intelligently defers dispatching of jobs when sleeping is beneficial. We further capitalize on feedback knowledge about actual execution times to anticipate computational demands without sacrificing deadline guarantees. As such, we contribute a novel feedback delay policy for leakage awareness, which addresses structural limitations of prior approaches. Experiments show that this combined DVS/leakage algorithm results in an average of (a) 50% additional energy savings over a leakage-oblivious DVS algorithm, (b) 20% more energy savings over a more simplistic combination of DVS and sleep policies and (c) 8.5% or more over dynamic slack reclamation with procrastination. Particularly task sets with periods shorter than ten milliseconds profit from our approach with 15% energy savings over best prior schemes. This makes DVS leak the best combined DVS/leakage regulation approach for real-time systems that we know of.
Bee+Cl@k
Authors: Alias Christophe , Baray Fabrice , Darte Alain
Published: September 2007

We build on prior work on intra-array memory reuse, for which a general theoretical framework was proposed based on lattice theory. Intra-array memory reuse is a way of reducing the size of a temporary array by folding, thanks to affine mappings and modulo operations, reusing memory locations when they contain a value not used later. We describe the algorithms needed to implement such a strategy. Our implementation has two parts. The first part, Bee, uses the source-to-source transformer ROSE to extract from the program all necessary information on the lifetime of array elements and to generate the code after memory reduction. The second part, Cl@k, is a stand-alone mathematical tool dedicated to optimizations on polyhedra, in particular the computation of successive minima and the computation of good admissible lattices, which are the basis for lattice-based memory reuse. Both tools are developed in C++ and use linear programming and polyhedra manipulations. They can be used either for embedded program optimizations, e.g., to limit memory expansion introduced for parallelization, or in high-level synthesis, e.g., to design memories between communicating hardware accelerators.
On the complexity of spill everywhere under SSA form
Authors: Bouchez Florent , Darte Alain , Rastello Fabrice
Published: September 2007

Compilation for embedded processors can be either aggressive (time consuming cross-compilation) or just in time (embedded and usually dynamic). The heuristics used in dynamic compilation are highly constrained by limited resources, time and memory in particular. Recent results on the SSA form open promising directions for the design of new register allocation heuristics for embedded systems and especially for embedded compilation. In particular, heuristics based on tree scan with two separated phases -- one for spilling, then one for coloring/coalescing -- seem good candidates for designing memory-friendly, fast, and competitive register allocators. Still, also because of the side effect on power consumption, the minimization of loads and stores overhead (spilling problem) is an important issue. This paper provides an exhaustive study of the complexity of the "spill everywhere" problem in the context of the SSA form. Unfortunately, conversely to our initial hopes, many of the questions we raised lead to NP-completeness results. We identify some polynomial cases but that are impractical in JIT context. Nevertheless, they can give hints to simplify formulations for the design of aggressive allocators.
Issues and challenges in compiling for the CBEA
Authors: O'Brien Kathryn
Published: September 2007

It has been demonstrated that expert programmers can develop and hand tune applications to exploit the full performance potential of the CBE architecture. We believe that sophisticated compiler optimization technology can bridge the gap between usability and performance in this arena. To this end we have developed a research prototype compiler targeting the Cell processor.

In this talk we describe a variety of compiler techniques to exploit the Cell processor. These techniques are aimed at automatically generating high quality codes for the heterogeneous parallelism available on the Cell processor. In particular we will focus the discussion on managing the small local memories of the SPEs and discuss our approach to presenting the user with a single shared memory image through our compiler controlled software cache. We will also report and discuss the results we have achieved to date, which indicate that significant speedup can be achieved on this processor with a high level of support from the compiler.
Automatic generation of embedded communication SW for heterogeneous MPSoC platforms
Authors: Viskic Ines , Abdi Samar , Gajski Daniel D.
Published: September 2007

This paper addresses the problem of long design cycle of MPSoCs communication SW with automatic synthesis. The tool we propose takes as input a transaction level model (TLM) of MPSoC communication and outputs pin and cycle-accurate (PCA) bus drivers that can be linked to the synthesizable PCA model (PCAM).

The TL communication is simple since TLM channels abstract away protocol details. PCAM communication, in turn, includes explicit definitions for each signal and pin. However, in most cases the TLMs are not suitable for implementation since they do not reflect the MPSoC platform. Usually the designers simulate (fast) TLMs, then manually implement PCA communication.

Our communication SW synthesis transforms TL send and receive functions into platform specific PCAM bus drivers which can be automatically downloaded to the FPGA board. The presented results demonstrate the significant productivity gain achieved with our tool, with no great cost to either code size or system performance.
Enabling compiler flow for embedded VLIW DSP processors with distributed register files
Authors: Chen Chung-Kai , Tseng Ling-Hua , Chen Shih-Chang , Lin Young-Jia , You Yi-Ping , Lu Chia-Han , Lee Jenq-Kuen
Published: September 2007

High-performance and low-power VLIW DSP processors are increasingly deployed on embedded devices to process video and multimedia applications. For reducing power and cost in designs of VLIW DSP processors, distributed register files and multi-bank register architectures are being adopted to eliminate the amount of read/write ports in register files. This presents new challenges for devising compiler optimization schemes for such architectures. In this paper, we address the compiler optimization issues for PAC architecture, which is a 5-way issue DSP processor with distributed register files. We present an integrated flow to address several phases of compiler optimizations in interacting with distributed register files and multi-bank register files in the layer of instruction scheduling, software pipelining, and data flow optimizations. Our experiments on a novel 32-bit embedded VLIW DSP (known as the PAC DSP core) exhibit the state of the art performance for embedded VLIW DSP processors with distributed register files by incorporating our proposed schemes in compilers.
Compiler-directed application mapping for NoC based chip multiprocessors
Authors: Chen Guangyu , Li Feihui , Kandemir Mahmut
Published: September 2007

The problem attacked in this paper is one of automatically mapping an application onto a Network-on-Chip (NoC) based chip multi-processor architecture in a locality-aware fashion. The proposed compiler approach has four major steps: task scheduling, processor mapping, data mapping, and packet routing. Our experimental result clearly shows that the proposed framework reduces energy consumption of our applications significantly (27.41% on average over a pure performance oriented application mapping strategy) as a result of improved locality of data accesses.
Addressing instruction fetch bottlenecks by using an instruction register file
Authors: Hines Stephen Roderick , Tyson Gary , Whalley David
Published: September 2007

The Instruction Register File (IRF) is an architectural extension for providing improved access to frequently occurring instructions. An optimizing compiler can exploit an IRF by packing an application's instructions, resulting in decreased code size, reduced energy consumption and improved execution time primarily due to a smaller footprint in the instruction cache. The nature of the IRF also allows the execution of packed instructions to overlap with instruction fetch, thus providing a means for tolerating increased fetch latencies, like those experienced by encrypted ICs as well as the presence of low-power L0 caches. Although previous research has focused on the direct benefits of instruction packing, this paper explores the use of increased fetch bandwidth provided by packed instructions. Small L0 caches improve energy efficiency but can increase execution time due to frequent cache misses. We show that this penalty can be significantly reduced by overlapping the execution of packed instructions with miss stalls. The IRF can also be used to supply additional instructions to a more aggressive execution engine, effectively reducing dependence on instruction cache bandwidth. This can improve energy efficiency, in addition to providing additional flexibility for evaluating various design tradeoffs in a pipeline with asymmetric instruction bandwidth. Thus, we show that the IRF is a complementary technique, operating as a buffer tolerating fetch bottlenecks, as well as providing additional fetch bandwidth for an aggressive pipeline backend.
Dynamic data scratchpad memory management for a memory subsystem with an MMU
Authors: Cho Hyungmin , Egger Bernhard , Lee Jaejin , Shin Heonshik
Published: September 2007

In this paper, we propose a dynamic scratchpad memory (SPM)management technique for a horizontally-partitioned memory subsystem with an MMU. The memory subsystem consists of a relatively cheap direct-mapped data cache and SPM. Our technique loads required global data and stack pages into the SPM on demand when a function is called. A scratchpad memory managerloads/unloads the data pages and maintains a page table for the MMU. Our approach is based on post-pass analysis and optimization techniques, and it handles the whole program including libraries. The data page mapping is determined by solving an integer linear programming (ILP) formulation that approximates our demand paging technique. The ILP model uses a dynamic call graph annotated with the number of memory accesses and/or cache misses obtained by profiling. We evaluate our technique on thirteen embedded applications. We compare the results to a reference system with a 4-way set associative data cache and the ideal case with the same 4-way cache and SPM, where all global and stack data is placed in the SPM. On average, our approach reduces the total system energy consumption by 8.1% with no performance degradation. This is equivalent to exploiting 60% of the room available in energy reduction between the reference case and the ideal case.
Optimizing software cache performance of packet processing applications
Authors: Wang Qin , Chen Junpu , Zhang Weihua , Yang Min , Zang Binyu
Published: September 2007

Network processors (NPs) are widely used in many types of networking equipment due to their high performance and flexibility. For most NPs, software cache is used instead of hardware cache due to the chip area, cost and power constraints. Therefore, programmers should take full responsibility for software cache management which is neither intuitive nor easy to most of them. Actually, without an effective use of it, long memory access latency will be a critical limiting factor to overall applications. Prior researches like hardware multi-threading, wide-word accesses and packet access combination for caching have already been applied to help programmers to overcome this bottleneck. However, most of them do not make enough use of the characteristics of packet processing applications and often perform intraprocedural optimizations only. As a result, the binary codes generated by those techniques often get lower performance than that comes from hand-tuned assembly programming for some applications. In this paper, we propose an algorithm including two techniques - Critical Path Based Analysis (CPBA) and Global Adaptive Localization (GAL), to optimize the software cache performance of packet processing applications. Packet processing applications usually have several hot paths and CPBA tries to insert localization instructions according to their execution frequencies. For further optimizations, GAL eliminates some redundant localization instructions by interprocedural analysis and optimizations. Our algorithm is applied on some representative applications. Experiment results show that it leads to an average speedup by a factor of 1.974.
On compact routing for the internet
Authors: Krioukov Dmitri , claffy k c , Fall Kevin , Brady Arthur
Published: September 2007

The Internet's routing system is facing stresses due to its poor fundamental scaling properties. Compact routing is a research field that studies fundamental limits of routing scalability and designs algorithms that try to meet these limits. In particular, compact routing research shows that shortest-path routing, forming a core of traditional routing algorithms, cannot guarantee routing table (RT) sizes that on all network topologies grow slower than linearly as functions of the network size. However, there are plenty of compact routing schemes that relax the shortest-path requirement and allow for improved, sublinear RT size scaling that is mathematically provable for all static network topologies. In particular, there exist compact routing schemes designed for grids, trees, and Internet-like topologies that offer RT sizes that scale logarithmically with the network size.

In this paper, we demonstrate that in view of recent results in compact routing research, such logarithmic scaling on Internet-like topologies is fundamentally impossible in the presence of topology dynamics or topology-independent (flat) addressing. We use analytic arguments to show that the number of routing control messages per topology change cannot scale better than linearly on Internet-like topologies. We also employ simulations to confirm that logarithmic RT size scaling gets broken by topology-independent addressing, a cornerstone of popular locator-identifier split proposals aiming at improving routing scaling in the presence of network topology dynamics or host mobility. These pessimistic findings lead us to the conclusion that a fundamental re-examination of assumptions behind routing models and abstractions is needed in order to find a routing architecture that would be able to scale "indefinitely.
Don't optimize existing protocols, design optimizable protocols
Authors: He Jiayue , Rexford Jennifer , Chiang Mung
Published: September 2007

As networks grow in size and complexity, network management has become an increasingly challenging task. Many protocols have tunable parameters, and optimization is the process of setting these parameters to optimize an objective. In recent years, optimization techniques have been widely applied to network management problems, albeit with mixed success. Realizing that optimization problems in network management are induced by assumptions adopted in protocol design, we argue that instead of optimizing existing protocols, protocols should be designed with optimization in mind from the beginning. Using examples from our past research on traffic management, we present principles that guide how changes to existing protocols and architectures can lead to optimizable protocols. We also discuss the trade-offs between making network optimization easier and the overhead these changes impose.
Internet clean-slate design
Authors: Feldmann Anja
Published: September 2007

Many believe that it is impossible to resolve the challenges facing today's Internet without rethinking the fundamental assumptions and design decisions underlying its current architecture. Therefore, a major research effort has been initiated on the topic of Clean Slate Design of the Internet's architecture. In this paper we first give an overview of the challenges that a future Internet has to address and then discuss approaches for finding possible solutions, including Clean Slate Design. Next, we discuss how such solutions can be evaluated and how they can be retrofitted into the current Internet. Then, we briefly outline the upcoming research activities both in Europe and the U. S. Finally, we end with a perspective on how network and service operators may benefit from such an initiative.