IBM PL Day

gistfile1.txt

 The 2012 Programming Languages Day will be held at the IBM Thomas J.
Watson Research Center on Thursday, June 28, 2012. The day will be held in
cooperation with the New Jersey and New England Programming Languages and
Systems Seminars. The main goal of the event is to increase awareness of
each other's work, and to encourage interaction and collaboration.

 The Programming Languages Day features a keynote presentation and 8
regular presentations.  Dr. Shriram Krishnamurthi of Brown University
will deliver the keynote presentation this year, "Securing JavaScript
on the Web".   Details of the program are below.

 You are welcome from 9AM onwards, and the keynote presentation will start
at 10AM sharp. We expect the program to run until 4PM.  Programming
Languages day will be held in the Auditorium (room GN-F15) in the
Hawthorne-1 building of the Thomas J. Watson Research Center at 19
Skyline Drive, Hawthorne, New York 10538.

 If you plan to attend the Programming Languages Day, please register by
sending an e-mail with your name, affiliation, and contact information to
[email protected].  It is important that everyone register in advance,
since security regulations at Watson require us to provide a list of
attendees in advance; also, registering enables us to plan for lunch
and refreshments to be  available.

 If you plan to attend, please let me know ideally by JUNE 8, but no
later than JUNE 14 (2 weeks before the event).

 Please note that we are currently have trouble with the Web site that
hosts the PL Day 2012 page.  I shall send further mail when the
situation with the Web site has been resolved.

-------------------------------------------------------
                                       Program Overview

9:00-10:00 Sign-in, Welcome

10:00-11:00 Keynote
Shriram Krishnamurthi
Securing JavaScript on the Web

11:00-11:15 Break

11:15-12:30 Concurrency
(3 25-minute slots)

Stephen Freund
Cooperative Concurrency for a Multicore World

Y. Annie Liu
From Clarity to Efficiency for Distributed Algorithms

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


12:30-1:40 Lunch


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

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

Eric Koskinen
Temporal property verification as a program analysis task

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


2:55-3:10 Break


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

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

-------------------------------------------------------
                                       Program Details

10:00-11:00 Keynote
Shriram Krishnamurthi
Securing JavaScript on the Web

JavaScript is the principal language for Web clients.  It powers both
the content of pages and, in many cases, the browser itself.
JavaScript is also a large language with a complex semantics.  In this
talk I will discuss our efforts to faithfully capture the essence of
JavaScript through an operational semantics and type system, and the
application of these to verifying multiple real-world systems.

Joint work with Arjun Guha, Joe Gibbs Politz, Ben Lerner, Claudiu
Saftoiu, Matt Carroll, and Hannah Quay-de la Vallee.


11:15-12:30 Concurrency
(3 25-minute slots)

Stephen Freund
Cooperative Concurrency for a Multicore World

Multithreaded programs are notoriously prone to unintended
interference between concurrent threads.  To address this
problem, we argue that yield annotations in the source code
should document all thread interference, and we present a type
system for verifying the absence of undocumented interference.
Well-typed programs behave as if context switches occur only at
yield annotations.  Thus, they can be understood using intuitive
sequential reasoning, except where yield annotations remind the
programmer to account for thread interference.

Experimental results show that our type system for yield
annotations is more precise at capturing thread interference than
prior techniques based on method-level atomicity specifications
and reduces the number of interference points a programmer must
reason about by an order of magnitude. The type system is also
more precise than prior methods targeting race freedom.  In
addition, yield annotations highlight all known concurrency
defects in the Java programs studied.

This is joint work with Cormac Flanagan, Tim Disney, Caitlin
Sadowski, and Jaeheon Yi at UC Santa Cruz.


Y. Annie Liu
From Clarity to Efficiency for Distributed Algorithms

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.  The
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.  The core of the
optimizations is the first general method for transforming logic
quantifications into efficient implementations.  We 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.  Our 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Ôæïs Center for Genomics and Systems 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 ÔæíflowÔæì 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 Òobviously correctÓ
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,  enables off-the-shelf program analysis tools to
naturally perform the reasoning necessary for proving temporal properties
(e.g.  backtracking, 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

 High level languages provide abstractions that assist programmers;
however these abstractions are not always sufficient and, in some cases,
they get in the way of writing efficient or functioning correct 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’s XCAP [2]. Bedrock2 is an extension and rewrite of
Chlipala’s Bedrock language [1].  Bedrock2 allows programmers to define
both control and data abstractions and integrate them into the system
in a first-class way. Control abstractions, e.g. conditionals and
function calls, are defined by providing a denotation into the core
language and derived inference rules are verified in a foundational way
with respect to the core language semantics. These inference rules are
used by the verification condition generator simplify the proof
obligations provided to the programmer. Verification conditions 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-defined
abstract predicates to enable efficient manipulation of arrays,
structures, stack frames, and other data abstractions. Final
verification condi- tions are discharged using a cancellation-based
separation logic prover. Proofs are generated using computational
reflection to enable good performance that, experiences suggest, will
scale to larger programs than previous work. Bedrock2 embraces a more
realistic machine model that exposes machine word sizes, byte
ordering, and finite memory. We are working to extend the language 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

 Despite 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.  Most 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.  The performance of JVM languages, for instance, often lags behind
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.   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.