bluuebunny/crossref_metadata_2025_split huggingface dataset:
Certifying low-level programs with hardware interrupts and preemptive threads
Authors: Feng Xinyu , Shao Zhong , Dong Yuan , Guo Yu 
Published: June 2008

Hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system programming. Unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). Existing formal verification techniques---including Hoare logic, typed assembly language, concurrent separation logic, and the assume-guarantee method---have consistently ignored the issues of interrupts; this severely limits the applicability and power of today's program verification systems.
In this paper we present a novel Hoare-logic-like framework for certifying low-level system programs involving both hardware interrupts and preemptive threads. We show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. By carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to---for the first time---successfully certify a preemptive thread implementation and a large number of common synchronization primitives. Our work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors.
Grammar-based whitebox fuzzing
Authors: Godefroid Patrice , Kiezun Adam , Levin Michael Y. 
Published: June 2008

Whitebox fuzzing is a form of automatic dynamic test generation, based on symbolic execution and constraint solving, designed for security testing of large applications. Unfortunately, the current effectiveness of whitebox fuzzing is limited when testing applications with highly-structured inputs, such as compilers and interpreters. These applications process their inputs in stages, such as lexing, parsing and evaluation. Due to the enormous number of control paths in early processing stages, whitebox fuzzing rarely reaches parts of the application beyond those first stages.
In this paper, we study how to enhance whitebox fuzzing of complex structured-input applications with a grammar-based specification of their valid inputs. We present a novel dynamic test generation algorithm where symbolic execution directly generates grammar-based constraints whose satisfiability is checked using a custom grammar-based constraint solver. We have implemented this algorithm and evaluated it on a large security-critical application, the JavaScript interpreter of Internet Explorer 7 (IE7). Results of our experiments show that grammar-based whitebox fuzzing explores deeper program paths and avoids dead-ends due to non-parsable inputs. Compared to regular whitebox fuzzing, grammar-based whitebox fuzzing increased coverage of the code generation module of the IE7 JavaScript interpreter from 53% to 81% while using three times fewer tests.
Copy coalescing by graph recoloring
Authors: Hack Sebastian , Goos Gerhard 
Published: June 2008

Register allocation is always a trade-off between live-range splitting and coalescing. Live-range splitting generally leads to less spilling at the cost of inserting shuffle code. Coalescing removes shuffle code while potentially raising the register demand and causing spilling.

Recent research showed that the live-range splitting of the SSA form's Æ-functions leads to
chordal
interference graphs. This improves upon two long-standing inconveniences of graph coloring register allocation: First, chordal graphs are optimally colorable in quadratic time. Second, the number of colors needed to color the graph is equal to the maximal register pressure in the program. However, the inserted shuffle code incurred by the Æ-functions can slow down the program severely. Hence, to make such an approach work in practice, a coalescing technique is needed that removes most of the shuffle code
without
causing further spilling.

In this paper, we present a coalescing technique designed for, but not limited to, SSA-form register allocation. We exploit that a valid coloring can be easily obtained by an SSA-based register allocator. This initial coloring is then improved by recoloring the interference graph and assigning shuffle-code related nodes the same color. Thereby, we always keep the coloring of the graph valid. Hence, the coalescing is safe, i. e. no spill code will be caused by coalescing.
Comparing to iterated register coalescing, the state of the art in safe coalescing, our method is able to remove 22.5% of the costs and 44.3% of the copies iterated coalescing left over. The best solution possible, found by a colaescer using integer linear programming (ILP), was 35.9% of the costs and 51.9% of the copies iterated coalescing left over. The runtime of programs compiled with our heuristic matches that of the programs compiled with the ILP technique.
Program analysis as constraint solving
Authors: Gulwani Sumit , Srivastava Saurabh , Venkatesan Ramarathnam 
Published: June 2008

A constraint-based approach to invariant generation in programs translates a program into constraints that are solved using off-the-shelf constraint solvers to yield desired program invariants.
In this paper we show how the constraint-based approach can be used to model a wide spectrum of program analyses in an expressive domain containing disjunctions and conjunctions of linear inequalities. In particular, we show how to model the problem of context-sensitive interprocedural program verification. We also present the first constraint-based approach to weakest precondition and strongest postcondition inference. The constraints we generate are boolean combinations of quadratic inequalities over integer variables. We reduce these constraints to SAT formulae using bitvector modeling and use off-the-shelf SAT solvers to solve them.
Furthermore, we present interesting applications of the above analyses, namely bounds analysis and generation of most-general counter-examples for both safety and termination properties. We also present encouraging preliminary experimental results demonstrating the feasibility of our technique on a variety of challenging examples.
Velodrome
Authors: Flanagan Cormac , Freund Stephen N. , Yi Jaeheon 
Published: June 2008

