bluuebunny/crossref_metadata_2025 huggingface dataset:
TAS-MRAM-Based Low-Power High-Speed Runtime Reconfiguration (RTR) FPGA
Authors: Zhao Weisheng , Belhaire Eric , Chappert Claude , Dieny Bernard , Prenat Guillaume
Published: June 2009

As one of the most promising Spintronics applications, MRAM combines the advantages of high writing and reading speed, limitless endurance, and nonvolatility. The integration of MRAM in FPGAs allows the logic circuit to rapidly configure the algorithm, the routing and logic functions, and easily realize the Runtime Reconfiguration (RTR) and multicontext configuration. However, the conventional MRAM technology based on the Field Induced Magnetic Switching (FIMS) writing approach consumes very high power, large circuit surfaces, and produces high disturbance between memory cells. These drawbacks prevent FIMS-MRAM’s further development in memory and logic circuit. Thermally Assisted Switching (TAS)-based MRAM is then evaluated to address these issues. In this article, some design techniques, novel computing architecture, and logic components for FPGA logic circuits based on TAS-MRAM technology are presented. By using STMicroelectronics CMOS 90nm technology and a complete TAS-MTJ spice model, some chip characteristic results such as the programming latency (~25ns) and power dissipation (~124pJ) have been calculated or simulated to demonstrate the expected performance of TAS-MRAM-based FPGA logic circuits.
Self-Measurement of Combinatorial Circuit Delays in FPGAs
Authors: Wong Justin S. J. , Sedcole Pete , Cheung Peter Y. K.
Published: June 2009

This article proposes a Built-In Self-Test (BIST) method to accurately measure the combinatorial circuit delays on an FPGA. The flexibility of the on-chip clock generation capability found in modern FPGAs is employed to step through a range of frequencies until timing failure in the combinatorial circuit is detected. In this way, the delay of any combinatorial circuit can be determined with a timing resolution of the order of picoseconds. Parallel and optimized implementations of the method for self-characterization of the delay of all the LUTs on an FPGA are also proposed. The method was applied to Altera Cyclone II and III FPGAs . A complete self-characterization of LUTs on a Cyclone II was achieved in 2.5 seconds, utilizing only 13kbit of block RAM to store the results. More extensive tests were carried out on the Cyclone III and the delays of adder circuits and embedded multiplier blocks were successfully measured. This self-measurement method paves the way for matching timing requirements in designs to FPGAs as a means of combating the problem of process variations.
Field Programmable Compressor Trees
Authors: Cevrero Alessandro , Athanasopoulos Panagiotis , Parandeh-Afshar Hadi , Verma Ajay K. , Niaki Hosein Seyed Attarzadeh , Nicopoulos Chrysostomos , Gurkaynak Frank K. , Brisk Philip , Leblebici Yusuf , Ienne Paolo
Published: June 2009

Multi-input addition occurs in a variety of arithmetically intensive signal processing applications. The DSP blocks embedded in high-performance FPGAs perform fixed bitwidth parallel multiplication and Multiply-ACcumulate (MAC) operations. In theory, the compressor trees contained within the multipliers could implement multi-input addition; however, they are not exposed to the programmer. To improve FPGA performance for these applications, this article introduces the Field Programmable Compressor Tree (FPCT) as an alternative to the DSP blocks. By providing just a compressor tree, the FPCT can perform multi-input addition along with parallel multiplication and MAC in conjunction with a small amount of FPGA general logic. Furthermore, the user can configure the FPCT to precisely match the bitwidths of the operands being summed. Although an FPCT cannot beat the performance of a well-designed ASIC compressor tree of fixed bitwidth, for example, 9×9 and 18×18-bit multipliers/MACs in DSP blocks, its configurable bitwidth and ability to perform multi-input addition is ideal for reconfigurable devices that are used across a variety of applications.
WireMap
Authors: Jang Stephen , Chan Billy , Chung Kevin , Mishchenko Alan
Published: June 2009

This article presents a new technology mapper, WireMap. The mapper uses an
edge flow
heuristic to improve the routability of a mapped design. The heuristic is applied during the iterative mapping optimization to reduce the total number of pin-to-pin connections (or edges). On academic benchmark (ISCAS, MCNC, and ITC designs), the average edge reduction of 9.3% is achieved while maintaining depth and LUT count compared to state-of-the-art technology mapping. Placing and routing the resulting netlists leads to an 8.5% reduction in the total wirelength, a 6.0% reduction in minimum channel width, and a 2.3% reduction in critical path delay. This technique is applied in the Xilinx ISE Design tool to evaluate its effect on industrial Virtex5 circuits. In a set of 20 large designs, we find the edge reduction is 6.8% while total wirelength measured in the placer is reduced by 3.6%. Applying WireMap has an additional advantage of reducing an average number of inputs of LUTs without increasing the total LUT count and depth. The percentages of 5- and 6-LUTs in a typical design are reduced, while the percentages of 2-, 3-, and 4-LUTs are increased. These smaller LUTs can be merged into pairs and implemented using the dual-output LUT structure found in commercial FPGAs. For academic benchmarks, WireMap leads to 9.4% fewer dual-output LUTs after merging. For the industrial designs, WireMap leads to 6.3% fewer dual-output Virtex5 LUTs.
ProtoFlex
Authors: Chung Eric S. , Papamichael Michael K. , Nurvitadhi Eriko , Hoe James C. , Mai Ken , Falsafi Babak
Published: June 2009

