28 Result(s)
within
Chapter
Alex Aiken
English
-
Chapter and Conference Paper
Speaking Pygion: Experiences Writing an Exascale Single Particle Imaging Code
The goal of the SpiniFEL project was to write, from scratch, a single particle imaging code for exascale supercomputers. The original vision was to have two versions of the code, one in MPI and one in Pygion, ...
-
Chapter and Conference Paper
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a bread...
-
Chapter
Introduction
This introductory chapter discusses the role of instruction level parallelism (ILP) in optimizing compilers and in machine architectures that automatically reorder or parallelize programs. A brief overview of ...
-
Chapter
Percolation Scheduling
Trace scheduling suffers from a number of problems related to its focus on a single trace at a time. Percolation scheduling overcomes these problems, to the extent possible at compile time, by providing a smal...
-
Chapter
Epilogue
This book focuses on compiler-managed instruction level parallelism. While a great deal of the work on this topic has been only touched upon or mentioned only in references, the book does cover all of the majo...
-
Chapter
Scheduling Basic Blocks
A basic block in a program is a sequence of consecutive operations, such that control flow enters at the beginning and leaves at the end without internal branches. While basic block scheduling is the simplest ...
-
Chapter
Software Pipelining by Kernel Recognition
Kernel recognition techniques avoid the search for an appropriate initiation interval by dealing directly with a representation of the unrolled loop and its compaction. Intuitively, kernel recognition tries to...
-
Chapter
Overview of ILP Architectures
In this chapter we trace the history of computer architecture, focusing on the evolution of techniques for instruction-level parallelism. After briefly summarizing the early years of machine design, we focus o...
-
Chapter
Trace Scheduling
Since its introduction by Joseph A. Fisher in 1979, trace scheduling has influenced much of the work on compile-time ILP. Initially developed for use in microcode compaction, trace scheduling quickly became th...
-
Chapter
Modulo Scheduling
Loop parallelization, and particularly the parallelization of innermost loops, is the most critical aspect of any parallelizing compiler. Trace scheduling can be applied to loops, but has the disadvantage that...
-
Chapter and Conference Paper
From Invariant Checking to Invariant Inference Using Randomized Search
We describe a general framework c2i for generating an invariant inference procedure from an invariant checking procedure. Given a checker and a language of possible invariants, c2i generates an inference procedur...
-
Chapter and Conference Paper
Verification as Learning Geometric Concepts
We formalize the problem of program verification as a learning problem, showing that invariants in program verification can be regarded as geometric concepts in machine learning. Safety properties define bad stat...
-
Chapter and Conference Paper
A Data Driven Approach for Algebraic Loop Invariants
We describe a Guess-and-Check algorithm for computing algebraic equation invariants of the form ∧ i f i (x ...
-
Chapter and Conference Paper
Minimum Satisfying Assignments for SMT
A minimum satisfying assignment of a formula is a minimum-cost partial assignment of values to the variables in the formula that guarantees the formula is true. Minimum satisfying assignments have applications in...
-
Chapter and Conference Paper
Interpolants as Classifiers
We show how interpolants can be viewed as classifiers in supervised machine learning. This view has several advantages: First, we are able to use off-the-shelf classification techniques, in particular support ...
-
Chapter and Conference Paper
Reasoning about Lock Placements
A lock placement describes, for each heap location, which lock guards the location, and under what circumstances. We formalize methods for reasoning about lock placements, making precise the interactions between ...
-
Chapter and Conference Paper
Simplifying Loop Invariant Generation Using Splitter Predicates
We present a novel static analysis technique that substantially improves the quality of invariants inferred by standard loop invariant generation techniques. Our technique decomposes multi-phase loops, which requ...
-
Chapter and Conference Paper
Community Epidemic Detection Using Time-Correlated Anomalies
An epidemic is malicious code running on a subset of a community, a homogeneous set of instances of an application. Syzygy is an epidemic detection framework that looks for time-correlated anomalies, i.e., diverg...
-
Chapter and Conference Paper
Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
Static analysis techniques that represent program states as formulas typically generate a large number of redundant formulas that are incrementally constructed from previous formulas. In addition to querying s...
-
Chapter and Conference Paper
Fluid Updates: Beyond Strong vs. Weak Updates
We describe a symbolic heap abstraction that unifies reasoning about arrays, pointers, and scalars, and we define a fluid update operation on this symbolic heap that relaxes the dichotomy between strong and weak ...