Atomicity is a fundamental correctness property in multithreaded programs, both because atomic code blocks are amenable to sequential reasoning (which significantly simplifies correctness arguments), and because atomicity violations often reveal defects in a program's synchronization structure. Unfortunately, all atomicity analyses developed to date are incomplete in that they may yield false alarms on correctly synchronized programs, which limits their usefulness.
We present the first dynamic analysis for atomicity that is both sound and complete. The analysis reasons about the exact dependencies between operations in the observed trace of the target program, and it reports error messages if and only if the observed trace is not conflict-serializable. Despite this significant increase in precision, the performance and coverage of our analysis is competitive with earlier incomplete dynamic analyses for atomicity.
Inferring locks for atomic sections
Authors: Cherem Sigmund , Chilimbi Trishul , Gulwani Sumit 
Published: June 2008

Atomic sections
are a recent and popular idiom to support the development of concurrent programs. Updates performed within an atomic section should not be visible to other threads until the atomic section has been executed entirely. Traditionally, atomic sections are supported through the use of optimistic concurrency, either using a transactional memory hardware, or an equivalent software emulation (STM).

This paper explores automatically supporting atomic sections using pessimistic concurrency. We present a system that combines compiler and runtime techniques to automatically transform programs written with atomic sections into programs that only use locking primitives. To minimize contention in the transformed programs, our compiler chooses from several lock granularities, using fine-grain locks whenever it is possible.
This paper formally presents our framework, shows that our compiler is sound (i.e., it protects all shared locations accessed within atomic sections), and reports experimental results.
Dataflow analysis for concurrent programs using datarace detection
Authors: Chugh Ravi , Voung Jan W. , Jhala Ranjit , Lerner Sorin 
Published: June 2008

Dataflow analyses for concurrent programs differ from their single-threaded counterparts in that they must account for shared memory locations being overwritten by concurrent threads. Existing dataflow analysis techniques for concurrent programs typically fall at either end of a spectrum: at one end, the analysis conservatively kills facts about all data that might possibly be shared by multiple threads; at the other end, a precise thread-interleaving analysis determines which data may be shared, and thus which dataflow facts must be invalidated. The former approach can suffer from imprecision, whereas the latter does not scale.
We present RADAR, a framework that automatically converts a dataflow analysis for sequential programs into one that is correct for concurrent programs. RADAR uses a race detection engine to kill the dataflow facts, generated and propagated by the sequential analysis, that become invalid due to concurrent writes. Our approach of factoring all reasoning about concurrency into a race detection engine yields two benefits. First, to obtain analyses for code using new concurrency constructs, one need only design a suitable race detection engine for the constructs. Second, it gives analysis designers an easy way to tune the scalability and precision of the overall analysis by only modifying the race detection engine. We describe the RADAR framework and its implementation using a pre-existing race detection engine. We show how RADAR was used to generate a concurrent version of a null-pointer dereference analysis, and we analyze the result of running the generated concurrent analysis on several benchmarks.
XMem
Authors: Wegiel Michal , Krintz Chandra 
Published: June 2008