Functional full-system simulators are powerful and versatile research tools for accelerating architectural exploration and advanced software development. Their main shortcoming is limited throughput when simulating large multiprocessor systems with hundreds or thousands of processors or when instrumentation is introduced. We propose theProtoFlexsimulation architecture, which uses FPGAs to accelerate full-system multiprocessor simulation and to facilitate high-performance instrumentation. Prior FPGA approaches that prototype a complete system in hardware are either too complex when scaling to large-scale configurations or require significant effort to provide full-system support. In contrast,ProtoFlexvirtualizes the execution of many logical processors onto a consolidated number of multiple-context execution engines on the FPGA. Through virtualization, the number of engines can be judiciously scaled, as needed, to deliver on necessary simulation performance at a large savings in complexity. Further, to achieve low-complexity full-system support, a hybrid simulation technique called transplanting allows implementing in the FPGA only the frequently encountered behaviors, while a software simulator preserves the abstraction of a complete system.

We have created a first instance of theProtoFlexsimulation architecture, which is an FPGA-based, full-system functional simulator for a 16-way UltraSPARC III symmetric multiprocessor server, hosted on a single Xilinx Virtex-II XCV2P70 FPGA. On average, the simulator achieves a 38x speedup (and as high as 49×) over comparable software simulation across a suite of applications, including OLTP on a commercial database server. We also demonstrate the advantages of minimal-overhead FPGA-accelerated instrumentation through a CMP cache simulation technique that runs orders-of-magnitude faster than software.
Dynamic software updates
Authors: Subramanian Suriya , Hicks Michael , McKinley Kathryn S.
Published: June 2009

Software evolves to fix bugs and add features. Stopping and restarting programs to apply changes is inconvenient and often costly. Dynamic software updating (DSU) addresses this problem by updating programs while they execute, but existing DSU systems for managed languages do not support many updates that occur in practice and are inefficient. This paper presents the design and implementation of J
volve
, a DSU-enhanced Java VM. Updated programs may add, delete, and replace fields and methods anywhere within the class hierarchy. Jvolve implements these updates by adding to and coordinating VM classloading, just-in-time compilation, scheduling, return barriers, on-stack replacement, and garbage collection. J
volve
, is
safe
: its use of bytecode verification and VM thread synchronization ensures that an update will always produce type-correct executions. Jvolve is
flexible
: it can support 20 of 22 updates to three open-source programs--Jetty web server, JavaEmailServer, and CrossFTP server--based on actual releases occurring over 1 to 2 years. Jvolve is
efficient
: performance experiments show that incurs
no overhead
during steady-state execution. These results demonstrate that this work is a significant step towards practical support for dynamic updates in virtual machines for managed languages.
Safe and timely updates to multi-threaded programs
Authors: Neamtiu Iulian , Hicks Michael
Published: June 2009

Many dynamic updating systems have been developed that enable a program to be patched while it runs, to fix bugs or add new features. This paper explores techniques for supporting dynamic updates to multi-threaded programs, focusing on the problem of applying an update in a timely fashion while still producing correct behavior. Past work has shown that this tension of
safety
versus timeliness can be balanced for single-threaded programs. For multi-threaded programs, the task is more difficult because myriad thread interactions complicate understanding the possible program states to which a patch could be applied. Our approach allows the programmer to specify a few program points (e.g., one per thread) at which a patch may be applied, which simplifies reasoning about safety. To improve timeliness, a combination of static analysis and run-time support automatically expands these few points to many more that produce behavior equivalent to the originals. Experiments with thirteen realistic updates to three multi-threaded servers show that we can safely perform a dynamic update within milliseconds when more straightforward alternatives would delay some updates indefinitely.
PetaBricks
Authors: Ansel Jason , Chan Cy , Wong Yee Lok , Olszewski Marek , Zhao Qin , Edelman Alan , Amarasinghe Saman
Published: June 2009

It is often impossible to obtain a one-size-fits-all solution for high performance algorithms when considering different choices for data distributions, parallelism, transformations, and blocking. The best solution to these choices is often tightly coupled to different architectures, problem sizes, data, and available system resources. In some cases, completely different algorithms may provide the best performance. Current compiler and programming language techniques are able to change some of these parameters, but today there is no simple way for the programmer to express or the compiler to choose different algorithms to handle different parts of the data. Existing solutions normally can handle only coarse-grained, library level selections or hand coded cutoffs between base cases and recursive cases.

