waashk/dblp huggingface dataset:
a gpgpu compiler for memory optimization and parallelism management. this paper presents a novel optimizing compiler for general purpose computation on graphics processing units (gpgpu). it addresses two major challenges of developing high performance gpgpu programs: effective utilization of gpu memory hierarchy and judicious management of parallelism. the input to our compiler is a naïve gpu kernel function, which is functionally correct but without any consideration for performance optimization. the compiler analyzes the code, identifies its memory access patterns, and generates both the optimized kernel and the kernel invocation parameters. our optimization process includes vectorization and memory coalescing for memory bandwidth enhancement, tiling and unrolling for data reuse and parallelism management, and thread block remapping or address-offset insertion for partition-camping elimination. the experiments on a set of scientific and media processing algorithms show that our optimized code achieves very high performance, either superior or very close to the highly fine-tuned library, nvidia cublas 2.2, and up to 128 times speedups over the naive versions. another distinguishing feature of our compiler is the understandability of the optimized code, which is useful for performance analysis and algorithm refinement.
schism: fragmentation-tolerant real-time garbage collection. managed languages such as java and c# are being considered for use in hard real-time systems. a hurdle to their widespread adoption is the lack of garbage collection algorithms that offer predictable space-and-time performance in the face of fragmentation. we introduce schism/cmr, a new concurrent and real-time garbage collector that is fragmentation tolerant and guarantees time-and-space worst-case bounds while providing good throughput. schism/cmr combines mark-region collection of fragmented objects and arrays (arraylets) with separate replication-copying collection of immutable arraylet spines, so as to cope with external fragmentation when running in small heaps. we present an implementation of schism/cmr in the fiji vm, a high-performance java virtual machine for mission-critical systems, along with a thorough experimental evaluation on a wide variety of architectures, including server-class and embedded systems. the results show that schism/cmr tolerates fragmentation better than previous schemes, with a much more acceptable throughput penalty.
jinn: synthesizing dynamic bug detectors for foreign language interfaces. programming language specifications mandate static and dynamic analyses to preclude syntactic and semantic errors. although individual languages are usually well-specified, composing languages is not, and this poor specification is a source of many errors in multilingual programs. for example, virtually all java programs compose java and c using the java native interface (jni). since jni is informally specified, developers have difficulty using it correctly, and current java compilers and virtual machines (vms) inconsistently check only a subset of jni constraints. this paper's most significant contribution is to show how to synthesize dynamic analyses from state machines to detect foreign function interface (ffi) violations. we identify three classes of ffi constraints encoded by eleven state machines that capture thousands of jni and python/c ffi rules. we use a mapping function to specify which state machines, transitions, and program entities (threads, objects, references) to check at each ffi call and return. from this function, we synthesize a context-specific dynamic analysis to find ffi bugs. we build bug detection tools for jni and python/c using this approach. for jni, we dynamically and transparently interpose the analysis on java and c language transitions through the jvm tools interface. the resulting tool, called jinn, is compiler and virtual machine independent. it detects and diagnoses a wide variety of ffi bugs that other tools miss. this approach greatly reduces the annotation burden by exploiting common ffi constraints: whereas the generated jinn code is 22,000+ lines, we wrote only 1,400 lines of state machine and mapping code. overall, this paper lays the foundation for a more principled approach to developing correct multilingual software and a more concise and automated approach to ffi specification.
composing parallel software efficiently with lithe. applications composed of multiple parallel libraries perform poorly when those libraries interfere with one another by obliviously using the same physical cores, leading to destructive resource oversubscription. this paper presents the design and implementation of lithe, a low-level substrate that provides the basic primitives and a standard interface for composing parallel codes efficiently. lithe can be inserted underneath the runtimes of legacy parallel libraries to provide bolt-on composability without needing to change existing application code. lithe can also serve as the foundation for building new parallel abstractions and libraries that automatically interoperate with one another. in this paper, we show versions of threading building blocks (tbb) and openmp perform competitively with their original implementations when ported to lithe. furthermore, for two applications composed of multiple parallel libraries, we show that leveraging our substrate outperforms their original, even expertly tuned, implementations.
mixing type checking and symbolic execution. static analysis designers must carefully balance precision and efficiency. in our experience, many static analysis tools are built around an elegant, core algorithm, but that algorithm is then extensively tweaked to add just enough precision for the coding idioms seen in practice, without sacrificing too much efficiency. there are several downsides to adding precision in this way: the tool's implementation becomes much more complicated; it can be hard for an end-user to interpret the tool's results; and as software systems vary tremendously in their coding styles, it may require significant algorithmic engineering to enhance a tool to perform well in a particular software domain. in this paper, we present mix, a novel system that mixes type checking and symbolic execution. the key aspect of our approach is that these analyses are applied independently on disjoint parts of the program, in an off-the-shelf manner. at the boundaries between nested type checked and symbolically executed code regions, we use special mix rules to communicate information between the off-the-shelf systems. the resulting mixture is a provably sound analysis that is more precise than type checking alone and more efficient than exclusive symbolic execution. in addition, we also describe a prototype implementation, mixy, for c. mixy checks for potential null dereferences by mixing a null/non-null type qualifier inference system with a symbolic executor.
green: a framework for supporting energy-conscious programming using controlled approximation. energy-efficient computing is important in several systems ranging from embedded devices to large scale data centers. several application domains offer the opportunity to tradeoff quality of service/solution (qos) for improvements in performance and reduction in energy consumption. programmers sometimes take advantage of such opportunities, albeit in an ad-hoc manner and often without providing any qos guarantees. we propose a system called green that provides a simple and flexible framework that allows programmers to take advantage of such approximation opportunities in a systematic manner while providing statistical qos guarantees. green enables programmers to approximate expensive functions and loops and operates in two phases. in the calibration phase, it builds a model of the qos loss produced by the approximation. this model is used in the operational phase to make approximation decisions based on the qos constraints specified by the programmer. the operational phase also includes an adaptation function that occasionally monitors the runtime behavior and changes the approximation decisions and qos model to provide strong statistical qos guarantees. to evaluate the effectiveness of green, we implemented our system and language extensions using the phoenix compiler framework. our experiments using benchmarks from domains such as graphics, machine learning, signal processing, and finance, and an in-production, real-world web search engine, indicate that green can produce significant improvements in performance and energy consumption with small and controlled qos degradation.
inferable object-oriented typed assembly language. a certifying compiler preserves type information through compilation to assembly language programs, producing typed assembly language (tal) programs that can be verified for safety independently so that the compiler does not need to be trusted. there are two challenges for adopting certifying compilation in practice. first, requiring every compiler transformation and optimization to preserve types is a large burden on compilers, especially when adopting certifying compilation into existing optimizing non-certifying compilers. second, type annotations significantly increase the size of assembly language programs. this paper proposes an alternative to traditional certifying compilers. it presents italx, the first inferable tal type system that supports existential types, arrays, interfaces, and stacks. we have proved our inference algorithm is complete, meaning if an assembly language program is typeable with italx then our algorithm will infer an italx typing for that program. furthermore, our algorithm is guaranteed to terminate even if the assembly language program is untypeable. we demonstrate that it is practical to infer such an expressive tal by showing a prototype implementation of type inference for code compiled by bartok, an optimizing c# compiler. our prototype implementation infers complete type annotations for 98% of functions in a suite of realistic c# benchmarks. the type-inference time is about 8% of the compilation time. we needed to change only 2.5% of the compiler code, mostly adding new code for defining types and for writing types to object files. most transformations are untouched. type-annotation size is only 17% of the size of pure code and data, reducing type annotations in our previous certifying compiler [4] by 60%. the compiler needs to preserve only essential type information such as method signatures, object-layout information, and types for static data and external labels. even non-certifying compilers have most of this information available.
lock elision for read-only critical sections in java. it is not uncommon in parallel workloads to encounter shared data structures with read-mostly access patterns, where operations that update data are infrequent and most operations are read-only. typically, data consistency is guaranteed using mutual exclusion or read-write locks. the cost of atomic update of lock variables result in high overheads and high cache coherence traffic under active sharing, thus slowing down single thread performance and limiting scalability. in this paper, we present solero (software optimistic lock elision for read-only critical sections), a new lock implementation called for optimizing read-only critical sections in java based on sequential locks. solero is compatible with the conventional lock implementation of java. however, unlike the conventional implementation, only critical sections that may write data or have side effects need to update lock variables, while read-only critical sections need only read lock variables without writing them. each writing critical section changes the lock value to a new value. hence, a read-only critical section is guaranteed to be consistent if the lock is free and its value does not change from the beginning to the end of the read-only critical section. using java workloads including specjbb2005 and the hashmap and treemap java classes, we evaluate the performance impact of applying solero to read-mostly locks. our experimental results show performance improvements across the board, often substantial, in both single thread speed and scalability over the conventional lock implementation (mutual exclusion) and read-write locks. solero improves the performance of specjbb2005 by 3-5% on single and multiple threads. the results using the hashmap and treemap benchmarks show that solero outperforms the conventional lock implementation and read-write locks by substantial multiples on multi-threads.
bringing extensibility to verified compilers. verified compilers, such as leroy's compcert, are accompanied by a fully checked correctness proof. both the compiler and proof are often constructed with an interactive proof assistant. this technique provides a strong, end-to-end correctness guarantee on top of a small trusted computing base. unfortunately, these compilers are also challenging to extend since each additional transformation must be proven correct in full formal detail. at the other end of the spectrum, techniques for compiler correctness based on a domain-specific language for writing optimizations, such as lerner's rhodium and cobalt, make the compiler easy to extend: the correctness of additional transformations can be checked completely automatically. unfortunately, these systems provide a weaker guarantee since their end-to-end correctness has not been proven fully formally. we present an approach for compiler correctness that provides the best of both worlds by bridging the gap between compiler verification and compiler extensibility. in particular, we have extended leroy's compcert compiler with an execution engine for optimizations written in a domain specific and proved that this execution engine preserves program semantics, using the coq proof assistant. we present our compcert extension, xcert, including the details of its execution engine and proof of correctness in coq. furthermore, we report on the important lessons learned for making the proof development manageable.
an analysis of the dynamic behavior of javascript programs. the javascript programming language is widely used for web programming and, increasingly, for general purpose computing. as such, improving the correctness, security and performance of javascript applications has been the driving force for research in type systems, static analysis and compiler techniques for this language. many of these techniques aim to reign in some of the most dynamic features of the language, yet little seems to be known about how programmers actually utilize the language or these features. in this paper we perform an empirical study of the dynamic behavior of a corpus of widely-used javascript programs, and analyze how and why the dynamic features are used. we report on the degree of dynamism that is exhibited by these javascript programs and compare that with assumptions commonly made in the literature and accepted industry benchmark suites.
safe to the last instruction: automated verification of a type-safe operating system. typed assembly language (tal) and hoare logic can verify the absence of many kinds of errors in low-level code. we use tal and hoare logic to achieve highly automated, static verification of the safety of a new operating system called verve. our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and applications (in fact, every part of the system software except the boot loader). verve consists of a "nucleus" that provides primitive access to hardware and memory, a kernel that builds services on top of the nucleus, and applications that run on top of the kernel. the nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. the kernel, written in c# and compiled to tal, builds higher-level services, such as preemptive threads, on top of the nucleus. a tal checker verifies the safety of the kernel and applications. a hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the nucleus. verve is, to the best of our knowledge, the first operating system mechanically verified to guarantee both type and memory safety. more generally, verve's approach demonstrates a practical way to mix high-level typed code with low-level untyped code in a verifiably safe manner.
drfx: a simple and efficient memory model for concurrent programming languages. the most intuitive memory model for shared-memory multithreaded programming is sequential consistency(sc), but it disallows the use of many compiler and hardware optimizations thereby impacting performance. data-race-free (drf) models, such as the proposed c++0x memory model, guarantee sc execution for datarace-free programs. but these models provide no guarantee at all for racy programs, compromising the safety and debuggability of such programs. to address the safety issue, the java memory model, which is also based on the drf model, provides a weak semantics for racy executions. however, this semantics is subtle and complex, making it difficult for programmers to reason about their programs and for compiler writers to ensure the correctness of compiler optimizations. we present the drfx memory model, which is simple for programmers to understand and use while still supporting many common optimizations. we introduce a memory model (mm) exception which can be signaled to halt execution. if a program executes without throwing this exception, then drfx guarantees that the execution is sc. if a program throws an mm exception during an execution, then drfx guarantees that the program has a data race. we observe that sc violations can be detected in hardware through a lightweight form of conflict detection. furthermore, our model safely allows aggressive compiler and hardware optimizations within compiler-designated program regions. we formalize our memory model, prove several properties about this model, describe a compiler and hardware design suitable for drfx, and evaluate the performance overhead due to our compiler and hardware requirements.
flumejava: easy, efficient data-parallel pipelines. mapreduce and similar systems significantly ease the task of writing data-parallel code. however, many real-world computations require a pipeline of mapreduces, and programming and managing such pipelines can be difficult. we present flumejava, a java library that makes it easy to develop, test, and run efficient data-parallel pipelines. at the core of the flumejava library are a couple of classes that represent immutable parallel collections, each supporting a modest number of operations for processing them in parallel. parallel collections and their operations present a simple, high-level, uniform abstraction over different data representations and execution strategies. to enable parallel operations to run efficiently, flumejava defers their evaluation, instead internally constructing an execution plan dataflow graph. when the final results of the parallel operations are eventually needed, flumejava first optimizes the execution plan, and then executes the optimized operations on appropriate underlying primitives (e.g., mapreduces). the combination of high-level abstractions for parallel data and computation, deferred evaluation and optimization, and efficient parallel primitives yields an easy-to-use system that approaches the efficiency of hand-optimized pipelines. flumejava is in active use by hundreds of pipeline developers within google.
software data spreading: leveraging distributed caches to improve single thread performance. single thread performance remains an important consideration even for multicore, multiprocessor systems. as a result, techniques for improving single thread performance using multiple cores have received considerable attention. this work describes a technique, software data spreading, that leverages the cache capacity of extra cores and extra sockets rather than their computational resources. software data spreading is a software-only technique that uses compiler-directed thread migration to aggregate cache capacity across cores and chips and improve performance. this paper describes an automated scheme that applies data spreading to various types of loops. experiments with a set of spec2000, spec2006, nas, and microbenchmark workloads show that data spreading can provide speedup of over 2, averaging 17% for the spec and nas applications on two systems. in addition, despite using more cores for the same computation, data spreading actually saves power since it reduces access to dram.
line-up: a complete and automatic linearizability checker. modular development of concurrent applications requires thread-safe components that behave correctly when called concurrently by multiple client threads. this paper focuses on linearizability, a specific formalization of thread safety, where all operations of a concurrent component appear to take effect instantaneously at some point between their call and return. the key insight of this paper is that if a component is intended to be deterministic, then it is possible to build an automatic linearizability checker by systematically enumerating the sequential behaviors of the component and then checking if each its concurrent behavior is equivalent to some sequential behavior. we develop this insight into a tool called line-up, the first complete and automatic checker for deterministic linearizability. it is complete, because any reported violation proves that the implementation is not linearizable with respect to any sequential deterministic specification. it is automatic, requiring no manual abstraction, no manual specification of semantics or commit points, no manually written test suites, no access to source code. we evaluate line-up by analyzing 13 classes with a total of 90 methods in two versions of the .net framework 4.0. the violations of deterministic linearizability reported by line-up exposed seven errors in the implementation that were fixed by the development team.
breadcrumbs: efficient context sensitivity for dynamic bug detection analyses. calling context--the set of active methods on the stack--is critical for understanding the dynamic behavior of large programs. dynamic program analysis tools, however, are almost exclusively context insensitive because of the prohibitive cost of representing calling contexts at run time. deployable dynamic analyses, in particular, have been limited to reporting only static program locations. this paper presents breadcrumbs, an efficient technique for recording and reporting dynamic calling contexts. it builds on an existing technique for computing a compact (one word) encoding of each calling context that client analyses can use in place of a program location. the key feature of our system is a search algorithm that can reconstruct a calling context from its encoding using only a static call graph and a small amount of dynamic information collected at cold (infrequently executed) callsites. breadcrumbs requires no offline training or program modifications, and handles all language features, including dynamic class loading. we use breadcrumbs to add context sensitivity to two dynamic analyses: a data-race detector and an analysis for diagnosing null pointer exceptions. on average, it adds 10% to 20% runtime overhead, depending on a tunable parameter that controls how much dynamic information is collected. collecting less information lowers the overhead, but can result in a search space explosion. in some cases this causes reconstruction to fail, but in most cases breadcrumbs >produces non-trivial calling contexts that have the potential to significantly improve both the precision of the analyses and the quality of the bug reports.