Developers commonly build contemporary enterprise applications using type-safe, component-based platforms, such as J2EE, and architect them to comprise multiple tiers, such as a web container, application server, and database engine. Administrators increasingly execute each tier in its own managed runtime environment (MRE) to improve reliability and to manage system complexity through the fault containment and modularity offered by isolated MRE instances. Such isolation, however, necessitates expensive cross-tier communication based on protocols such as object serialization and remote procedure calls. Administrators commonly co-locate communicating MREs on a single host to reduce communication overhead and to better exploit increasing numbers of available processing cores. However, state-of-the-art MREs offer no support for more efficient communication between co-located MREs, while fast inter-process communication mechanisms, such as shared memory, are widely available as a standard operating system service on most modern platforms.
To address this growing need, we present the design and implementation of XMem ? type-safe, transparent, shared memory support for co-located MREs. XMem guarantees type-safety through coordinated, parallel, multi-process class loading and garbage collection. To avoid introducing any level of indirection, XMem manipulates virtual memory mapping. In addition, object sharing in XMem is fully transparent: shared objects are identical to local objects in terms of field access, synchronization, garbage collection, and method invocation, with the only difference being that sharedto-private pointers are disallowed. XMem facilitates easy integration and use by existing communication technologies and software systems, such as RMI, JNDI, JDBC, serialization/XML, and network sockets.
We have implemented XMem in the open-source, productionquality HotSpot Java Virtual Machine. Our experimental evaluation, based on core communication technologies underlying J2EE, as well as using open-source server applications, indicates that XMem significantly improves throughput and response time by avoiding the overheads imposed by object serialization and network communication.
Model checking transactional memories
Authors: Guerraoui Rachid , Henzinger Thomas A. , Jobstmann Barbara , Singh Vasu 
Published: June 2008

Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.
Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.
Flexible task graphs
Authors: Auerbach Joshua , Bacon David F. , Guerraoui Rachid , Spring Jesper Honig , Vitek Jan 
Published: June 2008

The disadvantages of unconstrained shared-memory multi-threading in Java, especially with regard to latency and determinism in realtime systems, have given rise to a variety of language extensions that place restrictions on how threads allocate, share, and communicate memory, leading to order-of-magnitude reductions in latency and jitter. However, each model makes different trade-offs with respect to expressiveness, efficiency, enforcement, and latency, and no one model is best for all applications.
In this paper we present Flexible Task Graphs (Flexotasks), a single system that allows different isolation policies and mechanisms to be combined in an orthogonal manner, subsuming four previously proposed models as well as making it possible to use new combinations best suited to the needs of particular applications. We evaluate our implementation on top of the IBM Web-Sphere Real Time Java virtual machine using both a microbenchmark and a 30 KLOC avionics collision detector. We show that Flexotasks are capable of executing periodic threads at 10 KHz with a standard deviation of 1.2μs and that it achieves significantly better performance than RTSJ's scoped memory constructs while remaining impervious to interference from global garbage collection.
Impact of JVM superoperators on energy consumption in resource-constrained embedded systems
Authors: Badea Carmen , Nicolau Alexandru , Veidenbaum Alexander V. 
Published: June 2008

Energy consumption is one of the most important issues in resource-constrained embedded systems. Many such systems run Java-based applications due to Java's architecture-independent format (bytecode). Standard techniques for executing bytecode programs, e.g. interpretation or just-in-time compilation, have performance or memory issues that make them unsuitable for resource-constrained embedded systems.
A superoperator-extended, lightweight Java Virtual Machine (JVM) can be used in resource-constrained embedded systems to improve performance and reduce memory consumption. This paper shows that such a JVM also significantly reduces energy consumption. This is due primarily to a considerable reduction in the number of memory accesses and thus in energy consumption in the instruction and data TLBs and caches and, in most cases, in DRAM energy consumption. Since the fraction of processor energy dissipated in these units is approximately 60%, the energy savings achieved are significant.
The paper evaluates the number of load, store, and computational instructions eliminated by the use of proposed superoperators as compared to a simple interpreter on a set of embedded benchmarks. Using cache and DRAM per access energy we estimate the total processor/DRAM energy saved by using our JVM. Our results show that with 32KB caches the reduction in energy consumption ranges from 40% to 60% of the overall processor, plus DRAM energy. Even higher savings may be achieved with smaller caches and increased access to DRAM as DRAM access energy is fairly high.
Relative competitive analysis of cache replacement policies
Authors: Reineke Jan , Grund Daniel 
Published: June 2008

Caches are commonly employed to hide the latency gap between memory and the CPU by exploiting locality in memory accesses. On today's architectures a cache miss may cost several hundred CPU cycles.

In order to fulfill stringent performance requirements, caches are now also used in hard real-time systems. In such systems, upper and sometimes also lower bounds on the execution times of a task have to be computed. To obtain tight bounds, timing analyses
must
take into account the cache architecture. However, developing cache analyses -- analyses that determine whether a memory access is a hit or a miss -- is a difficult problem for some cache architectures.