We present PetaBricks, a new implicitly parallel language and compiler where having multiple implementations of multiple algorithms to solve a problem is the natural way of programming. We make algorithmic choice a first class construct of the language. Choices are provided in a way that also allows our compiler to tune at a finer granularity. The PetaBricks compiler autotunes programs by making both fine-grained as well as algorithmic choices. Choices also include different automatic parallelization techniques, data distributions, algorithmic parameters, transformations, and blocking.

Additionally, we introduce novel techniques to autotune algorithms for different convergence criteria. When choosing between various direct and iterative methods, the PetaBricks compiler is able to tune a program in such a way that delivers near-optimal efficiency for any desired level of accuracy. The compiler has the flexibility of utilizing different convergence criteria for the various components within a single algorithm, providing the user with accuracy choice alongside algorithmic choice.
Staged information flow for javascript
Authors: Chugh Ravi , Meister Jeffrey A. , Jhala Ranjit , Lerner Sorin
Published: June 2009

Modern websites are powered by JavaScript, a flexible dynamic scripting language that executes in client browsers. A common paradigm in such websites is to include third-party JavaScript code in the form of libraries or advertisements. If this code were malicious, it could read sensitive information from the page or write to the location bar, thus redirecting the user to a malicious page, from which the entire machine could be compromised. We present an information-flow based approach for inferring the effects that a piece of JavaScript has on the website in order to ensure that key security properties are not violated. To handle dynamically loaded and generated JavaScript, we propose a framework for staging information flow properties. Our framework propagates information flow through the currently known code in order to compute a minimal set of syntactic residual checks that are performed on the remaining code when it is dynamically loaded. We have implemented a prototype framework for staging information flow. We describe our techniques for handling some difficult features of JavaScript and evaluate our system's performance on a variety of large real-world websites. Our experiments show that static information flow is feasible and efficient for JavaScript, and that our technique allows the enforcement of information-flow policies with almost no run-time overhead.
Merlin
Authors: Livshits Benjamin , Nori Aditya V. , Rajamani Sriram K. , Banerjee Anindya
Published: June 2009

The last several years have seen a proliferation of static and runtime analysis tools for finding security violations that are caused by
explicit information flow
in programs. Much of this interest has been caused by the increase in the number of vulnerabilities such as cross-site scripting and SQL injection. In fact, these explicit information flow vulnerabilities commonly found in Web applications now outnumber vulnerabilities such as buffer overruns common in type-unsafe languages such as C and C++. Tools checking for these vulnerabilities require a specification to operate. In most cases the task of providing such a specification is delegated to the user. Moreover, the efficacy of these tools is only as good as the specification. Unfortunately, writing a comprehensive specification presents a major challenge: parts of the specification are easy to miss, leading to missed vulnerabilities; similarly, incorrect specifications may lead to false positives.

This paper proposes Merlin, a new approach for automatically inferring explicit information flow specifications from program code. Such specifications greatly reduce manual labor, and enhance the quality of results, while using tools that check for security violations caused by explicit information flow. Beginning with a data propagation graph, which represents interprocedural flow of information in the program, Merlin aims to automatically infer an information flow specification. Merlin models information flow paths in the propagation graph using probabilistic constraints. A naive modeling requires an exponential number of constraints, one per path in the propagation graph. For scalability, we approximate these path constraints using constraints on chosen triples of nodes, resulting in a cubic number of constraints. We characterize this approximation as a probabilistic abstraction, using the theory of probabilistic refinement developed by McIver and Morgan. We solve the resulting system of probabilistic constraints using factor graphs, which are a well-known structure for performing probabilistic inference.

We experimentally validate the Merlin approach by applying it to 10 large business-critical Web applications that have been analyzed with CAT.NET, a state-of-the-art static analysis tool for .NET. We find a total of 167 new confirmed specifications, which result in a total of 322
additional
vulnerabilities across the 10 benchmarks. More accurate specifications also reduce the false positive rate: in our experiments, Merlin-inferred specifications result in 13 false positives being removed; this constitutes a 15% reduction in the CAT.NET false positive rate on these 10 programs. The final false positive rate for CAT.NET after applying Merlin in our experiments drops to under 1%.
Stretching transactional memory
Authors: Dragojević Aleksandar , Guerraoui Rachid , Kapalka Michal
Published: June 2009

Transactional memory (TM) is an appealing abstraction for programming multi-core systems. Potential target applications for TM, such as business software and video games, are likely to involve complex data structures and large transactions, requiring specific software solutions (STM). So far, however, STMs have been mainly evaluated and optimized for smaller scale benchmarks.

