waashk/dblp huggingface dataset:
optimistic parallelism requires abstractions. irregular applications, which manipulate large, pointer-based data structures like graphs, are difficult to parallelize manually. automatic tools and techniques such as restructuring compilers and run-time speculative execution have failed to uncover much parallelism in these applications, in spite of a lot of effort by the research community. these difficulties have even led some researchers to wonder if there is any coarse-grain parallelism worth exploiting in irregular applications. in this paper, we describe two real-world irregular applications: a delaunay mesh refinement application and a graphics application thatperforms agglomerative clustering. by studying the algorithms and data structures used in theseapplications, we show that there is substantial coarse-grain, data parallelism in these applications, but that this parallelism is very dependent on the input data and therefore cannot be uncoveredby compiler analysis. in principle, optimistic techniques such asthread-level speculation can be used to uncover this parallelism, but we argue that current implementations cannot accomplish thisbecause they do not use the proper abstractions for the data structuresin these programs. these insights have informed our design of the galois system, an object-based optimistic parallelization system for irregular applications. there are three main aspects to galois: (1) a small number of syntactic constructs for packaging optimistic parallelism as iteration over ordered and unordered sets, (2)assertions about methods in class libraries, and (3) a runtime scheme for detecting and recovering from potentially unsafe accesses to shared memory made by an optimistic computation. we show that delaunay mesh generation and agglomerative clustering can be parallelized in a straight-forward way using the galois approach, and we present experimental measurements to show that this approach is practical. these results suggest that galois is a practical approach to exploiting data parallelismin irregular programs.
searching for type-error messages. advanced type systems often need some form of type inference to reduce the burden of explicit typing, but type inference often leads to poor error messages for ill-typed programs. this work pursues a new approach to constructing compilers and presenting type-error messages in which the type-checker itself does not produce the messages. instead, it is an oracle for a search procedure that finds similar programs that do type-check. our two-fold goal is to improve error messages while simplifying compiler construction. our primary implementation and evaluation is for caml, a language with full type inference. we also present a prototype for c++ template functions, where type instantiation is implicit. a key extension is making our approach robust even when the program has multiple independent type errors.
bootstrapping: a technique for scalable flow and context-sensitive pointer alias analysis. we propose a framework for improving both the scalability as well as the accuracy of pointer alias analysis, irrespective of its flow or context-sensitivities, by leveraging a three-pronged strategy that effectively combines divide and conquer, parallelization and function summarization. a key step in our approach is to first identify small subsets of pointers such that the problem of computing aliases of any pointer can be reduced to computing them in these small subsets instead of the entire program. in order to identify these subsets, we first apply a series of increasingly accurate but highly scalable (context and flow-insensitive) alias analyses in a cascaded fashion such that each analysis ai works on the subsets generated by the previous one ai-1. restricting the application of ai to subsets generated by ai-1, instead of the entire program, improves it scalability, i.e., ai is bootstrapped by ai-1. once these small subsets have been computed, in order to make our overall analysis accurate, we employ our new summarization-based flow and context-sensitive alias analysis. the small size of each subset offsets the higher computational complexity of the context-sensitive analysis. an important feature of our framework is that the analysis for each of the subsets can be carried out independently of others thereby allowing us to leverage parallelization further improving scalability.
model checking transactional memories. 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.
ucc: update-conscious compilation for energy efficiency in wireless sensor networks. wireless sensor networks (wsn), composed of a large number of low-cost, battery-powered sensors, have recently emerged as promising computing platforms for many non-traditional applications. the preloaded code on remote sensors often needs to be updated after deployment in order for the wsn to adapt to the changing demands from the users. post-deployment code dissemination is challenging as the data are transmitted via battery-powered wireless communication. recent studies show that the energy for sending a single bit is about the same as executing 1000 instructions in awsn. therefore it is important to achieve energy efficiency in code dissemination. in this paper, we propose novel update-conscious compilation(ucc) techniques for energy-efficient code dissemination in wsns. an update-conscious compiler, when compiling the modified code, includes the compilation decisions that were made when generating the old binary. the compiler employs a detailed energy model and strives to match the old decisions for a more energy-efficient result. in most cases, matching the previous decisions improves the binary code similarity, reduces the amount of data to be transmitted to remote sensors, and thus, consumes less energy. in this paper, we develop update-conscious register allocation and data layout algorithms. our experimental results show that they can achieve great improvements over the traditional, update-oblivious approaches.
a general framework for certifying garbage collectors and their mutators. garbage-collected languages such as java and c# are becoming more and more widely used in both high-end software and real-time embedded applications. the correctness of the gc implementation is essential to the reliability and security of a large portion of the world's mission-critical software. unfortunately, garbage collectors--especially incremental and concurrent ones--are extremely hard to implement correctly. in this paper, we present a new uniform approach to verifying the safety of both a mutator and its garbage collector in hoare-style logic. we define a formal garbage collector interface general enough to reason about a variety of algorithms while allowing the mutator to ignore implementation-specific details of the collector. our approach supports collectors that require read and write barriers. we have used our approach to mechanically verify assembly implementations of mark-sweep, copying and incremental copying gcs in coq, as well as sample mutator programs that can be linked with any of the gcs to produce a fully-verified garbage-collected program. our work provides a foundation for reasoning about complex mutator-collector interaction and makes an important advance toward building fully certified production-quality gcs.
automatic inversion generates divide-and-conquer parallel programs. divide-and-conquer algorithms are suitable for modern parallel machines, tending to have large amounts of inherent parallelism and working well with caches and deep memory hierarchies. among others, list homomorphisms are a class of recursive functions on lists, which match very well with the divide-and-conquer paradigm. however, direct programming with list homomorphisms is a challenge for many programmers. in this paper, we propose and implement a novel systemthat can automatically derive cost-optimal list homomorphisms from a pair of sequential programs, based on the third homomorphism theorem. our idea is to reduce extraction of list homomorphisms to derivation of weak right inverses. we show that a weak right inverse always exists and can be automatically generated from a wide class of sequential programs. we demonstrate our system with several nontrivial examples, including the maximum prefix sum problem, the prefix sum computation, the maximum segment sum problem, and the line-of-sight problem. the experimental results show practical efficiency of our automatic parallelization algorithm and good speedups of the generated parallel programs.
iterative context bounding for systematic testing of multithreaded programs. multithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the development cycle and post-deployment. model checking or systematic exploration of program behavior is a promising alternative to traditional testing methods. however, it is difficult to perform systematic search on large programs as the number of possible program behaviors grows exponentially with the program size. confronted with this state-explosion problem, traditional model checkers perform iterative depth-bounded search. although effective for message-passing software, iterative depth-bounding is inadequate for multithreaded software. this paper proposes iterative context-bounding, a new search algorithm that systematically explores the executions of a multithreaded program in an order that prioritizes executions with fewer context switches. we distinguish between preempting and nonpreempting context switches, and show that bounding the number of preempting context switches to a small number significantly alleviates the state explosion, without limiting the depth of explored executions. we show both theoretically and empirically that context-bounded search is an effective method for exploring the behaviors of multithreaded programs. we have implemented our algorithmin two model checkers and applied it to a number of real-world multithreaded programs. our implementation uncovered 9 previously unknown bugs in our benchmarks, each of which was exposed by an execution with at most 2 preempting context switches. our initial experience with the technique is encouraging and demonstrates that iterative context-bounding is a significant improvement over existing techniques for testing multithreaded programs.
automatically classifying benign and harmful data racesallusing replay analysis. many concurrency bugs in multi-threaded programs are due to dataraces. there have been many efforts to develop static and dynamic mechanisms to automatically find the data races. most of the prior work has focused on finding the data races and eliminating the false positives. in this paper, we instead focus on a dynamic analysis technique to automatically classify the data races into two categories - the dataraces that are potentially benign and the data races that are potentially harmful. a harmful data race is a real bug that needs to be fixed. this classification is needed to focus the triaging effort on those data races that are potentially harmful. without prioritizing the data races we have found that there are too many data races to triage. our second focus is to automatically provide to the developer a reproducible scenario of the data race, which allows the developer to understand the different effects of a harmful data race on a program's execution. to achieve the above, we record a multi-threaded program's execution in a replay log. the replay log is used to replay the multi-threaded program, and during replay we find the data races using a happens-before based algorithm. to automatically classify if a data race that we find is potentially benign or potentially harmful, were play the execution twice for a given data race - one for each possible order between the conflicting memory operations. if the two replays for the two orders produce the same result, then we classify the data race to be potentially benign. we discuss our experiences in using our replay based dynamic data race checker on several microsoft applications.
valgrind: a framework for heavyweight dynamic binary instrumentation. dynamic binary instrumentation (dbi) frameworks make it easy to build dynamic binary analysis (dba) tools such as checkers and profilers. much of the focus on dbi frameworks has been on performance; little attention has been paid to their capabilities. as a result, we believe the potential of dbi has not been fully exploited. in this paper we describe valgrind, a dbi framework designed for building heavyweight dba tools. we focus on its unique support for shadow values-a powerful but previously little-studied and difficult-to-implement dba technique, which requires a tool to shadow every register and memory value with another value that describes it. this support accounts for several crucial design features that distinguish valgrind from other dbi frameworks. because of these features, lightweight tools built with valgrind run comparatively slowly, but valgrind can be used to build more interesting, heavyweight tools that are difficult or impossible to build with other dbi frameworks such as pin and dynamorio.
exterminator: automatically correcting memory errors with high probability. programs written in c and c++ are susceptible to memory errors, including buffer overflows and dangling pointers. these errors, whichcan lead to crashes, erroneous execution, and security vulnerabilities, are notoriously costly to repair. tracking down their location in the source code is difficult, even when the full memory state of the program is available. once the errors are finally found, fixing them remains challenging: even for critical security-sensitive bugs, the average time between initial reports and the issuance of a patch is nearly one month. we present exterminator, a system that automatically correct sheap-based memory errors without programmer intervention. exterminator exploits randomization to pinpoint errors with high precision. from this information, exterminator derives runtime patches that fix these errors both in current and subsequent executions. in addition, exterminator enables collaborative bug correction by merging patches generated by multiple users. we present analytical and empirical results that demonstrate exterminator's effectiveness at detecting and correcting both injected and real faults.
fault-tolerant typed assembly language. a transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. although transient faults do not permanently damage the hardware, they may corrupt computations by altering stored values and signal transfers. in this paper, we propose a new scheme for provably safe and reliable computing in the presence of transient hardware faults. in our scheme, software computations are replicated to provide redundancy while special instructions compare the independently computed results to detect errors before writing critical data. in stark contrast to any previous efforts in this area, we have analyzed our fault tolerance scheme from a formal, theoretical perspective. to be specific, first, we provide an operational semantics for our assembly language, which includes a precise formal definition of our fault model. second, we develop an assembly-level type system designed to detect reliability problems in compiled code. third, we provide a formal specification for program fault tolerance under the given fault model and prove that all well-typed programs are indeed fault tolerant. in addition to the formal analysis, we evaluate our detection scheme and show that it only takes 34% longer to execute than the unreliable version.
static specification inference using predicate mining. the reliability and correctness of complex software systems can be significantly enhanced through well-defined specifications that dictate the use of various units of abstraction (e.g., modules, or procedures). often times, however, specifications are either missing, imprecise, or simply too complex to encode within a signature, necessitating specification inference. the process of inferring specifications from complex software systems forms the focus of this paper. we describe a static inference mechanism for identifying the preconditions that must hold whenever a procedure is called. these preconditions may reflect both data flow properties (e.g., whenever p is called, variable x must be non-null) as well as control-flow properties (e.g., every call to p must bepreceded by a call to q). we derive these preconditions using a ninter-procedural path-sensitive dataflow analysis that gathers predicates at each program point. we apply mining techniques to these predicates to make specification inference robust to errors. this technique also allows us to derive higher-level specifications that abstract structural similarities among predicates (e.g., procedure p is called immediately after a conditional test that checks whether some variable v is non-null.) we describe an implementation of these techniques, and validate the effectiveness of the approach on a number of large open-source benchmarks. experimental results confirm that our mining algorithms are efficient, and that the specifications derived are both precise and useful-the implementation discovers several critical, yet previously, undocumented preconditions for well-tested libraries.
parameterized tiled loops for free. parameterized tiled loops-where the tile sizes are not fixed at compile time, but remain symbolic parameters until later--are quite useful for iterative compilers and "auto-tuners" that produce highly optimized libraries and codes. tile size parameterization could also enable optimizations such as register tiling to become dynamic optimizations. although it is easy to generate such loops for (hyper) rectangular iteration spaces tiled with (hyper) rectangular tiles, many important computations do not fall into this restricted domain. parameterized tile code generation for the general case of convex iteration spaces being tiled by (hyper) rectangular tiles has in the past been solved with bounding box approaches or symbolic fourier motzkin approaches. however, both approaches have less than ideal code generation efficiency and resulting code quality. we present the theoretical foundations, implementation, and experimental validation of a simple, unified technique for generating parameterized tiled code. our code generation efficiency is comparable to all existing code generation techniques including those for fixed tile sizes, and the resulting code is as efficient as, if not more than, all previous techniques. thus the technique provides parameterized tiled loops for free! our "one-size-fits-all" solution, which is available as open source software can be adapted for use in production compilers.
automatic inference of optimizer flow functions from semantic meanings. previous work presented a language called rhodium for writing program analyses and transformations, in the form of declarative flow functions that propagate instances of user-defined dataflow fact schemas. each dataflow fact schema specifies a semantic meaning, which allows the rhodium system to automatically verify the correctness of the user's flow functions. in this work, we have reversed the roles of the flow functions and semantic meanings: rather than checking the correctness of the user-written flow functions using the facts' semantic meanings, we automatically infer correct flow functions solely from the meanings of the dataflow fact schemas. we have implemented our algorithm for inferring flow functions from fact schemas in the context of the whirlwind compiler, and have used this implementation to infer flow functions for a variety of fact schemas. the automatically generated flow functions cover most of the situations covered by an earlier suite of handwritten rules.
orchestrating the execution of stream programs on multicore platforms. while multicore hardware has become ubiquitous, explicitly parallel programming models and compiler techniques for exploiting parallelism on these systems have noticeably lagged behind. stream programming is one model that has wide applicability in the multimedia, graphics, and signal processing domains. streaming models execute as a set of independent actors that explicitly communicate data through channels. this paper presents a compiler technique for planning and orchestrating the execution of streaming applications on multicore platforms. an integrated unfolding and partitioning step based on integer linear programming is presented that unfolds data parallel actors as needed and maximally packs actors onto cores. next, the actors are assigned to pipeline stages in such a way that all communication is maximally overlapped with computation on the cores. to facilitate experimentation, a generalized code generation template for mapping the software pipeline onto the cell architecture is presented. for a range of streaming applications, a geometric mean speedup of 14.7x is achieved on a 16-core cell platform compared to a single core.
foundations of the c++ concurrency memory model. currently multi-threaded c or c++ programs combine a single-threaded programming language with a separate threads library. this is not entirely sound [7]. we describe an effort, currently nearing completion, to address these issues by explicitly providing semantics for threads in the next revision of the c++ standard. our approach is similar to that recently followed by java [25], in that, at least for a well-defined and interesting subset of the language, we give sequentially consistent semantics to programs that do not contain data races. nonetheless, a number of our decisions are often surprising even to those familiar with the java effort:we (mostly) insist on sequential consistency for race-free programs, in spite of implementation issues that came to light after the java work. we give no semantics to programs with data races. there are no benign c++ data races. we use weaker semantics for trylock than existing languages or libraries, allowing us to promise sequential consistency with an intuitive race definition, even for programs with trylock. this paper describes the simple model we would like to be able to provide for c++ threads programmers, and explain how this, together with some practical, but often under-appreciated implementation constraints, drives us towards the above decisions.