waashk/dblp huggingface dataset:
ditto: automatic incrementalization of data structure invariant checks (in java). we present ditto, an automatic incrementalizer for dynamic, side-effect-free data structure invariant checks. incrementalization speeds up the execution of a check by reusing its previous executions, checking the invariant anew only the changed parts of the data structure. ditto exploits properties specific to the domain of invariant checks to automate and simplify the process without restricting what mutations the program can perform. our incrementalizer works for modern imperative languages such as java and c#. it can incrementalize,for example, verification of red-black tree properties and the consistency of the hash code in a hash table bucket. our source-to-source implementation for java is automatic, portable, and efficient. ditto provides speedups on data structures with as few as 100 elements; on larger data structures, its speedups are characteristic of non-automatic incrementalizers: roughly 5-fold at 5,000 elements,and growing linearly with data structure size.
enforcing isolation and ordering in stm. transactional memory provides a new concurrency control mechanism that avoids many of the pitfalls of lock-based synchronization. high-performance software transactional memory (stm) implementations thus far provide weak atomicity: accessing shared data both inside and outside a transaction can result in unexpected, implementation-dependent behavior. to guarantee isolation and consistent ordering in such a system, programmers are expected to enclose all shared-memory accesses inside transactions. a system that provides strong atomicity guarantees isolation even in the presence of threads that access shared data outside transactions. a strongly-atomic system also orders transactions with conflicting non-transactional memory operations in a consistent manner. in this paper, we discuss some surprising pitfalls of weak atomicity, and we present an stm system that avoids these problems via strong atomicity. we demonstrate how to implement non-transactional data accesses via efficient read and write barriers, and we present compiler optimizations that further reduce the overheads of these barriers. we introduce a dynamic escape analysis that differentiates private and public data at runtime to make barriers cheaper and a static not-accessed-in-transaction analysis that removes many barriers completely. our results on a set of java programs show that strong atomicity can be implemented efficiently in a high-performance stm system.
sketching stencils. performance of stencil computations can be significantly improved through smart implementations that improve memory locality, computation reuse, or parallelize the computation. unfortunately, efficient implementations are hard to obtain because they often involve non-traditional transformations, which means that they cannot be produced by optimizing the reference stencil with a compiler. in fact, many stencils are produced by code generators that were tediously handcrafted. in this paper, we show how stencil implementations can be produced with sketching. sketching is a software synthesis approach where the programmer develops a partial implementation--a sketch--and a separate specification of the desired functionality given by a reference (unoptimized) stencil. the synthesizer then completes the sketch to behave like the specification, filling in code fragments that are difficult to develop manually. existing sketching systems work only for small finite programs, i.e.,, programs that can be represented as small boolean circuits. in this paper, we develop a sketching synthesizer that works for stencil computations, a large class of programs that, unlike circuits, have unbounded inputs and outputs, as well as an unbounded number of computations. the key contribution is a reduction algorithm that turns a stencil into a circuit, allowing us to synthesize stencils using an existing sketching synthesizer.
thin slicing. program slicing systematically identifies parts of a program relevant to a seed statement. unfortunately, slices of modern programs often grow too large for human consumption. we argue that unwieldy slices arise primarily from an overly broad definition of relevance, rather than from analysis imprecision. while a traditional slice includes all statements that may affect a point of interest, not all such statements appear equally relevant to a human. as an improved method of finding relevant statements, we propose thin slicing. a thin slice consists only of producer statements for the seed, i.e., those statements that help compute and copy avalue to the seed. statements that explain why producers affect the seed are excluded. for example, for a seed that reads a value from a container object, a thin slice includes statements that store the value into the container, but excludes statements that manipulate pointers to the container itself. thin slices can also be hierarchically expanded to include statements explaining how producers affect the seed, yielding a traditional slice in the limit. we evaluated thin slicing for a set of debugging and program understanding tasks. the evaluation showed that thin slices usually included the desired statements for the tasks (e.g., the buggy statement for a debugging task). furthermore, in simulated use of a slicing tool, thin slices revealed desired statements after inspecting 3.3 times fewer statements than traditional slicing for our debugging tasks and 9.4 times fewer statements for our program understanding tasks. finally, our thin slicing algorithm scales well to relatively large java benchmarks, suggesting that thin slicing represents an attractive option for practical tools.
the exovm system for automatic vm and application reduction. embedded systems pose unique challenges to java application developers and virtual machine designers. chief among these challenges is the memory footprint of both the virtual machine and the applications that run within it. with the rapidly increasing set of features provided by the java language, virtual machine designers are often forced to build custom implementations that make various tradeoffs between the footprint of the virtual machine and the subset of the java language and class libraries that are supported. in this paper, we present the exovm, a system in which an application is initialized in a fully featured virtual machine, and then the code, data, and virtual machine features necessary to execute it are packaged into a binary image. key to this process is feature analysis, a technique for computing the reachable code and data of a java program and its implementation inside the vm simultaneously. the exovm reduces the need to develop customized embedded virtual machines by reusing a single vm infrastructure and automatically eliding the implementation of unused java features on a per-program basis. we present a constraint-based instantiation of the analysis technique, an implementation in ibm's j9 java vm, experiments evaluating our technique for the eembc benchmark suite, and some discussion of the individual costs of some of java's features. our evaluation shows that our system can reduce the non-heap memory allocation of the virtual machine by as much as 75%. we discuss vm and language design decisions that our work shows are important in targeting embedded systems, supporting the long-term goal of a common vm infrastructure spanning from motes to large servers.
cgcexplorer: a semi-automated search procedure for provably correct concurrent collectors. concurrent garbage collectors are notoriously hard to design, implement, and verify. we present a framework for the automatic exploration of a space of concurrent mark-and-sweep collectors. in our framework, the designer specifies a set of "building blocks" from which algorithms can be constructed. these blocks reflect the designer's insights about the coordination between the collector and the mutator. given a set of building blocks, our framework automatically explores a space of algorithms, using model checking with abstraction to verify algorithms in the space. we capture the intuition behind some common mark-and-sweep algorithms using a set of building blocks. we utilize our framework to automatically explore a space of more than 1,600,000 algorithms built from these blocks, and derive over 100 correct fine-grained algorithms with various space, synchronization, and precision tradeoffs.
effective automatic parallelization of stencil computations. performance optimization of stencil computations has been widely studied in the literature, since they occur in many computationally intensive scientific and engineering applications. compiler frameworks have also been developed that can transform sequential stencil codes for optimization of data locality and parallelism. however, loop skewing is typically required in order to tile stencil codes along the time dimension, resulting in load imbalance in pipelined parallel execution of the tiles. in this paper, we develop an approach for automatic parallelization of stencil codes, that explicitly addresses the issue of load-balanced execution of tiles. experimental results are provided that demonstrate the effectiveness of the approach.
register allocation by puzzle solving. we show that register allocation can be viewed as solving a collection of puzzles. we model the register file as a puzzle board and the program variables as puzzle pieces; pre-coloring and register aliasing fit in naturally. for architectures such as powerpc, x86, and strongarm, we can solve the puzzles in polynomial time, and we have augmented the puzzle solver with a simple heuristic for spilling. for spec cpu2000, the compilation time of our implementation is as fast as that of the extended version of linear scan used by llvm, which is the jit compiler in the opengl stack of mac os 10.5. our implementation produces x86 code that is of similar quality to the code produced by the slower, state-of-the-art iterated register coalescing of george and appel with the extensions proposed by smith, ramsey, and holloway in 2004.
race directed random testing of concurrent programs. bugs in multi-threaded programs often arise due to data races. numerous static and dynamic program analysis techniques have been proposed to detect data races. we propose a novel randomized dynamic analysis technique that utilizes potential data race information obtained from an existing analysis tool to separate real races from false races without any need for manual inspection. specifically, we use potential data race information obtained from an existing dynamic analysis technique to control a random scheduler of threads so that real race conditions get created with very high probability and those races get resolved randomly at runtime. our approach has several advantages over existing dynamic analysis tools. first, we can create a real race condition and resolve the race randomly to see if an error can occur due to the race. second, we can replay a race revealing execution efficiently by simply using the same seed for random number generation--we do not need to record the execution. third, our approach has very low overhead compared to other precise dynamic race detection techniques because we only track all synchronization operations and a single pair of memory access statements that are reported to be in a potential race by an existing analysis. we have implemented the technique in a prototype tool for java and have experimented on a number of large multi-threaded java programs. we report a number of previously known and unknown bugs and real races in these java programs.
iterative optimization in the polyhedral model: part ii, multidimensional time. high-level loop optimizations are necessary to achieve good performance over a wide variety of processors. their performance impact can be significant because they involve in-depth program transformations that aim to sustain a balanced workload over the computational, storage, and communication resources of the target architecture. therefore, it is mandatory that the compiler accurately models the target architecture as well as the effects of complex code restructuring. however, because optimizing compilers (1) use simplistic performance models that abstract away many of the complexities of modern architectures, (2) rely on inaccurate dependence analysis, and (3) lack frameworks to express complex interactions of transformation sequences, they typically uncover only a fraction of the peak performance available on many applications. we propose a complete iterative framework to address these issues. we rely on the polyhedral model to construct and traverse a large and expressive search space. this space encompasses only legal, distinct versions resulting from the restructuring of any static control loop nest. we first propose a feedback-driven iterative heuristic tailored to the search space properties of the polyhedral model. though, it quickly converges to good solutions for small kernels, larger benchmarks containing higher dimensional spaces are more challenging and our heuristic misses opportunities for significant performance improvement. thus, we introduce the use of a genetic algorithm with specialized operators that leverage the polyhedral representation of program dependences. we provide experimental evidence that the genetic algorithm effectively traverses huge optimization spaces, achieving good performance improvements on large loop nests.
sharc: checking data sharing strategies for multithreaded c. unintended or unmediated data sharing is a frequent cause of insidious bugs in multithreaded programs. we present a tool called sharc (short for sharing checker) that allows a user to write lightweight annotations to declare how they believe objects are being shared between threads in their program. sharc uses a combination of static and dynamic analyses to check that the program conforms to this specification. sharc allows any type to have one of five "sharing modes" -- private to the current thread, read-only, shared under the control of a specified lock, intentionally racy, or checked dynamically. the dynamic mode uses run-time checking to verify that objects are either read-only, or only accessed by one thread. this allows us to check programs that would be difficult to check with a purely static system. if the user does not give a type an explicit annotation, then sharc uses a static type-qualifier analysis to infer that it is either private or should be checked dynamically. sharc allows objects to move between different sharing modes at runtime by using reference counting to check that there are no other references to the objects when they change mode. sharc's baseline dynamic analysis can check any c program, but is slow, and will generate false warnings about intentional data sharing. as the user adds more annotations, false warnings are reduced, and performance improves.we have found in practice that very few annotations are needed to describe all sharing and give reasonable performance. we ran sharc on 6 legacy c programs, summing to over 600k lines of code, and found that a total of only 60 simple annotations were needed to remove all false positives and to reduce performance overhead to only 2-14%.
velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. 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.
grammar-based whitebox fuzzing. 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.
an ant colony optimization approach to the probabilistic traveling salesman problem. the probabilistic traveling salesman problem (ptsp) is a tsp problem where each customer has a given probability of requiring a visit. the goal is to find an a-priori tour of minimal expected length over all customers, with the strategy of visiting a random subset of customers in the same order as they appear in the a-priori tour. we address the question of whether and in which context an a-priori tour found by a tsp heuristic can also be a good solution for the ptsp. we answer this question by testing the relative performance of two ant colony optimization algorithms, ant colony system (acs) introduced by dorigo and gambardella for the tsp, and a variant of it (pacs) which aims to minimize the ptsp objective function. we show in which probability configuration of customers pacs and acs are promising algorithms for the ptsp.
learning heuristics for obdd minimization by evolutionary algorithms. ordered binary decision diagrams (obdd) are the state-of-the-art data structure in cad for ics. obdds are very sensitive to the chosen variable ordering, i. e. the size may vary from linear to exponential. in this paper we present an evolutionary algorithm (ea) that learns good heuristics for obdd minimization starting from a given set of basic operations. the difference to other previous approaches to obdd minimization is that the ea does not solve the problem directly. instead, it develops strategies for solving the problem. to demonstrate the efficiency of our approach experimental results are given. the newly developed heuristics are more efficient than other previously presented methods.
an evolutive approach for the delineation of local labour markets. given a territory composed of basic geographical units, the delineation of local labour market areas (llmas) can be seen as a problem in which those units are grouped subject to multiple constraints. in previous research, standard genetic algorithms were not able to find valid solutions, and a specific evolutionary algorithm was developed. the inclusion of multiple ad hoc operators allowed the algorithm to find better solutions than those of a widely-used greedy method. the experimentation process showed that the rate of success of each operator in generating good individuals is different and evolves with time. we therefore propose different adaptive alternatives that modify the probabilities of application of each operator throughout the evolutionary process, and compare the results of such adaptive approaches with previous results and a greedy method.
implementation of standard genetic algorithm on mimd machines. genetic algorithms (gas) have been implemented on a number of multiprocessor machines. in many cases the ga has been adapted to the hardware structure of the system. this paper describes the implementation of a standard genetic algorithm on several mimd multiprocessor systems. it discusses the data dependencies of the different parts of the algorithm and the changes necessary to adapt the serial version to the parallel versions. timing measurements and speedups are given for a common problem implemented on all machines.
explicit filtering of building blocks for genetic algorithms. genetic algorithms are often applied to building block problems. we have developed a simple filtering algorithm that can locate building blocks within a bit-string, and does not make assumptions regarding the linkage of the bits. a comparison between the filtering algorithm and genetic algorithms reveals some interesting insights, and we discuss how the filtering algorithm can be used to build a powerful hybrid genetic algorithm.
evolutionary air traffic flow management for large 3d-problems. we present an evolutionary tool to solve free-route air traffic flow management problems within a three-dimensional air space. this is the first evolutionary tool which solves free-route planning problems involving a few hundred aircraft. we observe that the importance of the recombination operator increases as we scale to larger problem instances. the evolutionary algorithm is based on a variant of the elitist recombinationalgorithm. we show a theoretical analysis of the problem, and present the results of experiments.
nonsynonymous to synonymous substitution ratio ka/ks: measurement for rate of evolution in evolutionary computation. measuring fitness progression using numeric quantification in an evolutionary computation (ec) system may not be sufficient to capture the rate of evolution precisely. in this paper, we define the rate of evolution r e in an ec system based on the rate of efficient genetic variations being accepted by the ec population. this definition is motivated by the measurement of "amino acid to synonymous substitution ratio" k a/k s in biology, which has been widely accepted to measure the rate of gene sequence evolution. experimental applications to investigate the effects of four major configuration parameters on our rate of evolution measurement show that r e well reflects how evolution proceeds underneath fitness development and provides some insights into the effectiveness of ec parameters in evolution acceleration.
metaheuristics for group shop scheduling. the group shop scheduling problem (gsp) is a generalization of the classical job shop and open shop scheduling problems. in the gsp there are m machines and n jobs. each job consists of a set of operations, which must be processed on specified machines without preemption. the operations of each job are partitioned into groups on which a total precedence order is given. the problem is to order the operations on the machines and on the groups such that the maximal completion time (makespan) of all operations is minimized. the main goal of this paper is to provide a fair comparison of five metaheuristic approaches (i.e., ant colony optimization, evolutionary algorithm, iterated local search, simulated annealing, and tabu search) to tackle the gsp. we guarantee a fair comparison by a common definition of neighborhood in the search space, by using the same data structure, programming language and compiler, and by running the algorithms on the same hardware.