We revisit the main STM design choices from the perspective of complex workloads and propose a new STM, which we call SwissTM. In short, SwissTM is lock- and word-based and uses (1) optimistic (commit-time) conflict detection for read/write conflicts and pessimistic (encounter-time) conflict detection for write/write conflicts, as well as (2) a new two-phase contention manager that ensures the progress of long transactions while inducing no overhead on short ones. SwissTM outperforms state-of-the-art STM implementations, namely RSTM, TL2, and TinySTM, in our experiments on STMBench7, STAMP, Lee-TM and red-black tree benchmarks.

Beyond SwissTM, we present the most complete evaluation to date of the individual impact of various STM design choices on the ability to support the mixed workloads of large applications.
A decision procedure for subset constraints over regular languages
Authors: Hooimeijer Pieter , Weimer Westley
Published: June 2009

Reasoning about string variables, in particular program inputs, is an important aspect of many program analyses and testing frameworks. Program inputs invariably arrive as strings, and are often manipulated using high-level string operations such as equality checks, regular expression matching, and string concatenation. It is difficult to reason about these operations because they are not well-integrated into current constraint solvers.

We present a decision procedure that solves systems of equations over regular language variables. Given such a system of constraints, our algorithm finds satisfying assignments for the variables in the system. We define this problem formally and render a mechanized correctness proof of the core of the algorithm. We evaluate its scalability and practical utility by applying it to the problem of automatically finding inputs that cause SQL injection vulnerabilities.
Program verification using templates over predicate abstraction
Authors: Srivastava Saurabh , Gulwani Sumit
Published: June 2009

We address the problem of automatically generating invariants with quantified and boolean structure for proving the validity of given assertions or generating pre-conditions under which the assertions are valid. We present three novel algorithms, having different strengths, that combine template and predicate abstraction based formalisms to discover required sophisticated program invariants using SMT solvers.

Two of these algorithms use an iterative approach to compute fixed-points (one computes a least fixed-point and the other computes a greatest fixed-point), while the third algorithm uses a constraint based approach to encode the fixed-point. The key idea in all these algorithms is to reduce the problem of invariant discovery to that of finding
optimal
solutions for unknowns (over conjunctions of some predicates from a given set) in a template formula such that the formula is valid.

Preliminary experiments using our implementation of these algorithms show encouraging results over a benchmark of small but complicated programs. Our algorithms can verify program properties that, to our knowledge, have not been automatically verified before. In particular, our algorithms can generate full correctness proofs for sorting algorithms (which requires nested universally-existentially quantified invariants) and can also generate preconditions required to establish worst-case upper bounds of sorting algorithms. Furthermore, for the case of previously considered properties, in particular sortedness in sorting algorithms, our algorithms take less time than reported by previous techniques.
GC assertions
Authors: Aftandilian Edward E. , Guyer Samuel Z.
Published: June 2009

This paper introduces
GC assertions
, a system interface that programmers can use to check for errors, such as data structure invariant violations, and to diagnose performance problems, such as memory leaks. GC assertions are checked by the garbage collector, which is in a unique position to gather information and answer questions about the lifetime and connectivity of objects in the heap. By piggybacking on existing garbage collector computations, our system is able to check heap properties with very low overhead -- around 3% of total execution time -- low enough for use in a deployed setting.

We introduce several kinds of GC assertions and describe how they are implemented in the collector. We also describe our reporting mechanism, which provides a complete path through the heap to the offending objects. We report results on both the performance of our system and the experience of using our assertions to find and repair errors in real-world programs.
Implementation of the memory-safe full ANSI-C compiler
Authors: Oiwa Yutaka
Published: June 2009

This paper describes a completely memory-safe compiler for C language programs that is fully compatible with the ANSI C specification.

Programs written in C often suffer from nasty errors due to dangling pointers and buffer overflow. Such errors in Internet server programs are often exploited by malicious attackers to crack an entire system. The origin of these errors is usually corruption of in-memory data structures caused by out-of-bound array accesses. Usual C compilers do not provide any protection against such out-of-bound access, although many other languages such as Java and ML do provide such protection. There have been several proposals for preventing such memory corruption from various aspects: runtime buffer overrun detectors, designs for new C-like languages, and compilers for (subsets of) the C language. However, as far as we know, none of them have achieved full memory protection and full compatibility with the C language specification at the same time.

We propose the most powerful solution to this problem ever presented. We have developed
Fail-Safe C
, a memory-safe implementation of the full ANSI C language. It detects and disallows all unsafe operations, yet conforms to the full ANSI C standard (including casts and unions). This paper introduces several techniques--both compile-time and runtime--to reduce the overhead of runtime checks, while still maintaining 100% memory safety. This compiler lets programmers easily make their programs safe without heavy rewriting or porting of their code. It also supports many of the "dirty tricks" commonly used in many existing C programs, which do not strictly conform to the standard specification. In this paper, we demonstrate several real-world server programs that can be processed by our compiler and present technical details and benchmark results for it.
Error propagation analysis for file systems
Authors: Rubio-González Cindy , Gunawi Haryadi S. , Liblit Ben , Arpaci-Dusseau Remzi H. , Arpaci-Dusseau Andrea C.
Published: June 2009