In this paper, we present a tool to automatically compute relative competitive ratios for a large class of replacement policies, including LRU, FIFO, and PLRU. Relative competitive ratios bound the performance of one policy relative to the performance of another policy.
These performance relations allow us to use cache-performance predictions for one policy to compute predictions for another, including policies that could previously not be dealt with.
The amateur search
Authors: Olson Michael 
Published: June 2008

In the days that followed Jim's disappearance at sea, his family, friends and colleagues came together in a remarkable effort to help find him. The group gathered, analyzed and filtered information from many sources. In concert with the Coast Guard, the results were used to focus the search in the places where Jim and his sailboat Tenacious were most likely to be.
The scope and breadth -- indeed, the very existence -- of this amateur search effort reflect Jim at his best. The group was at first composed of those whose lives he had touched directly, who used skills and knowledge he had helped them to gain in hopes of finding him. As time passed, others joined in who were inspired by the unfolding story. In the end, thousands came together to search for Jim.
Knowledge and wisdom
Authors: Helland Pat 
Published: June 2008

Jim Gray was my mentor and friend for almost 25 years. Even before we met, he was changing my life through his writings. Jim continually and patiently nudged me to strive for more, accomplish more, and to pass these gifts on to others. He embodied those attributes that I most want to emulate.
Jim influenced those around him both by sharing in his immense knowledge and by listening and guiding. Even more, he created a community that fostered growth and sharing across competitive boundaries with a clear ethical compass. This paper summarizes my experiences with Jim's approach to nurturing and mentoring.
TerraServer and the Russia adventure...
Authors: Barclay Tom 
Published: June 2008

Jim Gray made many friends and few enemies in his career. Many of the projects he worked on were inspired by one or more of his friends and collaborators in industry and academia.
The original idea for an "image server" happened in the early 1990s when Jim was at Digital. Jim had met Jeff Dozier while working on the National Research Council's "Computing the Future" committee [NRC 1994]. Jeff became Dean of the Bren School of Environmental Sciences and chair of UC Santa Barbara's Alexandria Digital Library advisory board. Jeff asked Jim to serve on the board.
During an Alexandria board meeting, Jeff and Jim discussed the idea for a "geospatial image server". All they needed was a lot of accessible imagery, someone that wanted it done, and someone foolish enough to load a few tera-bytes of data. The cold war ended enabling the high resolution imagery marketplace. Microsoft SQL Server wanted a scalability internet demonstration. And I walked into Jim Gray's lab looking for a reason to move back to San Francisco. And that's where my 10 year project with Jim Gray and TerraServer begins...
Exponential Size Distributions for Snow
Authors: Heymsfield Andrew J. , Field Paul , Bansemer Aaron 
Published: June 2008

Abstract
Using airborne data from several recent field projects, the authors have taken another look at the properties of exponential ice particle size distributions (PSDs) when the PSDs are broad. Two primary questions are addressed: for what ranges of ice water content (IWC) and equivalent radar reflectivity (Ze) do exponentials produce accurate estimates of these higher moments of the PSD, and why is there a lower limit to the value to the slope of exponential fits to PSD, λ, as has been found from airborne measurements?
Earlier studies at temperatures primarily above −10°C have found that λ measured in snow during spiral descents through deep ice cloud layers decreases to about 9 cm−1 and then remains there. Several physical processes have been advanced to explain these observations. If reliable, the data could be used to improve retrieval of ice cloud properties through remote sensing and for cloud model representations of ice cloud microphysical properties.
For data acquired from 2D probes, recent evidence indicates shattering of large ice particles ahead of, but attributable to, the probe’s sensing area, generating small crystals that the probe then senses. Shattered artifacts have been objectively removed from the data. Comparisons of size distributions before and after removal of suspected shattered particles suggest that the reported minimum may have been due to shattering and/or other instrument errors.
The revised PSDs indicate that for λ &lt; 40 cm−1, 0.1 g m−1 &lt; IWC, and 5 dB &lt; Ze, moments two (IWC) through four (Ze) of the PSD are dominated by particles larger than a few hundred microns. Analytical representations with more variables than exponentials (e.g., gamma PSD) are not required to accurately derive these moments from the PSD. In these situations, the intercept parameter of the exponential PSD, N0 ≈ 1 cm−4, is 5 to 30 times larger than assumed earlier.