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