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


Objects as Software Services: Toward a World without Releases

Gilad Bracha (Sun Microsystems)

Software services seek to combine the advantages of traditional client
applications and web services. Software services go beyond web
services in supporting rich interaction when networks are slow,
unreliable or nonexistent. At the same time, software services retain
the advantages associated with web services: they are always available
and always up to date. Software services have the potential to
radically transform software development, as they enable a world
without versions and releases. We discuss the advantages of dynamic
object oriented language principles in facilitating the design of an
object based platform for software services.


Combining Static Analysis and Run-Time Analysis for Verification and Testing of Multithreaded Programs

Rahul Agarwal (Stony Brook University)

Concurrent programs are notorious for containing errors that are
difficult to reproduce and diagnose.  Some common concurrency errors
are data races, atomicity violations (informally, atomicity means that
executing methods concurrently is equivalent to executing them
serially), and deadlocks.  This talk focuses on using the synergy
between static and run-time analyses to efficiently detect these
errors.

We developed expressive type systems for proving absence of data
races, atomicity violations, and deadlocks.  To save the programmer
from writing type annotations, we developed type inference algorithms
for these type systems.  Our inference algorithm for race types, which
we call type discovery, is a novel combination of run-time analysis
and static analysis.

We also explored the use of static analysis to significantly decrease
the overhead of run-time checking for these errors.  Warnings from the
typechecker are used to identify parts of the program from which
run-time checking can safely be omitted.  When the types are obtained
by type discovery or type inference, the approach is completely
automatic, scalable to very large programs, and significantly reduces
the overhead of run-time checking for data races, atomicity
violations, and deadlocks.

This is joint work with Prof. Scott Stoller, Liqiang Wang, and Amit Sasturkar. It includes work published earlier at International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI) 2004, ACM SIGPLAN 2005 Symposium on Principles and Practice of Parallel Programming (PPoPP), IEEE/ACM International Conference on Automated Software Engineering (ASE) 2005, and Parallel and Distributed Systems: Testing and Debugging (PADTAD) Track of the 2005 IBM Verification Conference.


Statically Verified Typeful Compilation

Louis-Julien Guillemette (Universite de Montreal)

The use of typed intermediate representations can significantly
increase the reliability of a compiler.  By type-checking the code
produced at each transformation stage, one can identify bugs in the
compiler that would otherwise be much harder to find.  We propose to
take the use of types in compilation a step further by verifying that
the transformation itself is type correct, in the sense that it is
impossible that it produces an ill typed term given a well typed term
as input.

We base our approach on higher-order abstract syntax (HOAS), a
representation of programs where variables in the object language are
represented by meta-variables.  We use a representation that accounts
for the object language's type system using generalized algebraic data
types (GADTs).  In this way, the full binding and type structure of
the object language is exposed to the host language's type system.  In
this setting we encode a type preservation property of a CPS
conversion in Haskell's type system, using witnesses of a type
correctness proof encoded as values in a GADT.


Modular Verification of Assembly Code with Stack-Based Control Abstractions

Xinyu Feng (Yale University)

Runtime stacks are critical components of any modern software---they
are used to implement powerful control structures such as function
call/return, stack cutting and unwinding, coroutines, and thread
context switch. Stack operations, however, are very hard to reason
about: there are no known formal specifications for certifying C-style
setjmp/longjmp, stack cutting and unwinding, or weak continuations (in
C--).  In many proof-carrying code (PCC) systems, return code pointers
and exception handlers are treated as general first-class functions
(as in continuation-passing style) even though both should have more
limited scopes.

In this paper we show that stack-based control abstractions follow a
much simpler pattern than general first-class code pointers. We
present a simple but flexible Hoare-style framework for modular
verification of assembly code with all kinds of stack-based control
abstractions, including function call/return, tail call,
setjmp/longjmp, weak continuation, stack cutting, stack unwinding,
multi-return function call, coroutines, and thread context switch.
Instead of presenting a specific logic for each control structure, we
develop all reasoning systems as instances of a generic framework.
This allows program modules and their proofs developed in different
PCC systems to be linked together. Our system is fully mechanized. We
give the complete soundness proof and a full verification of several
examples in the Coq proof assistant.

This is joint work with Zhong Shao, Alexander Vaynberg, Zhaozhong Ni at Yale University, and Sen Xiang at University of Science and Technology at China.


Automatic Test Factoring for Java

David Saff (MIT)