Unchecked errors are especially pernicious in operating system file management code. Transient or permanent hardware failures are inevitable, and error-management bugs at the file system layer can cause silent, unrecoverable data corruption. We propose an interprocedural static analysis that tracks errors as they propagate through file system code. Our implementation detects overwritten, out-of-scope, and unsaved unchecked errors. Analysis of four widely-used Linux file system implementations (CIFS, ext3, IBM JFS and ReiserFS), a relatively new file system implementation (ext4), and shared virtual file system (VFS) code uncovers 312 error propagation bugs. Our flow- and context-sensitive approach produces more precise results than related techniques while providing better diagnostic information, including possible execution paths that demonstrate each bug found.
Sharing classes between families
Authors: Qi Xin , Myers Andrew C.
Published: June 2009

Class sharing is a new language mechanism for building extensible software systems. Recent work has separately explored two different kinds of extensibility: first, family inheritance, in which an entire family of related classes can be inherited, and second, adaptation, in which existing objects are extended in place with new behavior and state. Class sharing integrates these two kinds of extensibility mechanisms. With little programmer effort, objects of one family can be used as members of another, while preserving relationships among objects. Therefore, a family of classes can be adapted in place with new functionality spanning multiple classes. Object graphs can evolve from one family to another, adding or removing functionality even at run time.

Several new mechanisms support this flexibility while ensuring type safety. Class sharing has been implemented as an extension to Java, and its utility for evolving and extending software is demonstrated with realistic systems.
Typed self-representation
Authors: Rendel Tillmann , Ostermann Klaus , Hofer Christian
Published: June 2009

Self-representation -- the ability to represent programs in their own language -- has important applications in reflective languages and many other domains of programming language design. Although approaches to designing typed program representations for sublanguages of some base language have become quite popular recently, the question whether a fully metacircular typed self-representation is possible is still open. This paper makes a big step towards this aim by defining the F
ω
* calculus, an extension of the higher-order polymorphic lambda calculus F
ω
that allows typed self-representations. While the usability of these representations for metaprogramming is still limited, we believe that our approach makes a significant step towards a new generation of reflective languages that are both safe and efficient.
Type-based data structure verification
Authors: Kawaguchi Ming , Rondon Patrick , Jhala Ranjit
Published: June 2009

We present a refinement type-based approach for the static verification of complex data structure invariants. Our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and trees), and maps (e.g., arrays and hash tables). We introduce two novel type-based mechanisms targeted towards these elements: recursive refinements and polymorphic refinements. These mechanisms automate the challenging work of generalizing and instantiating rich universal invariants by piggybacking simple refinement predicates on top of types, and carefully dividing the labor of analysis between the type system and an SMT solver. Further, the mechanisms permit the use of the abstract interpretation framework of liquid type inference to automatically synthesize complex invariants from simple logical qualifiers, thereby almost completely automating the verification. We have implemented our approach in
dsolve
, which uses liquid types to verify
ocaml
programs. We present experiments that show that our type-based approach reduces the manual annotation required to verify complex properties like sortedness, balancedness, binary-search-ordering, and acyclicity by more than an order of magnitude.
Proving optimizations correct using parameterized program equivalence
Authors: Kundu Sudipta , Tatlock Zachary , Lerner Sorin
Published: June 2009

Translation validation is a technique for checking that, after an optimization has run, the input and output of the optimization are equivalent. Traditionally, translation validation has been used to prove concrete, fully specified programs equivalent. In this paper we present Parameterized Equivalence Checking (PEC), a generalization of translation validation that can prove the equivalence of parameterized programs. A parameterized program is a partially specified program that can represent multiple concrete programs. For example, a parameterized program may contain a section of code whose only known property is that it does not modify certain variables. By proving parameterized programs equivalent, PEC can prove the correctness of transformation rules that represent complex optimizations once and for all, before they are ever run. We implemented our PEC technique in a tool that can establish the equivalence of two parameterized programs. To highlight the power of PEC, we designed a language for implementing complex optimizations using many-to-many rewrite rules, and used this language to implement a variety of optimizations including software pipelining, loop unrolling, loop unswitching, loop interchange, and loop fusion. Finally, to demonstrate the effectiveness of PEC, we used our PEC implementation to verify that all the optimizations we implemented in our language preserve program behavior.
An integrated proof language for imperative programs
Authors: Zee Karen , Kuncak Viktor , Rinard Martin C.
Published: June 2009

We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge generated proof obligations. It is designed to 1) enable developers to resolve key choice points in complex program correctness proofs, thereby enabling automated reasoning systems to successfully prove the desired correctness properties; 2) allow developers to identify key lemmas for the reasoning systems to prove, thereby guiding the reasoning systems to find an effective proof decomposition; 3) enable multiple reasoning systems to work together productively to prove a single correctness property by providing a mechanism that developers can use to divide the property into lemmas, each of which is suitable for a different reasoning system; and 4) enable developers to identify specific lemmas that the reasoning systems should use when attempting to prove other lemmas or correctness properties, thereby appropriately confining the search space so that the reasoning systems can find a proof in an acceptable amount of time.

