waashk/dblp huggingface dataset:
exochi: architecture and programming environment for a heterogeneous multi-core multithreaded system. future mainstream microprocessors will likely integrate specialized accelerators, such as gpus, onto a single die to achieve better performance and power efficiency. however, it remains a keen challenge to program such a heterogeneous multicore platform, since these specialized accelerators feature isas and functionality that are significantly different from the general purpose cpu cores. in this paper, we present exochi: (1) exoskeleton sequencer(exo), an architecture to represent heterogeneous acceleratorsas isa-based mimd architecture resources, and a shared virtual memory heterogeneous multithreaded program execution model that tightly couples specialized accelerator cores with generalpurpose cpu cores, and (2) c for heterogeneous integration(chi), an integrated c/c++ programming environment that supports accelerator-specific inline assembly and domain-specific languages. the chi compiler extends the openmp pragma for heterogeneous multithreading programming, and produces a single fat binary with code sections corresponding to different instruction sets. the runtime can judiciously spread parallel computation across the heterogeneous cores to optimize performance and power. we have prototyped the exo architecture on a physical heterogeneous platform consisting of an intel® core™ 2 duo processor and an 8-core 32-thread intel® graphics media accelerator x3000. in addition, we have implemented the chi integrated programming environment with the intel® c++ compiler, runtime toolset, and debugger. on the exo prototype system, we have enhanced a suite of production-quality media kernels for video and image processing to utilize the accelerator through the chi programming interface, achieving significant speedup (1.41x to10.97x) over execution on the ia32 cpu alone.
sound and precise analysis of web applications for injection vulnerabilities. web applications are popular targets of security attacks. one common type of such attacks is sql injection, where an attacker exploits faulty application code to execute maliciously crafted database queries. bothstatic and dynamic approaches have been proposed to detect or prevent sql injections; while dynamic approaches provide protection for deployed software, static approaches can detect potential vulnerabilities before software deployment. previous static approaches are mostly based on tainted information flow tracking and have at least some of the following limitations: (1) they do not model the precise semantics of input sanitization routines; (2) they require manually written specifications, either for each query or for bug patterns; or (3) they are not fully automated and may require user intervention at various points in the analysis. in this paper, we address these limitations by proposing a precise, sound, and fully automated analysis technique for sql injection. our technique avoids the need for specifications by consideringas attacks those queries for which user input changes the intended syntactic structure of the generated query. it checks conformance to this policy byconservatively characterizing the values a string variable may assume with a context free grammar, tracking the nonterminals that represent user-modifiable data, and modeling string operations precisely as language transducers. we have implemented the proposed technique for php, the most widely-used web scripting language. our tool successfully discovered previously unknown and sometimes subtle vulnerabilities in real-world programs, has a low false positive rate, and scales to large programs (with approx. 100k loc).
immix: a mark-region garbage collector with space efficiency, fast collection, and mutator performance. programmers are increasingly choosing managed languages for modern applications, which tend to allocate many short-to-medium lived small objects. the garbage collector therefore directly determines program performance by making a classic space-time tradeoff that seeks to provide space efficiency, fast reclamation, and mutator performance. the three canonical tracing garbage collectors: semi-space, mark-sweep, and mark-compact each sacrifice one objective. this paper describes a collector family, called mark-region, and introduces opportunistic defragmentation, which mixes copying and marking in a single pass. combining both, we implement immix, a novel high performance garbage collector that achieves all three performance objectives. the key insight is to allocate and reclaim memory in contiguous regions, at a coarse block grain when possible and otherwise in groups of finer grain lines. we show that immix outperforms existing canonical algorithms, improving total application performance by 7 to 25% on average across 20 benchmarks. as the mature space in a generational collector, immix matches or beats a highly tuned generational collector, e.g. it improves jbb2000 by 5%. these innovations and the identification of a new family of collectors open new opportunities for garbage collector design.
copy coalescing by graph recoloring. register allocation is always a trade-off between live-range splitting and coalescing. live-range splitting generally leads to less spilling at the cost of inserting shuffle code. coalescing removes shuffle code while potentially raising the register demand and causing spilling. recent research showed that the live-range splitting of the ssa form's æ-functions leads to chordal interference graphs. this improves upon two long-standing inconveniences of graph coloring register allocation: first, chordal graphs are optimally colorable in quadratic time. second, the number of colors needed to color the graph is equal to the maximal register pressure in the program. however, the inserted shuffle code incurred by the æ-functions can slow down the program severely. hence, to make such an approach work in practice, a coalescing technique is needed that removes most of the shuffle code without causing further spilling. in this paper, we present a coalescing technique designed for, but not limited to, ssa-form register allocation. we exploit that a valid coloring can be easily obtained by an ssa-based register allocator. this initial coloring is then improved by recoloring the interference graph and assigning shuffle-code related nodes the same color. thereby, we always keep the coloring of the graph valid. hence, the coalescing is safe, i. e. no spill code will be caused by coalescing. comparing to iterated register coalescing, the state of the art in safe coalescing, our method is able to remove 22.5% of the costs and 44.3% of the copies iterated coalescing left over. the best solution possible, found by a colaescer using integer linear programming (ilp), was 35.9% of the costs and 51.9% of the copies iterated coalescing left over. the runtime of programs compiled with our heuristic matches that of the programs compiled with the ilp technique.
checking race freedom via linear programming. we present a new static analysis for race freedom and race detection. the analysis checks race freedom by reducing the problem to (rational) linear programming. unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. we achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. this paper reports on the formal properties of the analysis and the experience with applying an implementation to real world c programs.
discovering properties about arrays in simple programs. array bound checking and array dependency analysis (for parallelization) have been widely studied. however, there are much less results about analyzing properties of array contents. in this paper, we propose a way of using abstract interpretation for discovering properties about array contents in some restricted cases: one-dimensional arrays, traversed by simple "for" loops. the basic idea, borrowed from [grs05], consists in partitioning arrays into symbolic intervals (e.g., [1,i -- 1], [i,i], [i + 1,n]), and in associating with each such interval i and each array a an abstract variable ai; the new idea is to consider relational abstract properties ψ(ai, bi, ...) about these abstract variables, and to interpret such a property pointwise on the interval i: ∀l ∈ i, ψ(a[l], b[l],...). the abstract semantics of our simple programs according to these abstract properties has been defined and implemented in a prototype tool. the method is able, for instance, to discover that the result of an insertion sort is a sorted array, or that, in an array traversal guarded by a "sentinel", the index stays within the bounds.
program analysis as constraint solving. a constraint-based approach to invariant generation in programs translates a program into constraints that are solved using off-the-shelf constraint solvers to yield desired program invariants. in this paper we show how the constraint-based approach can be used to model a wide spectrum of program analyses in an expressive domain containing disjunctions and conjunctions of linear inequalities. in particular, we show how to model the problem of context-sensitive interprocedural program verification. we also present the first constraint-based approach to weakest precondition and strongest postcondition inference. the constraints we generate are boolean combinations of quadratic inequalities over integer variables. we reduce these constraints to sat formulae using bitvector modeling and use off-the-shelf sat solvers to solve them. furthermore, we present interesting applications of the above analyses, namely bounds analysis and generation of most-general counter-examples for both safety and termination properties. we also present encouraging preliminary experimental results demonstrating the feasibility of our technique on a variety of challenging examples.
a practical automatic polyhedral parallelizer and locality optimizer. we present the design and implementation of an automatic polyhedral source-to-source transformation framework that can optimize regular programs (sequences of possibly imperfectly nested loops) for parallelism and locality simultaneously. through this work, we show the practicality of analytical model-driven automatic transformation in the polyhedral model -- far beyond what is possible by current production compilers. unlike previous works, our approach is an end-to-end fully automatic one driven by an integer linear optimization framework that takes an explicit view of finding good ways of tiling for parallelism and locality using affine transformations. the framework has been implemented into a tool to automatically generate openmp parallel code from c program sections. experimental results from the tool show very high speedups for local and parallel execution on multi-cores over state-of-the-art compiler frameworks from the research community as well as the best native production compilers. the system also enables the easy use of powerful empirical/iterative optimization for general arbitrarily nested loop sequences.
conditional correlation analysis for safe region-based memory management. region-based memory management is a popular scheme in systems software for better organization and performance. in the scheme, a developer constructs a hierarchy of regions of different lifetimes and allocates objects in regions. when the developer deletes a region, the runtime will recursively delete all its subregions and simultaneously reclaim objects in the regions. the developer must construct a consistent placement of objects in regions; otherwise, if a region that contains pointers to other regions is not always deleted before pointees, an inconsistency will surface and cause dangling pointers, which may lead to either crashes or leaks. this paper presents a static analysis tool regionwiz that can find such lifetime inconsistencies in large c programs using regions. the tool is based on an analysis framework that generalizes the relations and constraints over regions and objects as conditional correlations. this framework allows a succinct formalization of consistency rules for region lifetimes, preserving memory safety and avoiding dangling pointers. regionwiz uses these consistency rules to implement an efficient static analysis to compute the conditional correlation and reason about region lifetime consistency; the analysis is based on a context-sensitive, field-sensitive pointer analysis with heap cloning. experiments with applying regionwiz to six real-world software packages (including the rc compiler, apache web server, and subversion version control system) with two different region-based memory management interfaces show that regionwiz can reason about region lifetime consistency in large c programs. the experiments also show that regionwiz can find several previously unknown inconsistency bugs in these packages.
full functional verification of linked data structures. we present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. specifically, we present the use of the jahob verification system to verify formal specifications, written in classical higher-order logic, that completely capture the desired behavior of the java data structure implementations (with the exception of properties involving execution time and/or memory consumption). given that the desired correctness properties include intractable constructs such as quantifiers, transitive closure, and lambda abstraction, it is a challenge to successfully prove the generated verification conditions. our jahob verification system uses integrated reasoning to split each verification condition into a conjunction of simpler subformulas, then apply a diverse collection of specialized decision procedures, first-order theorem provers, and, in the worst case, interactive theorem provers to prove each subformula. techniques such as replacing complex subformulas with stronger but simpler alternatives, exploiting structure inherently present in the verification conditions, and, when necessary, inserting verified lemmas and proof hints into the imperative source code make it possible to seamlessly integrate all of the specialized decision procedures and theorem provers into a single powerful integrated reasoning system. by appropriately applying multiple proof techniques to discharge different subformulas, this reasoning system can effectively prove the complex and challenging verification conditions that arise in this context.
certifying low-level programs with hardware interrupts and preemptive threads. hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. handling interrupts properly is an essential component of low-level system programming. unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). existing formal verification techniques---including hoare logic, typed assembly language, concurrent separation logic, and the assume-guarantee method---have consistently ignored the issues of interrupts; this severely limits the applicability and power of today's program verification systems. in this paper we present a novel hoare-logic-like framework for certifying low-level system programs involving both hardware interrupts and preemptive threads. we show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. by carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to---for the first time---successfully certify a preemptive thread implementation and a large number of common synchronization primitives. our work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors.
path invariants. the success of software verification depends on the ability to find a suitable abstraction of a program automatically. we propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. in current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. by contrast, we view the cause of a false alarm -the spurious counterexample- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. there are two advantages to using such path programs as counterexamples for abstraction refinement. first, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. specifically, we use constraint-based invariant generation to automatically infer invariants of path programs-so-called path invariants. second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.
checkfence: checking consistency of concurrent data types on relaxed memory models. concurrency libraries can facilitate the development of multi-threaded programs by providing concurrent implementations of familiar data types such as queues or sets. there exist many optimized algorithms that can achieve superior performance on multiprocessors by allowing concurrent data accesses without using locks. unfortunately, such algorithms can harbor subtle concurrency bugs. moreover, they requirememory ordering fences to function correctly on relaxed memory models. to address these difficulties, we propose a verification approach that can exhaustively check all concurrent executions of a given test program on a relaxed memory model and can verify that they are observationally equivalent to a sequential execution. our checkfence prototype automatically translates the c implementation code and the test program into a sat formula, hands the latter to a standard sat solver, and constructs counter example traces if there exist incorrect executions. applying checkfence to five previously published algorithms, we were able to (1) find several bugs (some not previously known), and (2) determine how to place memory ordering fences for relaxed memory models.
certified self-modifying code. self-modifying code (smc), in this paper, broadly refers to anyprogram that loads, generates, or mutates code at runtime. it is widely used in many of the world's critical software systems tosupport runtime code generation and optimization, dynamic loading and linking, os boot loader, just-in-time compilation, binary translation,or dynamic code encryption and obfuscation. unfortunately, smc is alsoextremely difficult to reason about: existing formal verification techniques-including hoare logic and type system-consistentlyassume that program code stored in memory is fixedand immutable; this severely limits their applicability and power. this paper presents a simple but novel hoare-logic-like framework that supports modular verification of general von-neumann machine code with runtime code manipulation. by dropping the assumption that code memory is fixed and immutable, we are forced to apply local reasoningand separation logic at the very beginning, and treat program code uniformly as regular data structure. we address the interaction between separation and code memory and show how to establish the frame rules for local reasoning even in the presence of smc. our frameworkis realistic, but designed to be highly generic, so that it can support assembly code under all modern cpus (including both x86 andmips). our system is expressive and fully mechanized. we prove itssoundness in the coq proof assistant and demonstrate its power by certifying a series of realistic examples and applications-all of which can directly run on the spim simulator or any stock x86 hardware.
practical memory leak detection using guarded value-flow analysis. this paper presents a practical inter-procedural analysis algorithm for detecting memory leaks in c programs. our algorithm tracks the flow of values from allocation points to deallocation points using a sparse representation of the program consisting of a value flow graph that captures def-use relations and value flows via program assignments. edges in the graph are annotated with guards that describe branch conditions in the program. the memory leak analysis is reduced to a reachability problem over the guarded value flowgraph. our implemented tool has been effective at detecting more than 60 memory leaks in the spec2000 benchmarks and in two open-source applications, bash and sshd, while keeping the false positive rate below 20%. the sparse program representation makes the tool efficient in practice, and allows it to report concise error messages.
a certified type-preserving compiler from lambda calculus to assembly language. we present a certified compiler from the simply-typed lambda calculus to assembly language. the compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the coq proof assistant. the compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. semantics preservation is proved based on denotational semantics assigned to the intermediate languages. we demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.
proving thread termination. concurrent programs are often designed such that certain functions executing within critical threads must terminate. examples of such cases can be found in operating systems, web servers, e-mail clients, etc. unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. in this paper we describe such a procedure. the procedure's scalability is achieved through the use of environment models that abstract away the surrounding threads. the procedure's accuracy is due to a novel method of incrementally constructing environment abstractions. our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. the paper gives a description of experimental results using an implementation of our procedureon windows device drivers and adescription of a previously unknown bug found withthe tool.