waashk/dblp huggingface dataset:
offline compression for on-chip ram. we present offline ram compression, an automated source-to-source transformation that reduces a program's data size. statically allocated scalars, pointers, structures, and arrays are encoded and packed based on the results of a whole-program analysis in the value set and pointer set domains. we target embedded software written in c that relies heavily on static memory allocation and runs on harvard-architecture microcontrollers supporting just a few kb of on-chip ram. on a collection of embedded applications for avr microcontrollers, our transformation reduces ram usage by an average of 12%, in addition to a 10% reduction through a dead-data elimination pass that is also driven by our whole-program analysis, for a total ram savings of 22%. we also developeda technique for giving developers access to a flexible spectrum of tradeoffs between ram consumption, rom consumption, and cpu efficiency. this technique is based on a model for estimating the cost/benefit ratio of compressing each variable and then selectively compressing only those variables that present a good value proposition in terms of the desired tradeoffs.
static error detection using semantic inconsistency inference. inconsistency checking is a method for detecting software errors that relies only on examining multiple uses of a value. we propose that inconsistency inference is best understood as a variant of the older and better understood problem of type inference. using this insight, we describe a precise and formal framework for discovering inconsistency errors. unlike previous approaches to the problem, our technique for finding inconsistency errors is purely semantic and can deal with complex aliasing and path-sensitive conditions. we have built a nullde reference analysis of c programs based on semantic inconsistency inference and have used it to find hundreds of previously unknown null dereference errors in widely used c programs.
software behavior oriented parallelization. many sequential applications are difficult to parallelize because of unpredictable control flow, indirect data access, and input-dependent parallelism. these difficulties led us to build a software system for behavior oriented parallelization (bop), which allows a program to be parallelized based on partial information about program behavior, for example, a user reading just part of the source code, or a profiling tool examining merely one or few executions. the basis of bop is programmable software speculation, where a user or an analysis tool marks possibly parallel regions in the code, and the run-time system executes these regions speculatively. it is imperative to protect the entire address space during speculation. the main goal of the paper is to demonstrate that the general protection can be made cost effective by three novel techniques: programmable speculation, critical-path minimization, and value-based correctness checking. on a recently acquired multi-core, multi-processor pc, the bop system reduced the end-to-end execution time by integer factors for a lisp interpreter, a data compressor, a language parser, and a scientific library, with no change to the underlying hardware or operating system.
goldilocks: a race and transaction-aware java runtime. data races often result in unexpected and erroneous behavior. in addition to causing data corruption and leading programs to crash, the presence of data races complicates the semantics of an execution which might no longer be sequentially consistent. motivated by these observations, we have designed and implemented a java runtime system that monitors program executions and throws a dataraceexception when a data race is about to occur. analogous to other runtime exceptions, the dataraceexception provides two key benefits. first, accesses causing race conditions are interruptedand handled before they cause errors that may be difficult to diagnose later. second, if no dataraceexception is thrown in an execution, it is guaranteed to be sequentially consistent. this strong guarantee helps to rule out many concurrency-related possibilities as the cause of erroneous behavior. when a dataraceexception is caught, the operation, thread, or program causing it can be terminated gracefully. alternatively, the dataraceexception can serve as a conflict-detection mechanism inoptimistic uses of concurrency. we start with the definition of data-race-free executions in the java memory model. we generalize this definition to executions that use transactions in addition to locks and volatile variables for synchronization. we present a precise and efficient algorithm for dynamically verifying that an execution is free of data races. this algorithm generalizes the goldilocks algorithm for data-race detectionby handling transactions and providing the ability to distinguish between read and write accesses. we have implemented our algorithm and the dataraceexception in the kaffe java virtual machine. we have evaluated our system on a variety of publicly available java benchmarks and a few microbenchmarks that combine lock-based and transaction-based synchronization. our experiments indicate that our implementation has reasonable overhead. therefore, we believe that inaddition to being a debugging tool, the dataraceexception may be a viable mechanism to enforce the safety of executions of multithreaded java programs.
liquid types. we present logically qualified data types, abbreviated to liquid types, a system that combines hindley-milner type inference with predicate abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation. we have implemented liquid type inference in dsolve, which takes as input an ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the ocaml program. to demonstrate the utility of our approach, we describe experiments using dsolve to statically verify the safety of array accesses on a set of ocaml benchmarks that were previously annotated with dependent types as part of the dml project. we show that when used in conjunction with a fixed set of array bounds checking qualifiers, dsolve reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%.
efficient static analysis of xml paths and types. we present an algorithm to solve xpath decision problems under regular tree type constraints and show its use to statically type-check xpath queries. to this end, we prove the decidability of a logic with converse for finite ordered trees whose time complexity is a simple exponential of the size of a formula. the logic corresponds to the alternation free modal μ-calculus without greatest fixpoint, restricted to finite trees, and where formulas are cycle-free. our proof method is based on two auxiliary results. first, xml regular tree types and xpath expressions have a linear translation to cycle-free formulas. second, the least and greatest fixpoints are equivalent for finite trees, hence the logic is closed under negation. building on these results, we describe a practical, effective system for solving the satisfiability of a formula. the system has been experimented with some decision problems such as xpath emptiness, containment, overlap, and coverage, with or without type constraints. the benefit of the approach is that our system can be effectively used in static analyzers for programming languages manipulating both xpath expressions and xml type annotations (as input and output types).
thread-modular shape analysis. we present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. this allows us to use a sequential shape analysis on each thread. we show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from windows device drivers.
shape analysis with inductive recursion synthesis. separation logic with recursively defined predicates allows for concise yet precise description of the shapes of data structures. however, most uses of separation logic for program analysis rely on pre-defined recursive predicates, limiting the class of programs analyzable to those that manipulate only a priori data structures. this paper describes a general algorithm based on inductive program synthesis that automatically infers recursive shape invariants, yielding a shape analysis based on separation logic that can be applied to any program. a key strength of separation logic is that it facilitates, via explicit expression of structural separation, local reasoning about heap where the effects of altering one part of a data structure are analyzed in isolation from the rest. the interaction between local reasoning and the global invariants given by recursive predicates is a difficult area, especially in the presence of complex internal sharing in the data structures. existing approaches, using logic rules specifically designed for the list predicate to unfold and fold linked-lists, again require a priori knowledge about the shapes of the data structures and do not easily generalize to more complex data structures. we introduce a notion of "truncation points" in a recursive predicate, which gives rise to generic algorithms for unfolding and folding arbitrary data structures.
the ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code. pointer information is a prerequisite for most program analyses, and the quality of this information can greatly affect their precision and performance. inclusion-based (i.e. andersen-style) pointer analysis is an important point in the space of pointer analyses, offering a potential sweet-spot in the trade-off between precision and performance. however, current techniques for inclusion-based pointer analysis can have difficulties delivering on this potential. we introduce and evaluate two novel techniques for inclusion-based pointer analysis---one lazy, one eager1---that significantly improve upon the current state-of-the-art without impacting precision. these techniques focus on the problem of online cycle detection, a critical optimization for scaling such analyses. using a suite of six open-source c programs, which range in size from 169k to 2.17m loc, we compare our techniques against the three best inclusion-based analyses--described by heintze and tardieu [11], by pearce et al. [21], and by berndl et al. [4]. the combination of our two techniques results in an algorithm which is on average 3.2 xfaster than heintze and tardieu's algorithm, 6.4 xfaster than pearce et al.'s algorithm, and 20.6 faster than berndl et al.'s algorithm. we also investigate the use of different data structures to represent points-to sets, examining the impact on both performance and memory consumption. we compare a sparse-bitmap implementation used in the gcc compiler with a bdd-based implementation, and we find that the bdd implementation is on average 2x slower than using sparse bitmaps but uses 5.5x less memory.
quantitative information flow as network flow capacity. we present a new technique for determining how much information about a program's secret inputs is revealed by its public outputs. in contrast to previous techniques based on reachability from secret inputs (tainting), it achieves a more precise quantitative result by computing a maximum flow of information between the inputs and outputs. the technique uses static control-flow regions to soundly account for implicit flows via branches and pointer operations, but operates dynamically by observing one or more program executions and giving numeric flow bounds specific to them (e.g., "17 bits"). the maximum flow in a network also gives a minimum cut (a set of edges that separate the secret input from the output), which can be used to efficiently check that the same policy is satisfied on future executions. we performed case studies on 5 real c, c++, and objective c programs, 3 of which had more than 250k lines of code. the tool checked multiple security policies, including one that was violated by a previously unknown bug.
fair stateless model checking. stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. existing stateless model checkers are limited to the verification of safety properties on terminating programs. however, realistic concurrent programs are nonterminating, a property that significantly reduces the efficacy of stateless model checking in testing them. moreover, existing stateless model checkers are unable to verify that a nonterminating program satisfies the important liveness property of livelock-freedom, a property that requires the program to make continuous progress for any input. to address these shortcomings, this paper argues for incorporating a fair scheduler in stateless exploration. the key contribution of this paper is an explicit scheduler that is (strongly) fair and at the same time sufficiently nondeterministic to guarantee full coverage of safety properties.we have implemented the fair scheduler in the chess model checker. we show through theoretical arguments and empirical evaluation that our algorithm satisfies two important properties: 1) it visits all states of a finite-state program achieving state coverage at a faster rate than existing techniques, and 2) it finds all livelocks in a finite-state program. before this work, nonterminating programs had to be manually modified in order to apply chess to them. the addition of fairness has allowed chess to be effectively applied to real-world nonterminating programs without any modification. for example, we have successfully booted the singularity operating system under the control of chess.
mace: language support for building distributed systems. building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment where these systemsmust run. tools for building distributed systems must strike a compromise between reducing programmer effort and increasing system efficiency. we present mace, a c++ language extension and source-to-source compiler that translates a concise but expressive distributed system specification into a c++ implementation. mace overcomes the limitations of low-level languages by providing a unified framework for networking and event handling, and the limitations of high-level languages by allowing programmers to write program components in a controlled and structured manner in c++. by imposing structure and restrictions on how applications can be written, mace supports debugging at a higher level, including support for efficient model checking and causal-path debugging. because mace programs compile to c++, programmers can use existing c++ tools, including optimizers, profilers, and debuggers to analyze their systems.
regularly annotated set constraints. a general class of program analyses area combination of context-free and regular language reachability. we define regularly annotated set constraints, a constraint formalism that captures this class. our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.
reliable and efficient programming abstractions for wireless sensor networks. it is currently difficult to build practical and reliable programming systems out of distributed and resource-constrained sensor devices. the state of the art in today's sensornet programming is centered around a component-based language called nesc. nesc is a node-level language-a program is written for an individual node in the network-and nesc programs use the services of an operating system called tinyos. we are pursuing an approach to programming sensor networks that significantly raises the level of abstraction over this practice. the critical change is one of perspective: rather than writing programs from the point of view of an individual node, programmers implement a central program that conceptually has access to the entire network. this approach pushes to the compiler the task of producing node-level programs that implement the desired behavio. we present the pleiades programming language, its compiler, and its runtime. the pleiades language extends the c language with constructs that allow programmers to name and access node-local state within the network and to specify simple forms of concurrent execution. the compiler and runtime system cooperate to implement pleiades programs efficiently and reliably. first, the compiler employs a novel program analysis to translate pleiades programs into message-efficient units of work implemented in nesc. the pleiades runtime system orchestrates execution of these units, using tinyos services, across a network of sensor nodes. second, the compiler and runtime system employ novel locking, deadlock detection, and deadlock recovery algorithms that guarantee serializability in the face of concurrent execution. we illustrate the readability, reliability and efficiency benefits of the pleiades language through detailed experiments, and demonstrate that the pleiades implementation of a realistic application performs similar to a hand-coded nesc version that contains more than ten times as much code.
expressive and safe static reflection with morphj. recently, language extensions have been proposed for java and c# to support pattern-based reflective declaration. these extensions introduce a disciplined form of meta-programming and aspect-oriented programming to mainstream languages: they allow members of a class (i.e., fields and methods) to be declared by statically iterating over and pattern-matching on members of other classes. such techniques, however, have been unable to safely express simple, but common, idioms such as declaring getter and setter methods for fields. in this paper, we present a mechanism that addresses the lack of expressiveness in past work without sacrificing safety. our technique is based on the idea of nested patterns that elaborate the outer-most pattern with blocking or enabling conditions. we implemented this mechanism in a language, morphj. we demonstrate the expressiveness of morphj with real-world applications. in particular, the morphj reimplementation of dstm2, a software transactional memory library, reduces 1,107 lines of java reflection and bytecode engineering library calls to just 374 lines of morphj code. at the same time, the morphj solution is both high level and safer, as morphj can separately type check generic classes and catch errors early. we present and formalize the morphj type system, and offer a type-checking algorithm.
explaining failures of program analyses. with programs getting larger and often more complex with each new release, programmers need all the help they can get in understanding and transforming programs. fortunately, modern development environments, such as eclipse, incorporate tools for understanding, navigating, and transforming programs. these tools typically use program analyses to extract relevant properties of programs. these tools are often invaluable to developers; for example, many programmers use refactoring tools regularly. however, poor results by the underlying analyses can compromise a tool's usefulness. for example, a bug finding tool may produce too many false positives if the underlying analysis is overly conservative, and thus overwhelm the user with too many possible errors in the program. in such cases it would be invaluable for the tool to explain to the user why it believes that each bug exists. armed with this knowledge, the user can decide which bugs are worth pursing and which are false positives. the contributions of this paper are as follows: (i) we describe requirements on the structure of an analysis so that we can produce reasons when the analysis fails; the user of the analysis determines whether or not an analysis's results constitute failure. we also describe a simple language that enforces these requirements; (ii) we describe how to produce necessary and sufficient reasons for analysis failure; (iii) we evaluate our system with respect to a number of analyses and programs and find that most reasons are small (and thus usable) and that our system is fast enough for interactive use.
sketching concurrent data structures. we describe psketch, a program synthesizer that helps programmers implement concurrent data structures. the system is based on the concept of sketching, a form of synthesis that allows programmers to express their insight about an implementation as a partial program: a sketch. the synthesizer automatically completes the sketch to produce an implementation that matches a given correctness criteria. psketch is based on a new counterexample-guided inductive synthesis algorithm (cegis) that generalizes the original sketch synthesis algorithm from solar-lezama et.al. to cope efficiently with concurrent programs. the new algorithm produces a correct implementation by iteratively generating candidate implementations, running them through a verifier, and if they fail, learning from the counterexample traces to produce a better candidate; converging to a solution in a handful of iterations. psketch also extends sketch with higher-level sketching constructs that allow the programmer to express her insight as a "soup" of ingredients from which complicated code fragments must be assembled. such sketches can be viewed as syntactic descriptions of huge spaces of candidate programs (over 108 candidates for some sketches we resolved). we have used the psketch system to implement several classes of concurrent data structures, including lock-free queues and concurrent sets with fine-grained locking. we have also sketched some other concurrent objects including a sense-reversing barrier and a protocol for the dining philosophers problem; all these sketches resolved in under an hour.