[logo suggestions welcome]

N
E
P
L
S

These abstracts are for talks at this event.

NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.


Modular, Sequential Reasoning for Multithreaded Spec# Programs

Wolfram Schulte (Microsoft Research)

Spec# is an experimental extension to C# that adds design-by-contract
features. Contracts include method preconditions, postconditions, and
object invariants. Contracts capture programmer intentions about how
methods and data are to be used. The Spec# compiler emits run-time
checks that enforce the contracts and the Spec# program verifier uses
theorem-proving technology to statically check the consistency between
a program and its contracts.

In this talk I will introduce Spec# and then focus on Spec#'s features
that prevent data races and deadlocks. The technique to do so imposes
a specific programming model, i.e. a set of rules that prescribe how
to use the existing synchronization primitives from C#. We show that
properly annotated programs can be formally verified to comply with
the programming model. In other words, if the annotated program
verifies, the underlying C# program is guaranteed to be free from data
races and deadlocks, and it is sound to reason locally and
sequentially about program behavior.

Joint work with Bart Jacobs, Jan Smans, Frank Piessens, all from KU Leuven.


Programming by Sketching

Ras Bodik (The University of California at Berkeley)

Sketching is a software synthesis approach where the programmer
develops a partial implementation --- a program with holes called a
sketch. The synthesizer then completes the sketch to make it behave
like a separately provided specification. Holes typically stand for
error-prone code fragments such as index expressions, lookup tables,
or bitmasks.

I will present SKETCH, a language for sketching finite
programs. Finite programs include many high-performance kernels, which
are notorious for requiring orchestration of minute details. Sketching
can often synthesize these details, allowing the programmer to focus
on the higher-level implementation strategy. As a case study, I will
describe our implementation of the AES cipher.

In contrast to prior synthesizers, which had to be equipped with
domain-specific rules, SKETCH reduces synthesis to eneralized Boolean
satisfiability. Consequently, our synthesizer is complete for the
class of finite programs: it is guaranteed to complete any sketch in
theory, and in practice has scaled to realistic programming problems.


Parallelism in Fortress

Jan-Willem Maessen (Sun Microsystems)

The Fortress programming language is designed to run programs in
parallel without knowing the number of processors involved in
computation.  To accomplish this goal, we must begin with a shared-
memory (NUMA) view of the underlying machine.  Each parallel loop is
recursively subdivided into sub-loops which can be scheduled
independently on a large shared-memory machine.

The recursive subdivision of Fortress computations is guided entirely
by library code.  In this talk I will present generators, the
mechanism for expressing parallelism in Fortress.  To permit control
over the distribution of parallel computations, generators invert the
structure of traditional object-oriented iterators: the generator
provides the control structure, rather than acting as a passive source
of values.  The resulting model is very much in the map/reduce style.
By using type information and overloading, we can create generators
which adapt to the algebraic properties of particular reduction
operators (idempotence, zeros for early termination, etc.).  These
different adaptations correspond to catamorphisms over Boom trees with
the corresponding algebraic properties.

Joint work with Guy Steele.


FrTime: An Embedding of Dynamic Dataflow in a Call-by-Value Language

Gregory Cooper (Brown University)

FrTime is an extension of Scheme designed for writing interactive
applications.  Inspired by functional reactive programming, it embeds
dynamic dataflow within a call-by-value functional language.  The
essence of the embedding is to make program expressions evaluate to
nodes in a dataflow graph; a dataflow engine reacts to events by
recomputing the corresponding nodes and their dependents.  Our
embedding strategy offers several benefits, including easy importation
of legacy code and support for incremental program construction.  We
have integrated FrTime with the DrScheme programming environment and
have used it to develop several novel applications.  We have also
developed a formal semantics, which I will discuss briefly.

This is joint work with Shriram Krishnamurthi, and was presented at ESOP 2006.


Object Segregation According to Life Expectancy

Fabio Rojas (Northeastern University and Sun Microsystems)

We present a technique we refer to as the scan-only prefix, an
optimization over generational garbage collection. It scans, but does
not evacuate, regions of the young generation with high expected
survival rates in order to give objects in these regions another
chance to die "in-place'' and be reclaimed efficiently during a
subsequent young collection. The decision of which regions of the
young generation to scan and which to evacuate is taken so that the
efficiency of young collection is maximized.

We further refine this idea by segregating objects in the young
generation according to their life expectancy: short-lived and
non-short-lived.  We then apply the scan-only prefix technique to
those non-short-lived objects that are likely to survive the
collection, while ensuring that all the short-lived objects are
considered for collection. We perform the object segregation
dynamically and at allocation site granularity, using a novel
profiling technique.

Our measurements, show that for applications that have a non-trivial
population of medium-lived objects, the scan-only prefix technique, in
conjunction with young object segregation, decreases overall garbage
collection time and increases throughput.

Joint work with Tony Printezis.


Distributed Meta-Programming

Rui Shi (Boston University)

Distributed meta-programming (DMP), which allows code to be generated
and distributed at run-time, has already become a common
practice. However, code generation currently often relies on rather ad
hoc approaches that represent code as plain text, making DMP
notoriously error-prone. This unfortunate situation is further
exacerbated due to issues such as mobility (of code) and locality and
heterogeneity (of resources), which complicate testing and debugging
drastically. We study distributed meta-programming from a
type-theoretic perspective, presenting a language to facilitate the
construction of programs that may generate and distribute code at
run-time. The approach we take makes use of a form of typeful code
representation developed in a previous study on metaprogramming, and
it guarantees statically that only well-typed code (according to some
chosen type discipline) can be constructed at run-time and sent to
proper locations for execution.

Joint work with Chiyan Chen (Yahoo! Inc.) and Hongwei Xi (Boston University).


Modular Multiple Dispatch with Multiple Inheritance

J.J. Hallett (Sun Microsystems)

Overloaded functions and methods with multiple dispatch are useful for
extending the functionality of existing classes in an object-oriented
language.  However, such functions introduce the possibility of
ambiguous calls that cannot be resolved at run time, and modular
static checking that such ambiguity does not exist has proved elusive
in the presence of multiple implementation inheritance.  We present a
core language for defining overloaded functions and methods that
supports multiple dispatch and multiple inheritance, together with a
set of restrictions on these definitions that can be statically and
modularly checked.  We have proved that these restrictions guarantee
that no undefined or ambiguous calls occur at run time, while still
permitting various kinds of overloadings not permitted in other
languages that provide such guarantees.

Joint work with Eric Allen, Victor Luchangco, Sukyoung Ryu and Guy Steele.


Abstract Predicates and Mutable ADTs in Hoare Type Theory

Aleksandar Nanevski (Harvard University)

Hoare Type Theory (HTT) combines a dependently typed, higher-order
language with monadically-encapsulated, stateful computations.  The
type system incorporates pre- and post-conditions, in a fashion
similar to Hoare and Separation Logic, so that programmers can
modularly specify the requirements and effects of computations within
types.

In this work, we extend HTT with quantification over abstract
predicates (i.e., higher-order logic), thus embedding into HTT the
Extended Calculus of Constructions.

When combined with the Hoare-like specifications, abstract predicates
provide a powerful way to define and encapsulate the invariants of
private state; that is state that may be shared by several functions
but is not accessible to their clients. We demonstrate this power by
sketching a number of abstract data types that demand ownership of
mutable memory, including an idealized custom memory manager.

Joint work with Amal Ahmed, Greg Morrisett and Lars Birkedal.


Last modified Thursday, September 28th, 2006 10:08:52pmPowered by PLT