The language includes a rich set of declarative proof constructs that enables developers to direct the reasoning systems as little or as much as they desire. Because the declarative proof statements are embedded into the program as specialized comments, they also serve as verified documentation and are a natural extension of the assertion mechanism found in most program verification systems.

We have implemented our integrated proof language in the context of a program verification system for Java and used the resulting system to verify a collection of linked data structure implementations. Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems.
Automatic generation of library bindings using static analysis
Authors: Ravitch Tristan , Jackson Steve , Aderhold Eric , Liblit Ben
Published: June 2009

High-level languages are growing in popularity. However, decades of C software development have produced large libraries of fast, time-tested, meritorious code that are impractical to recreate from scratch. Cross-language bindings can expose low-level C code to high-level languages. Unfortunately, writing bindings by hand is tedious and error-prone, while mainstream binding generators require extensive manual annotation or fail to offer the language features that users of modern languages have come to expect.

We present an improved binding-generation strategy based on static analysis of unannotated library source code. We characterize three high-level idioms that are not uniquely expressible in C's low-level type system: array parameters, resource managers, and multiple return values. We describe a suite of interprocedural analyses that recover this high-level information, and we show how the results can be used in a binding generator for the Python programming language. In experiments with four large C libraries, we find that our approach avoids the mistakes characteristic of hand-written bindings while offering a level of Python integration unmatched by prior automated approaches. Among the thousands of functions in the public interfaces of these libraries, roughly 40% exhibit the behaviors detected by our static analyses.
Efficiently and precisely locating memory leaks and bloat
Authors: Novark Gene , Berger Emery D. , Zorn Benjamin G.
Published: June 2009

Inefficient use of memory, including leaks and bloat, remain a significant challenge for C and C++ developers. Applications with these problems become slower over time as their working set grows and can become unresponsive. At the same time, memory leaks and bloat remain notoriously difficult to debug, and comprise a large number of reported bugs in mature applications. Previous tools for diagnosing memory inefficiencies-based on garbage collection, binary rewriting, or code sampling-impose high overheads (up to 100X) or generate many false alarms.

This paper presents Hound, a runtime system that helps track down the sources of memory leaks and bloat in C and C++ applications. Hound employs
data sampling
, a staleness-tracking approach based on a novel heap organization, to make it both precise and efficient. Hound has no false positives, and its runtime and space overhead are low enough that it can be used in deployed applications. We demonstrate Hound's efficacy across a suite of synthetic benchmarks and real applications.
Programming model for a heterogeneous x86 platform
Authors: Saha Bratin , Zhou Xiaocheng , Chen Hu , Gao Ying , Yan Shoumeng , Rajagopalan Mohan , Fang Jesse , Zhang Peinan , Ronen Ronny , Mendelson Avi
Published: June 2009

The client computing platform is moving towards a heterogeneous architecture consisting of a combination of cores focused on scalar performance, and a set of throughput-oriented cores. The throughput oriented cores (e.g. a GPU) may be connected over both coherent and non-coherent interconnects, and have different ISAs. This paper describes a programming model for such heterogeneous platforms. We discuss the language constructs, runtime implementation, and the memory model for such a programming environment. We implemented this programming environment in a x86 heterogeneous platform simulator. We ported a number of workloads to our programming environment, and present the performance of our programming environment on these workloads.
Binary analysis for measurement and attribution of program performance
Authors: Tallent Nathan R. , Mellor-Crummey John M. , Fagan Michael W.
Published: June 2009

