[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.


Efficient and Precise Datarace Detection for Multithreaded Object-Oriented Programs

Manu Sridharan (MIT/IBM), Jong-Deok Choi (IBM), Robert O'Callahan (IBM)

Concurrent shared-memory programs exhibit dataraces when thread
scheduling decisions lead to changes in output. Dataraces are very
hard to debug because error-inducing schedules may be extremely rare
and hard to reproduce, making tool support for detecting dataraces
invaluable.  Past dynamic datarace detection tools either incurred
large overhead, ranging from 3x to 30x, or sacrificed precision in
reducing overhead.  We present a novel approach to efficient and
precise datarace detection for multithreaded object-oriented programs.
Our runtime detector incurs an overhead ranging from 13% to 42% for
our test suite, well below the overheads reported in previous work.
Furthermore, our precise approach reveals dangerous dataraces in real
programs with few spurious warnings.


A Parameterized Type System for Race-Free Java Programs

Chandrasekhar Boyapati, Robert Lee, Martin Rinard (MIT)

Multithreaded programming is difficult and error prone.  It is easy to make
a mistake in synchronization that produces a data race, yet it can be
extremely difficult to locate this mistake during debugging.  This talk
presents a new static type system for object-oriented programs; this type
system guarantees that any well-typed program is free of data races.

Every object in our system is associated with a {\em protection mechanism}
that ensures that accesses to the object never create data races.
Programmers specify the protection mechanism of an object as part of the
type of the variables that refer to that object.  The type checker
statically verifies that programs use objects only in accordance with their
declared protection mechanisms.

Our system includes a type inference algorithm that reduces the burden of
writing the extra type annotations.  In particular, single-threaded
programs require almost no programming overhead.  We implemented several
multithreaded Java programs in our system.  Our experience indicates that
our type system provides a promising approach to make multithreaded
programs reliable and efficient.

Speaker's Supplement

A preliminary version of this work appeared in OOPSLA 2001. The paper can be found at: http://www.pmg.lcs.mit.edu/~chandra/publications/oopsla01.ps.


A Bytecode-Compiled, Type-safe, Multi-Stage Language

Cristiano Calcagno, Walid Taha (Yale), Liwen Huang, and Xavier Leroy

Inspired by the successes of program generation, partial evaluation, and
runtime code generation, multi-stage languages were developed as a
uniform, high-level, and principled view of staging.  Our current goal is
to demonstrate the utility of these languages in a practical
implementation.  As a first step this paper presents MetaOCaml, a
type-safe, multi-stage language, built as an extension to OCaml's bytecode
compiler.  Future-stage computations are represented as source programs.
This makes it possible to ensure type-safety, produce better dynamically
compiled code, and apply crucial runtime source-to-source transformations
such as tag elimination.  We have used MetaOCaml to measure performance
for a set of small staged programs.  The gains are consistent with those
of partial evaluation and runtime code generation, and support the claim
that multi-stage languages are well-suited for building staged
interpreters, even when the runtime compilation times are taken into
account.

Speaker's Supplement

MetaOCaml

Fully Automatic Adaptation of Software Components Based on Semantic Specifications

Christian Haack (Heriot-Watt University), Brian Howard, Allen Stoughton, Joe Wells

We describe the design and methods of a tool that, based on 
behavioral specifications in interfaces, automatically generates 
simple adaptation functors to overcome minor incompatibilities 
between SML modules. The transformations that get generated can 
be expressed in a small recursion-free sublanguage of SML, namely 
a typed lambda-calculus with function and record types, ML polymorphism, 
first-order type functions and SML equality types. The transformations 
are correct, they transform type- and behaviorally correct implementations 
of an interface A into type- and behaviorally correct implementations of 
an interface B. 

The hope is that a tool of this kind can be useful for automatically
overcoming incompatibilities that result from certain common interface 
changes in the evolution of software systems. Examples are changes 
that generalize functions by adding extra parameters, or changes that 
give functions different, but isomorphic, types. Such changes alter 
the types. The behavioral specifications, on the other hand, remain 
similar, and in many cases the similarities can be automatically 
recognized and the differences automatically overcome. Another possible 
application domain is in automatic library retrieval based on semantic 
specifications.

Speaker's Supplement

The associated paper can be found at http://www.cee.hw.ac.uk/~haack/papers/.


Adaptive Optimization in the Jikes RVM

Michael Hind (IBM Watson Research Center)

This talk will present an overview of the Jikes(TM) Research Virtual
Machine (RVM), an open source VM for Java(TM) formerly called
Jalapeño.  The Jikes RVM provides a flexible open testbed to prototype
new virtual machine technologies and experiment with a large variety
of design alternatives.  The system includes state-of-the-art
techniques for dynamic compilation, adaptive optimization, garbage
collection, thread scheduling and synchronization. The system is
implemented in the Java programming language and is self-hosted i.e.,
its Java code runs on itself without requiring a second virtual
machine.  The system runs on AIX(TM)/PowerPC(TM), Linux©/PowerPC and
Linux/IA-32 platforms.

This presentation will highlight the various components of the Jikes
RVM, and focus on results from the adaptive optimization system, a
system that uses an online cost/benefit model to determine which
methods should be optimized and at what optimization level.  The talk
will also discuss some work in progress.

Jikes, AIX, and PowerPC are trademarks or registered trademarks of
International Business Machines Corporation in the United States,
other countries, or both.
 
Java and all Java-based trademarks and logos are trademarks or
registered trademarks of Sun Microsystems, Inc. in the United States,
other countries, or both.

Speaker's Supplement

The Jikes RVM is the result of a large team of researchers. Further information on the project is available at http://www.ibm.com/developerworks/oss/jikesrvm and about the author at http://www.research.ibm.com/people/h/hind.


Genuinely Functional User Interfaces

Antony Courtney (Yale) and Conal Elliott (Microsoft Research)

Fruit is a new graphical user interface library for Haskell
based on a formal model of user interfaces. The model identifies
signals (continuous time-varying values) and signal transformers (pure
functions mapping signals to signals) as core abstractions, and
defines GUIs compositionally as signal transformers.  In this talk, I
will describe why we think a formal denotational model of user
interfaces is useful, present our model and prototype library
implementation, and show some example programs that demonstrate novel
features of our library.

This is joint work with Conal Elliott (Microsoft Research).

Speaker's Supplement

This talk was first presented at the 2001 Haskell Workshop (part of PLI 2001). Our paper describing this work can be found at http://apocalypse.org/~antony/pubs/genuinely-functional-guis.pdf.


Principal Typings Demystified: what they are, why you want them, and why your type system doesn't have them

Joe Wells (Heriot-Watt)

Let S be some type system. A typing in S for a typable term M is the
collection of all of the information other than M which appears in the
final judgement of a proof derivation showing that M is typable. For
example, suppose there is a derivation in S ending with the judgement
A |- M : tau meaning that M has result type tau when assuming the
types of free variables are given by A. Then (A, tau) is a typing for
M.

A principal typing in S for a term M is a typing for M which somehow
represents all other possible typings in S for M. It is important not
to confuse this notion with the weaker notion of principal type often
mentioned in connection with the Hindley/Milner type system. Previous
definitions of principal typings for specific type systems have
involved various syntactic operations on typings such as substitution
of types for type variables, expansion, lifting, etc.

This talk presents a new general definition of principal typings which
does not depend on the details of any particular type system. This
talk shows that the new general definition correctly generalizes
previous system-dependent definitions. This talk explains why the new
definition is the right one. Furthermore, the new definition is used
to prove that certain polymorphic type systems using "for all"
quantifiers, namely System F and the Hindley/Milner system, do not
have principal typings.


A Modular, Extensible Proof Method for Small-step Flow Analyses

Galen Williamson and Mitch Wand (Northeastern)

We introduce a new proof technique for showing the
correctness of 0CFA-like analyses with respect to small-step
semantics.  We illustrate the technique by proving the correctness of
0CFA for the pure lambda-calculus under arbitrary beta-reduction.  This
result was claimed by Palsberg in 1995; unfortunately, his proof was
flawed.  We provide a correct proof of this result, using a simpler
and more general proof method.  We illustrate the extensibility of the
new method by showing the correctness of an analysis for the
Abadi-Cardelli object calculus under small-step semantics.

Speaker's Supplement

This talk will be presented at ESOP 2002. Our paper can be found at http://www.ccs.neu.edu/home/gwilliam/esop02.ps.gz


Last modified Tuesday, February 12th, 2002 0:56:09amPowered by PLT