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.
7,482 papers · page 227 of 375
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.
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 …
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…
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 summar…
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 s…
Quantitative information flow as network flow capacity
Abstract We present a new technique for determining how much informationabout a program's secret inputs is revealed by its public outputs. In
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 ar…
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, …
A study of concurrent real-time garbage collectors
Concurrent garbage collection is highly attractive for real-time systems, because offloading the collection effort from the executing threads allows faster response, allowing for extremely short deadlines at the microseconds level. Concurrent collectors also offer much better sca…
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, an…
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…
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 …
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. Th…
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 loc…
Deriving linearizable fine-grained concurrent objects
Practical and efficient algorithms for concurrent data structures are difficult to construct and modify. Algorithms in the literature are often optimized for a specific setting, making it hard to separate the algorithmic insights from implementation details. The goal of this work…
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 w…
XMem: type-safe, transparent, shared memory for cross-runtime communication and coordination
Developers commonly build contemporary enterprise applications using type-safe, component-based platforms, such as J2EE, and architect them to comprise multiple tiers, such as a web container, application server, and database engine. Administrators increasingly execute each tier …
Efficient program execution indexing
Execution indexing uniquely identifies a point in an execution. Desirable execution indices reveal correlations between points in an execution and establish correspondence between points across multiple executions. Therefore, execution indexing is essential for a wide variety of …
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, writt…