Test factoring creates fast, focused unit tests from slow system-wide
tests; each new unit test exercises only a subset of the functionality
exercised by the system test. Augmenting a test suite with factored
unit tests should catch errors earlier in a test run.

One way to factor a test is to introduce mock objects. If a test
exercises a component T, which interacts with another component E (the
``environment''), the implementation of E can be replaced by a
mock. The mock checks that T's calls to E are as expected, and it
simulates E's behavior in response. We introduce an automatic
technique for test factoring. Given a system test for T and E, and a
record of T's and E's behavior when the system test is run, test
factoring generates unit tests for T in which E is mocked. The
factored tests can isolate bugs in T from bugs in E and, if E is slow
or expensive, improve test performance or cost.

Our implementation of automatic dynamic test factoring for the Java
language reduces the running time of a system test suite by up to an
order of magnitude.


Programming with Exceptions in JCilk

Angelina Lee (MIT)

JCilk extends the Java language to provide call-return semantics for
multithreading, much as Cilk does for C.  Java's built-in thread model
does not support the passing of exceptions or return values from one
thread back to the "parent" thread that created it.  JCilk imports
Cilk's fork-join primitives spawn and sync into Java to provide
procedure-call semantics for concurrent subcomputations.  The talk
presents how JCilk integrates exception handling with multithreading
by defining semantics consistent with the existing semantics of Java's
try and catch constructs, but which handle concurrency in spawned
methods.

JCilk's strategy of integrating multithreading with Java's exception
semantics yields some surprising semantic synergies.  In particular,
JCilk extends Java's exception semantics to allow exceptions to be
passed from a spawned method to its parent in a natural way that
obviates the need for Cilk's inlet and abort constructs.  This
extension is "faithful" in that it obeys Java's ordinary serial
semantics when executed on a single processor.  When executed in
parallel, however, an exception thrown by a JCilk computation signals
its sibling computations to abort, which yields a clean semantics in
which only a single exception from the enclosing try block is handled.
The decision to implicitly abort side computations opens a Pandora's
box of subsidiary linguistic problems to be resolved, however.  For
instance, aborting might cause a computation to be interrupted
asynchronously, causing havoc in programmer understanding of code
behavior.  To minimize the complexity of reasoning about aborts, JCilk
signals them "semisynchronously" so that abort signals do not
interrupt ordinary serial code.  In addition, JCilk propagates an
abort signal throughout a subcomputation naturally with a built-in
CilkAbort exception, thereby allowing programmers to handle clean-up
by simply catching the CilkAbort exception.

The semantics of JCilk allow programs with speculative computations to
be programmed easily.  Speculation is essential for parallelizing
programs such as branch-and-bound or heuristic search.  We show how
JCilk's linguistic mechanisms can be used to program a solution to the
"queens" problem.


Custom Object Layout for Garbage-Collected Languages

Gene Novark (University of Massachusetts, Amherst)

Modern architectures require data locality to achieve
performance. However, garbage-collected languages like Java limit the
ability of programmers to influence object locality, and so impose a
significant performance penalty. We present custom object layout, an
approach that allows programmers to control object layout in
garbage-collected languages. Custom object layout cooperates with
copying garbage collection. At collection time, the garbage collector
invokes programmer-supplied methods that direct object
placement. Custom object layout is particularly effective at improving
the locality of classes with well-known traversal patterns, such as
dictionary data structures. We show that using custom object layout
can reduce cache misses by 50%-77% and thus improves the query
performance of dictionary data structures by 20%.


XVP - An extended virtual platform

Mark Royer (University of Southern Maine)

We argue that a major limitation of current object oriented languages
and their virtual platforms is proper support for assertions
(logic-based constraints).  The main components of the required
architecture will be presented in this talk.  This architecture
includes representation of logic-based constraints in class file and
class object structures, a loader that performs appropriate actions on
type parameters and constraints, and reflective capabilities that
report information on type signatures and their associated
constraints. A particularly distinctive component of this
architecture, not considered as a part of a virtual platform, is an
interface with a program verification system that performs checking of
constraints and verifies behavioral subtyping requirements. This is
accomplished by interfacing the program verification system with
reflective capabilities and performing verification by accessing type
signatures and their associated constraints in (dynamically) loaded
class objects. The specifics are implemented by extending the Java
Virtual Machine with the proposed functionalities.

Joint work with Suad Alagic and Dan Dillon.


Last modified Monday, February 20th, 2006 3:37:03pmPowered by PLT