No subject

This talk presents a very high-level language for clear description of
distributed algorithms, compilation to executable code, and
optimizations necessary for generating efficient implementations. =C2=A0The
language supports high-level control flows where complex
synchronization conditions can be expressed using high-level queries,
especially logic quantifications, over message history sequences.
Unfortunately, these programs would be extremely inefficient,
including consuming unbounded memory, if executed straightforwardly.

We present new optimizations that automatically transform complex
synchronization conditions into incremental updates of necessary
auxiliary values as messages are sent and received. =C2=A0The core of the
optimizations is the first general method for transforming logic
quantifications into efficient implementations. =C2=A0We have developed an
operational semantics of the language, implemented a prototype of the
compiler and the optimizations, and successfully used the language and
implementation on a variety of important distributed algorithms,
including multi-Paxos for distributed consensus.

Our high-level specification and optimization method also helped us
discover improvements to some of the algorithms, both for correctness
and for optimizations. =C2=A0Our language has also been used by
undergraduate and graduate students to easily implement a variety of
distributed algorithms used in distributed file sharing, routing,
etc., including Chord, Kademlia, Pastry, and Tapestry, AODV, and parts
of HDFS and Upright.

(Joined work with Scott Stoller, Bo Lin, and Michael Gorbovitski)


Sebastien Mondet, Ashish Agarwal, Paul Scheid, Aviv Madar, Richard
Bonneau, Jane Carlton, Kristin C. Gunsalus
Managing and Analyzing Big-Data in Genomics

Biology is an increasingly computational discipline. Rapid advances in
experimental techniques, especially DNA sequencing, are generating data at
exponentially increasing rates. Aside from the algorithmic challenges this
poses, researchers must manage large volumes and innumerable varieties of
data, run computational jobs on an HPC cluster, and track the
inputs/outputs of the numerous computational tools they employ. Here we
describe a software stack fully implemented in OCaml that operates the
Genomics Core Facility at NYU=C3=94=C3=A6=C3=AFs Center for Genomics and Sy=
stems Biology.

We define a domain specific language (DSL) that allows us to easily
describe the data we need to track. More importantly, the DSL approach
provides us with code generation capabilities. From a single description,
we generate PostgreSQL schema definitions, OCaml bindings to the database,
and web pages and forms for end-users to interact with the database.
Strong type safety is provided at each stage. Database bindings check
properties not expressible in SQL, and web pages, forms, and links are
validated at compile time by the Ocsigen framework. Since the entire stack
depends on this single data description, rapid updates are easy; the
compiler informs us of all necessary changes.

The application launches compute intensive jobs on a high-performance
compute (HPC) cluster, requiring consideration of concurrency and
fault-tolerance. We have implemented what we call a =C3=94=C3=A6=C3=ADflow=
=C3=94=C3=A6=C3=AC monad that
combines error and thread monads. Errors are modeled with polymorphic
variants, which get arranged automatically into a hierarchical structure
from lower level system calls to high level functions. The net result is
extremely precise information in the case of any failures and reasonably
straightforward concurrency management.


1:40-2:55 Program Analysis and Verification
(3 25-minute slots)

J. Ian Johnson
Designing Precise Higher-Order Pushdown Flow Analyses

Formalisms for context-free approaches to higher-order control-flow
analysis are complex and require significant effort to prove correct.
However, these approaches are enticing because they provide improved
precision over finite state approaches. We present a new method for
deriving context-free analyses that results in =E2=88=9A=C3=ADobviously cor=
rect=E2=88=9A=C3=AC
formalisms that consists of making small changes to the original concrete
semantics. We validate this method by using it to derive existing
context-free analyses from abstract machines. We further exercise the
technique by applying it to abstract machines that more closely represent
real language implementations and consequently derive analyses more
precise than existing ones. Specifically, we use an escape analysis to
derive better stack allocation, and use garbage collection to derive
better heap allocation. We also present a novel semantics for call/cc
that, when turned into an analysis, handles non-escaping continuations
more precisely than prior treatments of first-class control.


Eric Koskinen
Temporal property verification as a program analysis task

We describe a reduction from temporal property verification to a program
analysis problem. We produce an encoding which, with the use of recursion
and nondeterminism, =C2=A0enables off-the-shelf program analysis tools to
naturally perform the reasoning necessary for proving temporal properties
(e.g. =C2=A0backtracking, eventuality checking, tree counterexamples for
branching-time properties, abstraction refinement, etc.). This reduction
allows us to prove branching-time properties of programs, as well as
trace-based properties such as those expressed in Linear Temporal Logic
(LTL) when the reduction is combined with our recently described iterative
symbolic determinization procedure. We demonstrate---using examples taken
from the PostgreSQL database server, Apache web server, and Windows OS
kernel---that our method can yield enormous performance improvements in
comparison to known tools, allowing us to automatically prove properties
of programs where we could not prove them before.



Gregory Malecha, Adam Chlipala, Patrick Hulin, and Edward Yang
A Framework for Verifying Low-level Programs

=C2=A0High level languages provide abstractions that assist programmers;
however these abstractions are not always su=C3=94=C2=A8=C3=89cient and, in=
 some cases,
