![[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.
Mechanizing Metatheory Using Twelf
Robert Harper (Carnegie Mellon University)
What does it mean for a programming language to exist? The usual approach is to define a language by a "reasonably precise" description a la K&R, together with a "reference compiler" that implements it (and serves as the final arbiter of ambiguities). This relies heavily on social constructs such as standardization committees, or on the marketing clout of a large corporation, and is not suitable as a basis for a rigorous analysis of the safety or security properties of the language. Another approach is to define a language by a rigorous semantics that is amenable to mathematical analysis. The most successful method of semantic definition is to give a static semantics in the form of a type system and a dynamic semantics in the form of execution rules for a program. This gives the definition an objective character that is amenable to analysis, and helps to ensure the compatibility of compilers for it. But having a rigorous definition is not enough; at a minimum one must prove that it is internally coherent according to various criteria. This re-introduces some of the difficulties of the traditional methods, because someone has to do the proofs and someone has to read them to ensure they are right. The burdens of doing "at scale" are so severe that the semantics becomes an inhibitor, rather than an enabler, of innovation. One way forward is to formalize the definition within a logical framework and to use verification tools to check crucial properties, much as we use type systems to ensure sensibility of our programs. I will describe the work we have been doing on mechanizing formal language definitions, and describe some of the successes, and difficulties, of using the Twelf system to verify their metatheory. Joint work with Karl Crary and Michael Ashley-Rolman.
A Functional Approach to Typed Object-Oriented Programming
Rui Shi, Chiyan Chen, and Hongwei Xi (Boston University)
ATS is a recently developed programming language with a highly expressive type system rooted in the framework Applied Type System. In this paper, we present a design to support typed object-oriented programming (OOP) with multiple inheritance in ATS. In contrast to most existing approaches that represent objects as records, we instead represent objects as functions in ATS. We demonstrate that full-fledged support for OOP can be built directly on the top of the functional core of ATS without seeking ad hoc extensions. In particular, we show that a variety of issues with OOP (e.g., binary methods, the self type, parametric polymorphism, multiple inheritance) can be readily addressed by the approach we take to support OOP.
For more information about ATS and the implementation, see http://www.cs.bu.edu/~hwxi/ATS/ATS.html.
Static Deadlock Detection for Java Libraries
Amy Williams, William Thies, and Michael D. Ernst (MIT)
Library writers wish to provide a guarantee not only that each procedure in the library performs correctly in isolation, but also that the procedures perform correctly when run in conjunction. To this end, we propose a method for static detection of deadlock in Java libraries. Our goal is to determine whether client code exists that may deadlock a library, and, if so, to enable the library writer to discover the calling patterns that can lead to deadlock. Our flow-sensitive, context-sensitive analysis determines possible deadlock configurations using a lock-order graph. This graph represents the order in which locks are acquired by the library. Cycles in the graph indicate deadlock possibilities, and our tool reports all such possibilities. We implemented our analysis and evaluated it on 18 libraries comprising 1245 kLOC. We verified 13 libraries to be free from deadlock, and found 14 distinct deadlocks in 3 libraries.
This work will be presented at ECOOP 2005. The full paper is available at http://cag.csail.mit.edu/~amy/papers/deadlock-ecoop05.pdf.
Debugging Concurrent Software by Context-Bounded Analysis
Shaz Qadeer (Microsoft Research)
Designing concurrent programs is difficult. The nondeterministic interaction between concurrently executing threads of a concurrent program results in programming errors that are notoriously difficult to reproduce and fix. I will present a new static analysis technique based on model checking for automatically finding errors in concurrent software. An execution of a concurrent program is a sequence of contexts, where each context consists of transitions performed by a single thread. My work is motivated by the insight that many subtle errors in a concurrent program are manifested by executions with few contexts. I will use this insight to create analyses based on systematic state exploration that are efficient and effective in finding concurrency errors. I will first present KISS (Keep It Simple and Sequential), a technique for transforming a concurrent program P into a sequential program Q that encodes all executions of P with a small number of contexts. I used KISS to convert SDV (Static Driver Verifier), a model checker for sequential C programs, into a model checker for concurrent C programs. The combination of KISS and SDV has found a number of subtle concurrency errors in Windows device drivers. Next, I will present a new theoretical result which illustrates that context-bounding significantly reduces the complexity of verifying concurrent programs. It is well-known that the problem of verifying assertions in a concurrent boolean program is undecidable. I will show that if analysis is limited to executions with a fixed but arbitrary context-bound, the problem becomes decidable, even in the presence of unbounded dynamic thread creation.
This talk presents work done in collaboration with Dinghao Wu (Princeton University) and Jakob Rehof (Microsoft Research). Our two papers on this work, "KISS: Keep it simple and sequential" and "Context-bounded model checking of concurrent software" can be found at my home page under the heading "Recent Publications".
Exploiting Schemas in Data Synchronization
Nate Foster (University of Pennsylvania)
Increased reliance on optimistic data replication has led to burgeoning interest in tools and frameworks for synchronizing disconnected updates to replicated data. We have implemented a generic synchronization framework, called Harmony, that can be used to build state-based synchronizers for a wide variety of tree-structured data formats. A novel feature of this framework is that the synchronization process---in particular, the recognition of conflicts---is driven by the schema of the structures being synchronized. In this talk, I will describe Harmony's core synchronization algorithm, state a simple and intuitive specification, and illustrate how it can be used to build a robust synchronizer for browser bookmarks.
Facilitating Pointer Program Verification with Stateful Views
Dengping Zhu and Hongwei Xi (Boston University)
A great obstacle in the verification of programs involving pointers is the lack of an effective approach to modeling the highly dynamic nature of the imperative data structures (e.g., various linked lists and trees) that make explicit use of pointers. In this talk, we show that (recursive) stateful views, a recently developed type-theoretic notion for modeling memory layouts, can enable us to effectively capture (sophisticated) invariants in pointer-rich programs while retaining practical type-checking. For instance, the interesting invariant can be readily captured in our system that each node in a doubly linked binary tree points to its children that point back to the node itself. This is done in a programming paradigm which we call programming with theorem proving. We are to first briefly explain the type theory behind stateful views and then present some realistic programming examples based on a running implementation, which is currently available to the public, to demonstrate the effectiveness of stateful views in facilitating program verification involving pointers.
Our paper on this work can be found at ATS Homepage.
Quantifying the Performance of Garbage Collection vs. Explicit Memory Management
Matthew Hertz and Emery D. Berger (University of Massachusetts Amherst)
Garbage collection yields numerous software engineering benefits, but its quantitative impact on performance remains elusive. One can measure the cost of conservative garbage collection relative to explicit memory management in C/C++ programs by linking in an appropriate collector. This kind of direct comparison is not possible for languages designed for garbage collection (e.g., Java), because programs in these languages naturally do not contain calls to free. Thus, the actual gap between the time and space performance of explicit memory management and precise, copying garbage collection remains unknown. We describe a system we developed which enables us to take the first steps towards quantifying the performance of precise garbage collection versus explicit memory management. Using this "oracular" memory management system, we compare explicit memory management to both copying and non-copying garbage collectors across a range of benchmarks. We then present results which quantify the time-space tradeoff of garbage collection and show when garbage collection performance is competitive with that of explicit memory management. We also show that the time-space tradeoff for garbage collection is even more observable when physical memory is scarce: while paging, garbage collection can run over an order of magnitude slower than explicit memory management.
Sneaking Existentials into Java
Kim Bruce (Williams College -> Pomona College via UCSC)
Existential types were introduced by Mitchell and Plotkin to model the sort of abstraction found in abstract data types. Existential types also play an important role in hiding the visibility of instance variables in modeling objects in object-oriented languages, though they are used quite differently in modeling objects compared to ADT's. Theoretically, existential types are quite nice, forming a nice dual to universal (polymorphic) types, and supporting the Curry-Howard isomorphism between types and formulas of inuitionistic second-order propositional logic. Wild-card types were a last minute addition to Java 5. In fact, a minor variant was rejected by the group controlling the evolution of the language. In this talk we review the use of existential types and how they explain some of the idiosyncracies of wild-card types. We also point out how most of the uses of existential types could easily be eliminated from the signatures of methods of Java libraries, though at some cost in verbosity.
