waashk/dblp huggingface dataset:
evaluating iterative optimization across 1000 datasets. while iterative optimization has become a popular compiler optimization approach, it is based on a premise which has never been truly evaluated: that it is possible to learn the best compiler optimizations across data sets. up to now, most iterative optimization studies find the best optimizations through repeated runs on the same data set. only a handful of studies have attempted to exercise iterative optimization on a few tens of data sets. in this paper, we truly put iterative compilation to the test for the first time by evaluating its effectiveness across a large number of data sets. we therefore compose kdatasets, a data set suite with 1000 data sets for 32 programs, which we release to the public. we characterize the diversity of kdatasets, and subsequently use it to evaluate iterative optimization.we demonstrate that it is possible to derive a robust iterative optimization strategy across data sets: for all 32 programs, we find that there exists at least one combination of compiler optimizations that achieves 86% or more of the best possible speedup across all data sets using intel's icc (83% for gnu's gcc). this optimal combination is program-specific and yields speedups up to 1.71 on icc and 2.23 on gcc over the highest optimization level (-fast and -o3, respectively). this finding makes the task of optimizing programs across data sets much easier than previously anticipated, and it paves the way for the practical and reliable usage of iterative optimization. finally, we derive pre-shipping and post-shipping optimization strategies for software vendors.
pacer: proportional detection of data races. data races indicate serious concurrency bugs such as order, atomicity, and sequential consistency violations. races are difficult to find and fix, often manifesting only after deployment. the frequency and unpredictability of these bugs will only increase as software adds parallelism to exploit multicore hardware. unfortunately, sound and precise race detectors slow programs by factors of eight or more and do not scale to large numbers of threads. this paper presents a precise, low-overhead sampling-based data race detector called pacer. pacer makes a proportionality guarantee: it detects any race at a rate equal to the sampling rate, by finding races whose first access occurs during a global sampling period. during sampling, pacer tracks all accesses using the dynamically sound and precise fasttrack algorithm. in nonsampling periods, pacer discards sampled access information that cannot be part of a reported race, and pacer simplifies tracking of the happens-before relationship, yielding near-constant, instead of linear, overheads. experimental results confirm our theoretical guarantees. pacer reports races in proportion to the sampling rate. its time and space overheads scale with the sampling rate, and sampling rates of 1-3% yield overheads low enough to consider in production software. the resulting system provides a "get what you pay for" approach that is suitable for identifying real, hard-to-reproduce races in deployed systems.
2010 athena lecture. susan eggers, a professor of computer science and engineering at the university of washington, joined her department in 1989. she received a b.a. in 1965 from connecticut college and a ph.d. in 1989 from the university of california, berkeley. her research interests are in computer architecture and back-end compiler optimization, with an emphasis on experimental performance analysis. with her colleague hank levy and their students, she developed the first commercially viable multithreaded architecture, simultaneous multithreading, adopted by intel (as hyperthreading), ibm, sun and others. her current research is in the areas of distributed dataflow machines, fpgas and chip multiprocessors. in 1989 professor eggers was awarded an ibm faculty development award, in 1990 an nsf presidential young investigator award, in 1994 the microsoft professorship in computer science and engineering, and in 2009 the acm-w athena lecturer. she is a fellow of the acm and ieee, a fellow of the aaas, and a member of the national academy of engineering.
adversarial memory for detecting destructive races. multithreaded programs are notoriously prone to race conditions, a problem exacerbated by the widespread adoption of multi-core processors with complex memory models and cache coherence protocols. much prior work has focused on static and dynamic analyses for race detection, but these algorithms typically are unable to distinguish destructive races that cause erroneous behavior from benign races that do not. performing this classification manually is difficult, time consuming, and error prone. this paper presents a new dynamic analysis technique that uses adversarial memory to classify race conditions as destructive or benign on systems with relaxed memory models. unlike a typical language implementation, which may only infrequently exhibit non-sequentially consistent behavior, our adversarial memory implementation exploits the full freedom of the memory model to return older, unexpected, or stale values for memory reads whenever possible, in an attempt to crash the target program (that is, to force the program to behave erroneously). a crashing execution provides concrete evidence of a destructive bug, and this bug can be strongly correlated with a specific race condition in the target program. experimental results with our jumble prototype for java demonstrate that adversarial memory is highly effective at identifying destructive race conditions, and in distinguishing them from race conditions that are real but benign. adversarial memory can also reveal destructive races that would not be detected by traditional testing (even after thousands of runs) or by model checkers that assume sequential consistency.
guesstimate: a programming model for collaborative distributed systems. we present a new programming model gueesstimate for developing collaborative distributed systems. the model allows atomic, isolated operations that transform a system from consistent state to consistent state, and provides a shared transactional store for a collection of such operations executed by various machines in a distributed system. in addition to "committed state" which is identical in all machines in the distributed system, guesstimate allows each machine to have a replicated local copy of the state (called "guesstimated state") so that operations on shared state can be executed locally without any blocking, while also guaranteeing that eventually all machines agree on the sequences of operations executed. thus, each operation is executed multiple times, once at the time of issue when it updates the guesstimated state of the issuing machine, once when the operation is committed (atomically) to the committed state of all machines, and several times in between as the guesstimated state converges toward the committed state. while we expect the results of these executions of the operation to be identical most of the time in the class of applications we study, it is possible for an operation to succeed the first time when it is executed on the guesstimated state, and fail when it is committed. guesstimate provides facilities that allow the programmer to deal with this potential discrepancy. this paper presents our programming model, its operational semantics, its realization as an api in c#, and our experience building collaborative distributed applications with this model.
traceable data types for self-adjusting computation. self-adjusting computation provides an evaluation model where computations can respond automatically to modifications to their data by using a mechanism for propagating modifications through the computation. current approaches to self-adjusting computation guarantee correctness by recording dependencies in a trace at the granularity of individual memory operations. tracing at the granularity of memory operations, however, has some limitations: it can be asymptotically inefficient (\eg, compared to optimal solutions) because it cannot take advantage of problem-specific structure, it requires keeping a large computation trace (often proportional to the runtime of the program on the current input), and it introduces moderately large constant factors in practice. in this paper, we extend dependence-tracing to work at the granularity of the query and update operations of arbitrary (abstract) data types, instead of just reads and writes on memory cells. this can significantly reduce the number of dependencies that need to be kept in the trace and followed during an update. we define an interface for supporting a traceable version of a data type, which reports the earliest query that depends on (is changed by) revising operations back in time, and implement several such structures, including priority queues, queues, dictionaries, and counters. we develop a semantics for tracing, extend an existing self-adjusting language, δml, and its implementation to support traceable data types, and present an experimental evaluation by considering a number of benchmarks. our experiments show dramatic improvements on space and time, sometimes by as much as two orders of magnitude.
evaluating the accuracy of java profilers. performance analysts profile their programs to find methods that are worth optimizing: the "hot" methods. this paper shows that four commonly-used java profilers (xprof , hprof , jprofile, and yourkit) often disagree on the identity of the hot methods. if two profilers disagree, at least one must be incorrect. thus, there is a good chance that a profiler will mislead a performance analyst into wasting time optimizing a cold method with little or no performance improvement. this paper uses causality analysis to evaluate profilers and to gain insight into the source of their incorrectness. it shows that these profilers all violate a fundamental requirement for sampling based profilers: to be correct, a sampling-based profilermust collect samples randomly. we show that a proof-of-concept profiler, which collects samples randomly, does not suffer from the above problems. specifically, we show, using a number of case studies, that our profiler correctly identifies methods that are important to optimize; in some cases other profilers report that these methods are cold and thus not worth optimizing.
finding low-utility data structures. many opportunities for easy, big-win, program optimizations are missed by compilers. this is especially true in highly layered java applications. often at the heart of these missed optimization opportunities lie computations that, with great expense, produce data values that have little impact on the program's final output. constructing a new date formatter to format every date, or populating a large set full of expensively constructed structures only to check its size: these involve costs that are out of line with the benefits gained. this disparity between the formation costs and accrued benefits of data structures is at the heart of much runtime bloat. we introduce a run-time analysis to discover these low-utility data structures. the analysis employs dynamic thin slicing, which naturally associates costs with value flows rather than raw data flows. it constructs a model of the incremental, hop-to-hop, costs and benefits of each data structure. the analysis then identifies suspicious structures based on imbalances of its incremental costs and benefits. to decrease the memory requirements of slicing, we introduce abstract dynamic thin slicing, which performs thin slicing over bounded abstract domains. we have modified the ibm j9 commercial jvm to implement this approach. we demonstrate two client analyses: one that finds objects that are expensive to construct but are not necessary for the forward execution, and second that pinpoints ultimately-dead values. we have successfully applied them to large-scale and long-running java applications. we show that these analyses are effective at detecting operations that have unbalanced costs and benefits.
mint: java multi-stage programming using weak separability. multi-stage programming (msp) provides a disciplined approach to run-time code generation. in the purely functional setting, it has been shown how msp can be used to reduce the overhead of abstractions, allowing clean, maintainable code without paying performance penalties. unfortunately, msp is difficult to combine with imperative features, which are prevalent in mainstream languages. the central difficulty is scope extrusion, wherein free variables can inadvertently be moved outside the scopes of their binders. this paper proposes a new approach to combining msp with imperative features that occupies a "sweet spot" in the design space in terms of how well useful msp applications can be expressed and how easy it is for programmers to understand. the key insight is that escapes (or "anti-quotes") must be weakly separable from the rest of the code, i.e. the computational effects occurring inside an escape that are visible outside the escape are guaranteed to not contain code. to demonstrate the feasibility of this approach, we formalize a type system based on lightweight java which we prove sound, and we also provide an implementation, called mint, to validate both the expressivity of the type system and the effect of staging on the performance of java programs.
safe programmable speculative parallelism. execution order constraints imposed by dependences can serialize computation, preventing parallelization of code and algorithms. speculating on the value(s) carried by dependences is one way to break such critical dependences. value speculation has been used effectively at a low level, by compilers and hardware. in this paper, we focus on the use of speculation by programmers as an algorithmic paradigm to parallelize seemingly sequential code. we propose two new language constructs, speculative composition and speculative iteration. these constructs enable programmers to declaratively express speculative parallelism in programs: to indicate when and how to speculate, increasing the parallelism in the program, without concerning themselves with mundane implementation details. we present a core language with speculation constructs and mutable state and present a formal operational semantics for the language. we use the semantics to define the notion of a correct speculative execution as one that is equivalent to a non-speculative execution. in general, speculation requires a runtime mechanism to undo the effects of speculative computation in the case of mis predictions. we describe a set of conditions under which such rollback can be avoided. we present a static analysis that checks if a given program satisfies these conditions. this allows us to implement speculation efficiently, without the overhead required for rollbacks. we have implemented the speculation constructs as a c# library, along with the static checker for safety. we present an empirical evaluation of the efficacy of this approach to parallelization.
ur: statically-typed metaprogramming with type-level record computation. dependent types provide a strong foundation for specifying and verifying rich properties of programs through type-checking. the earliest implementations combined dependency, which allows types to mention program variables; with type-level computation, which facilitates expressive specifications that compute with recursive functions over types. while many recent applications of dependent types omit the latter facility, we argue in this paper that it deserves more attention, even when implemented without dependency. in particular, the ability to use functional programs as specifications enables statically-typed metaprogramming: programs write programs, and static type-checking guarantees that the generating process never produces invalid code. since our focus is on generic validity properties rather than full correctness verification, it is possible to engineer type inference systems that are very effective in narrow domains. as a demonstration, we present ur, a programming language designed to facilitate metaprogramming with first-class records and names. on top of ur, we implement ur/web, a special standard library that enables the development of modern web applications. ad-hoc code generation is already in wide use in the popular web application frameworks, and we show how that generation may be tamed using types, without forcing metaprogram authors to write proofs or forcing metaprogram users to write any fancy types.
z-rays: divide arrays and conquer speed and flexibility. arrays are the ubiquitous organization for indexed data. throughout programming language evolution, implementations have laid out arrays contiguously in memory. this layout is problematic in space and time. it causes heap fragmentation, garbage collection pauses in proportion to array size, and wasted memory for sparse and over-provisioned arrays. because of array virtualization in managed languages, an array layout that consists of indirection pointers to fixed-size discontiguous memory blocks can mitigate these problems transparently. this design however incurs significant overhead, but is justified when real-time deadlines and space constraints trump performance. this paper proposes z-rays, a discontiguous array design with flexibility and efficiency. a z-ray has a spine with indirection pointers to fixed-size memory blocks called arraylets, and uses five optimizations: (1) inlining the first n array bytes into the spine, (2) lazy allocation, (3) zero compression, (4) fast array copy, and (5) arraylet copy-on-write. whereas discontiguous arrays in prior work improve responsiveness and space efficiency, z-rays combine time efficiency and flexibility. on average, the best z-ray configuration performs within 12.7% of an unmodified java virtual machine on 19 benchmarks, whereas previous designs have two to three times higher overheads. furthermore, language implementers can configure z-ray optimizations for various design goals. this combination of performance and flexibility creates a better building block for past and future array optimization.
the reachability-bound problem. we define the reachability-bound problem to be the problem of finding a symbolic worst-case bound on the number of times a given control location inside a procedure is visited in terms of the inputs to that procedure. this has applications in bounding resources consumed by a program such as time, memory, network-traffic, power, as well as estimating quantitative properties (as opposed to boolean properties) of data in programs, such as information leakage or uncertainty propagation. our approach to solving the reachability-bound problem brings together two different techniques for reasoning about loops in an effective manner. one of these techniques is an abstract-interpretation based iterative technique for computing precise disjunctive invariants (to summarize nested loops). the other technique is a non-iterative proof-rules based technique (for loop bound computation) that takes over the role of doing inductive reasoning, while deriving its power from the use of smt solvers to reason about abstract loop-free fragments. our solution to the reachability-bound problem allows us to compute precise symbolic complexity bounds for several loops in .net base-class libraries for which earlier techniques fail. we also illustrate the precision of our algorithm for disjunctive invariant computation (which has a more general applicability beyond the reachability-bound problem) on a set of benchmark examples.
printing floating-point numbers quickly and accurately with integers. we present algorithms for accurately converting floating-point numbers to decimal representation. they are fast (up to 4 times faster than commonly used algorithms that use high-precision integers) and correct: any printed number will evaluate to the same number, when read again. our algorithms are fast, because they require only fixed-size integer arithmetic. the sole requirement for the integer type is that it has at least two more bits than the significand of the floating-point number. hence, for ieee 754 double-precision numbers (having a 53-bit significand) an integer type with 55 bits is sufficient. moreover we show how to exploit additional bits to improve the generated output. we present three algorithms with different properties: the first algorithm is the most basic one, and does not take advantage of any extra bits. it simply shows how to perform the binary-to-decimal transformation with the minimal number of bits. our second algorithm improves on the first one by using the additional bits to produce a shorter (often the shortest) result. finally we propose a third version that can be used when the shortest output is a requirement. the last algorithm either produces optimal decimal representations (with respect to shortness and rounding) or rejects its input. for ieee 754 double-precision numbers and 64-bit integers roughly 99.4% of all numbers can be processed efficiently. the remaining 0.6% are rejected and need to be printed by a slower complete algorithm.
type-preserving compilation of end-to-end verification of security enforcement. a number of programming languages use rich type systems to verify security properties of code. some of these languages are meant for source programming, but programs written in these languages are compiled without explicit security proofs, limiting their utility in settings where proofs are necessary, e.g., proof-carrying authorization. others languages do include explicit proofs, but these are generally lambda calculi not intended for source programming, that must be further compiled to an executable form. a language suitable for source programming backed by a compiler that enables end-to-end verification is missing. in this paper, we present a type-preserving compiler that translates programs written in fine, a source-level functional language with dependent refinements and affine types, to dcil, a new extension of the .net common intermediate language. fine is type checked using an external smt solver to reduce the proof burden on source programmers. we extract explicit lcf-style proof terms from the solver and carry these proof terms in the compilation to dcil, thereby removing the solver from the trusted computing base. explicit proofs enable dcil to be used in a number of important scenarios, including the verification of mobile code, proof-carrying authorization, and evidence-based auditing. we report on our experience using fine to build reference monitors for several applications, ranging from a plugin-based email client to a conference management server.
bamboo: a data-centric, object-oriented approach to many-core software. traditional data-oriented programming languages such as dataflow languages and stream languages provide a natural abstraction for parallel programming. in these languages, a developer focuses on the flow of data through the computation and these systems free the developer from the complexities of low-level, thread-oriented concurrency primitives. this simplification comes at a cost --- traditional data-oriented approaches restrict the mutation of state and, in practice, the types of data structures a program can effectively use. bamboo borrows from work in typestate and software transactions to relax the traditional restrictions of data-oriented programming models to support mutation of arbitrary data structures. we have implemented a compiler for bamboo which generates code for the tilepro64 many-core processor. we have evaluated this implementation on six benchmarks: tracking, a feature tracking algorithm from computer vision; kmeans, a k-means clustering algorithm; montecarlo, a monte carlo simulation; filterbank, a multi-channel filter bank; fractal, a mandelbrot set computation; and series, a fourier series computation. we found that our compiler generated implementations that obtained speedups ranging from 26.2x to 61.6x when executed on 62 cores.