they get in the way of writing e=C3=94=C2=A8=C3=89cient or functioning corr=
ect code. In
this work we develop Bedrock2, a Coq framework for foundational
reasoning about low-level pro- grams using a program logic based on Ni
and Shao=E2=80=9A=C3=84=C3=B4s XCAP [2]. Bedrock2 is an extension and rewri=
te of
Chlipala=E2=80=9A=C3=84=C3=B4s Bedrock language [1]. =C2=A0Bedrock2 allows =
programmers to de=C3=94=C2=A8=C3=85ne
both control and data abstractions and integrate them into the system
in a =C3=94=C2=A8=C3=85rst-class way. Control abstractions, e.g. conditiona=
ls and
function calls, are de=C3=94=C2=A8=C3=85ned by providing a denotation into =
the core
language and derived inference rules are veri=C3=94=C2=A8=C3=85ed in a foun=
dational way
with respect to the core language semantics. These inference rules are
used by the veri=C3=94=C2=A8=C3=85cation condition generator simplify the p=
roof
obligations provided to the programmer. Veri=C3=94=C2=A8=C3=85cation condit=
ions are
expressed as pre- and post- conditions on execution traces allowing
the bulk of the work to be done by symbolic evaluation. Unlike
Bedrock, the Bedrock2 symbolic evaluator incorpo- rates user-de=C3=94=C2=A8=
=C3=85ned
abstract predicates to enable e=C3=94=C2=A8=C3=89cient manipulation of arra=
ys,
structures, stack frames, and other data abstractions. Final
veri=C3=94=C2=A8=C3=85cation condi- tions are discharged using a cancellati=
on-based
separation logic prover. Proofs are generated using computational
re=C3=94=C2=A8=C3=87ection to enable good performance that, experiences sug=
gest, will
scale to larger programs than previous work. Bedrock2 embraces a more
realistic machine model that exposes machine word sizes, byte
ordering, and =C3=94=C2=A8=C3=85nite memory. We are working to extend the l=
anguage to
more interesting abstractions, real assembly languages, and
concurrency.


3:10-4:00 Runtime Issues
(2 25-minute slots)

Kangkook Jee
A General Approach for Efficiently Accelerating Software-based Dynamic
Data Flow Tracking on Commodity Hardware

=C2=A0Despite the demonstrated usefulness of dynamic data flow tracking
(DDFT) techniques in a variety of security applications, the poor
performance achieved by available prototypes prevents their widespread
adoption and use in production systems. We present and evaluate a
novel methodology for improving the performance overhead of DDFT
frameworks, by combining static and dynamic analysis. Our intuition is
to separate the program logic from the corresponding tracking logic,
extracting the semantics of the latter and abstracting them using a
Taint Flow Algebra. We then apply optimization techniques to eliminate
redundant tracking logic and minimize interference with the target
program. Our optimizations are directly applicable to binary-only
software and do not require any high level semantics. Furthermore,
they do not require additional resources to improve performance,
neither do they restrict or remove functionality. =C2=A0Most importantly,
our approach is orthogonal to optimizations devised in the past, and
can deliver additive performance benefits. We extensively evaluate the
correctness and impact of our optimizations, by augmenting a freely
available high-performance DDFT framework, and applying it to multiple
applications, including command line utilities, server applications,
language runtimes, and web browsers. Our results show a speedup of
DDFT by as much as 2:23x, with an average of 1:72x across all tested
applications.


Jose Castanos, David Edelsohn, Kazuaki Ishizaki,Toshio Nakatani,
Takeshi Ogasawara, Priya Nagpurkar, Peng Wu
On the Benefits and Pitfalls of Extending a Statically Typed Language
JIT Compiler for Dynamic Scripting Languages

Whenever the need to compile a new dynamically typed language arises, the
option of reusing an existing statically typed language Just-In-Time (JIT)
compiler (reusing JITs) always seems appealing. Existing reusing JITs,
however, do not deliver the kind of performance boost as proponents have
hoped. =C2=A0The performance of JVM languages, for instance, often lags beh=
ind
standard interpreter implementations. Even more customized solutions that
extend the internals of a JIT compiler for the target language cannot
compete with those designed specifically for dynamically typed languages.
Our own Fiorano JIT compiler is a living example of such a phenomenon. As
a state-of-the-art reusing JIT compiler for Python, Fiorano JIT compiler
outperforms two other reusing JITs (Unladen Swallow and Jython), but still
has a noticeable performance gap with PyPy, the best performing Python JIT
compiler today.

In this talk, we offer an in-depth look on the reusing JITs phenomenon.
Based on our Fiorano JIT experience and evaluation of PyPy, Jython,
Fiorano JIT, and Unalden-swallow JIT, we discuss techniques that have
proved effective and quantify weakness of the reusing JIT approach. =C2=A0 =
More
importantly, we identify several common pitfalls of today's reusing JITs,
the most important one of them is not focusing sufficiently on
specialization, an abundant optimization opportunity unique to dynamically
typed languages. These findings, though presented in the context of
Python, are applicable to other scripting languages as well.