Modern programs frequently employ sophisticated modular designs. As a result, performance problems cannot be identified from costs attributed to routines in isolation; understanding code performance requires information about a routine's calling context. Existing performance tools fall short in this respect. Prior strategies for attributing context-sensitive performance at the source level either compromise measurement accuracy, remain too close to the binary, or require custom compilers. To understand the performance of fully optimized modular code, we developed two novel binary analysis techniques: 1)
on-the-fly
analysis of optimized machine code to enable minimally intrusive and accurate attribution of costs to dynamic calling contexts; and 2) post-mortem analysis of optimized machine code and its debugging sections to recover its program structure and reconstruct a mapping back to its source code. By combining the recovered static program structure with dynamic calling context information, we can accurately attribute performance metrics to calling contexts, procedures, loops, and inlined instances of procedures. We demonstrate that the fusion of this information provides unique insight into the performance of complex modular codes. This work is implemented in the HPCToolkit performance tools (http://hpctoolkit.org).
Semantics-aware trace analysis
Authors: Hoffman Kevin J. , Eugster Patrick , Jagannathan Suresh
Published: June 2009

As computer systems continue to become more powerful and complex, so do programs. High-level abstractions introduced to deal with complexity in large programs, while simplifying human reasoning, can often obfuscate salient program properties gleaned from automated source-level analysis through subtle (often non-local) interactions. Consequently, understanding the effects of program changes and whether these changes violate intended protocols become difficult to infer. Refactorings, and feature additions, modifications, or removals can introduce hard-to-catch bugs that often go undetected until many revisions later.

To address these issues, this paper presents a novel dynamic program analysis that builds a
semantic view
of program executions. These views reflect program abstractions and aspects; however, views are not simply projections of execution traces, but are linked to each other to capture semantic interactions among abstractions at different levels of granularity in a scalable manner.

We describe our approach in the context of Java and demonstrate its utility to improve
regression analysis
. We first formalize a subset of Java and a grammar for traces generated at program execution. We then introduce several types of views used to analyze regression bugs along with a novel, scalable technique for semantic differencing of traces from different versions of the same program. Benchmark results on large open-source Java programs demonstrate that semantic-aware trace differencing can identify precise and useful details about the underlying cause for a regression, even in programs that use reflection, multithreading, or dynamic code generation, features that typically confound other analysis techniques.
QTL for several metabolic traits map to loci controlling growth and body composition in an F2 intercross between high- and low-growth chicken lines
Authors: Nadaf Javad , Pitel Frédérique , Gilbert Hélène , Duclos Michel J. , Vignoles Florence , Beaumont Catherine , Vignal Alain , Porter Tom E. , Cogburn Larry A. , Aggrey Samuel E. , Simon Jean , Le Bihan-Duval Elisabeth
Published: June 2009

Quantitative trait loci (QTL) for metabolic and body composition traits were mapped at 7 and 9 wk, respectively, in an F2 intercross between high-growth and low-growth chicken lines. These lines also diverged for abdominal fat percentage (AFP) and plasma insulin-like growth factor-I (IGF-I), insulin, and glucose levels. Genotypings were performed with 129 microsatellite markers covering 21 chromosomes. A total of 21 QTL with genomewide level of significance were detected by single-trait analyses for body weight (BW), breast muscle weight (BMW) and percentage (BMP), AF weight (AFW) and percentage (AFP), shank length (ShL) and diameter (ShD), fasting plasma glucose level (Gluc), and body temperature (Tb). Other suggestive QTL were identified for these parameters and for plasma IGF-I and nonesterified fatty acid levels. QTL controlling adiposity and Gluc were colocalized on GGA3 and GGA5 and QTL for BW, ShL and ShD, adiposity, and Tb on GGA4. Multitrait analyses revealed two QTL controlling Gluc and AFP on GGA5 and Gluc and Tb on GGA26. Significant effects of the reciprocal cross were observed on BW, ShD, BMW, and Gluc, which may result from mtDNA and/or maternal effects. Most QTL regions for Gluc and adiposity harbor genes for which alleles have been associated with increased susceptibility to diabetes and/or obesity in humans. Identification of genes responsible for these metabolic QTL will increase our understanding of the constitutive “hyperglycemia” found in chickens. Furthermore, a comparative approach could provide new information on the genetic causes of diabetes and obesity in humans.
Ambient Games, Revealing a Route to a World Where Work is Play?
Authors: Eyles Mark , Eglin Roger
Published: June 2009

A novel way of playing games called ambient gaming is defined and described. Growing out of ideas in ambient music, ambient gaming is defined as “ignorable as it is interesting” after Brian Eno′s description of ambient music. Ambient gaming is set in the context of existing games. Further, ambient games are set in a technological context, showing that the technology enabling their development is now becoming available. The specification and implementation of an ambient game prototype, Ambient Quest, are described. Finally, future directions leading to work enhancing games are suggested.
Successful Tricuspid Valve Replacement in a Patient with Severe Pulmonary Arterial Hypertension and Preserved Right Ventricular Systolic Function
Authors: Aboulhosn Jamil A. , Oudiz Ronald J. , Dave Amish S. , Ardehali Abbas , Ross David J.
Published: June 2009

A 56-year-old patient with severe pulmonary hypertension developed severe tricuspid regurgitation, right-sided heart failure, and congestive hepatopathy. She was transferred for possible lung transplant and/or tricuspid valve surgery. Clinical and echocardiographic assessment provided confidence that acute tricuspid valve failure was responsible for the decompensation and that tricuspid valve replacement despite pulmonary hypertension could be performed.
Characterizing Wool Keratin
Authors: Cardamone Jeanette M. , Nuñez Alberto , Garcia Rafael A. , Aldema-Ramos Mila
Published: June 2009

Keratin from wool is a reactive, biocompatible, and biodegradable material. As the biological structural component of skin (soft keratins) and of nails, claws, hair, horn, feathers, and scales (hard keratins) pure keratin comprises up to 90% by weight of wool. Wool was treated in alkaline solutions to extract from 68% to 82% keratin within 2 to 5 hours of exposure at 65∘C. The keratin products were water‐soluble and were confirmed to contain intermediate filament and microfibrillar component‐proteins of fractured, residual cuticle, and cortical cells. Oxidation of wool by peroxycarboximidic acid in alkaline hydrogen peroxide produced keratin products with distinct microcrystalline structures: descaled fibers, fibrous matrices, and lyophilized powders. Morphology and confirmation of peptide functionality were documented by SEM, Amino Acid Analysis, SDS‐PAGE gel electrophoresis, MALDI‐TOF/TOF, and FTIR analyses. The reactivity of keratin from wool models the reactivity of keratin from low‐value sources such as cattle hair.
Impact of Weather Covariates on Wildfire in Tanjung Puting National Park
Authors: Eslami Esa , Nishimura Akane , Schoenberg Frederic Paik
Published: June 2009

This paper explores wildfire modeling based on meteorological variables for Tanjung Puting National Park, located on the island of Borneo. A separable model is developed for predicting daily wildfire burn area using variables such as temperature, sea level pressure, humidity, precipitation, visibility, and wind speed. Each component in the model is estimated using kernel smoothing and maximum likelihood methods. The data are shown to be largely compatible with the separable model, suggesting that the relationship between wildfire burn area and any of these weather variables in particular does not appear to change significantly depending on the values of the other weather variables. The analysis appears to confirm the findings of previous studies on wildfire in Southern California which indicate that wildfire hazard may be suitably estimated using a simple multiplicative model where the impact of each weather covariate is estimated separately.
Solitary Tibial Osteolytic Lesion
Authors: Pakos Emilios E. , Gartzonikas Dimitrios N. , Tsekeris Pericles G. , Xenakis Theodore A.
Published: June 2009

We report an unusual case of solitary osteolytic tibial metastasis from a primary endometrial cancer in a 62-year-old woman. The primary cancer was treated with total abdominal hysterectomy and bilateral salpingo-oophorectomy combined with postoperative external beam radiotherapy, while the tibial metastasis was treated with an above knee amputation. The rarity of the case lies on the fact that metastases distally to the elbow and knee are uncommon and endometrial cancer rarely gives distal bone metastases and particularly solitary to the extremities.
Direct Percutaneous Endoscopic Jejunostomy: High Completion Rates with Selective Use of a Long Drainage Access Needle
Authors: Moran G. W. , Fisher N. C.
Published: June 2009

Background. Direct percutaneous endoscopic jejunostomy (DPEJ) insertion is a useful technique for artificial nutritional support in selected patients. However, it is technically difficult and most case series report significant procedural failure rates. Methods. We reviewed our case series of DPEJ insertions, done in a tertiary care referral centre from 2002 to 2008. Patients were selected for DPEJ if they required artificial enteric nutritional support but were unsuitable for endoscopic gastrostomy. Our technique includes selective usage of a long drainage access needle for gut luminal puncture, selective fluoroscopic guidance and selective usage of general anaesthesia. Results. Of 40 consecutive patients undergoing attempted DPEJ insertion, 39/40 (97.5%) had a successful procedure. Sixteen cases (40%) required the drainage access needle for completion, nineteen cases (47.5%) were done with fluoroscopy, and five cases (12.5%) were done under general anaesthesia. There were no procedural complications. Conclusions. This technique led to a high completion rate and low complication rate. With appropriate care and expertise, DPEJ insertion is reliable and safe.
On the Almost Periodic Solutions of Differential Equations on Hilbert Spaces
Authors: Lan Nguyen Thanh
Published: June 2009

For the differential equation u′(t) = Au
(t) + f(t), t ≥ 0 on a
Hilbert space H, we find the necessary and sufficient conditions that
the above‐mentioned equation has a unique almost periodic solution. Some applications are also
given.
Traumatic Lumbosacral Dislocation Treated with Posterior Lumbar Interbody Fusion Using Intersomatic Cages
Authors: Tofuku Katsuhiro , Koga Hiroaki , Yone Kazunori , Komiya Setsuro
Published: June 2009

A 35-year-old man was struck by a car on his right side and presented with paraparesis of both lower extremities. Radiographic examination revealed multiple transverse process fractures and anterior displacement of L5 on S1. Computed tomography revealed a bilateral anterior facet dislocation of the fifth lumbar vertebra on the sacrum. MRI showed rupture of the posterior ligamentous complex. A posterior lumbar interbody fusion using two intersomatic cages and pedicle screw instrumentation and posterior fusion were performed. Although no major disc lesion was found at the level of L5-S1 on preoperative MRI, a severely collapsed L5-S1 disc was found intraoperatively. Two years after surgery, the patient was asymptomatic with normal neurological findings, and has resumed normal activity. We believe that lumbosacral dislocation can be considered a three-column injury with an L5-S1 disc lesion, and, therefore, requires a solid circumferential segmental arthrodesis to improve fusion rate.