![[logo suggestions welcome]](/logo.gif){kind=logo}
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.
