Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 10:45
Benjamin Goldberg(NYU)
Translation Validation of Loop Optimizations
Break: 10:45 - 11:00
Session 2: 11:00 - 12:30
Jeff Foster (Maryland)
Aliasing and Flow-Sensitive Type Qualifiers
Greg Morrisett (Cornell)
Beyond Regions in Cyclone
Lunch: 12:30 - 1:50
Business meeting: 1:50 - 2:00
Session 3: 2:00 - 3:30
Limin Jia (Princeton University)
Modal Proofs as Distributed Programs
Benjamin Pierce (UPenn)
Harmony: A Synchronization Framework
for Tree-Structured Data
We will briefly describe our approach to validating optimizations which preserve the loop structure of the code, and describe a tool, VOC-64, which implements this technique. For more aggressive optimizations which alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and loop interchange, we will then present permutation rules which establish that the transformed code satisfies all the implied data dependencies necessary for the validity of the considered transformation.
If time permits, we will present some preliminary work on run-time validation of speculative loop optimizations, which involves using run-time tests to ensure the correctness of loop optimizations of which neither the compiler nor compiler-validation techniques can guarantee the correctness. In this work, the theorem prover CVC is used not only to prove that the verification conditions are satisfied, but to generate the run-time tests.
This is joint work with Lenore Zuck, Amir Pnueli, Clark Barrett, Yi Fang, and Ying Hu.
Abstract: Cyclone is a type-safe, low-level programming language based on C. To facilitate programmer-controlled memory management, the language provides a number of options including a garbage collected heap, stack allocation, and lexical region allocation. A region-based type-and-effects system is used to ensure that a dangling pointer is never dereferenced.
Recently, we have integrated support for three new mechanisms so that programmers can better tailor memory management for an application: (1) dynamic regions, (2) unique pointers, and (3) reference counted objects. A key aspect of our design is the support for polymorphism needed to write re-usable libraries, regardless of the memory management strategy used by the client.
These new mechanisms provide an unprecedented degree of control for the programmer without sacrificing safety. For instance, we were able to improve the throughput of the MediaNet server by up to 42% and decrease the high-water mark from 8MB to a few kilobytes through a judicious use of all of these mechanisms.
Collaborators: Dan Grossman (U.Wash), Mike Hicks (U.Maryland), and Trevor Jim (AT&T)
Abstract: We develop a new foundation for distributed programming languages by defining an intuitionistic, modal logic and then interpreting the modal proofs as distributed programs. More specifically, the proof terms for the various modalities have computational interpretations as remote procedure calls, commands to broadcast computations to all nodes in the network, commands to use portable code, and finally, commands to invoke computational agents that can find their own way to safe places in the network where they can execute. We prove some simple meta-theoretic results about our logic as well as a safety theorem that demonstrates that the deductive rules act as a sound type system for a distributed programming language.
Joint work with David Walker.
Abstract: Type qualifiers are a lightweight, practical mechanism that allow programmers to specify and check properties not captured by traditional type systems. In this talk, I will examine the interaction between type qualifiers and aliasing. I will briefly describe an algorithm for flow-sensitive type qualifier inference in the presence of pointers. In order to gain efficiency, the algorithm sacrifices a certain amount of precision in its alias analysis. I will present a language construct called restrict, based on the new ANSI C type qualifier of the same name, that allows us to regain local non-aliasing information, which can be used to improve the precision of flow-sensitive type qualifier inference and can also be adapted to other flow-sensitive analyses. I will also present a type and effect system for checking the correctness of restrict, and show how it is integrated with the rest of the analysis. Finally, I will describe a system for automatically inferring restrict and confine, a short-hand for common uses of restrict, and some experiments using restrict and confine to find locking errors in Linux device drivers. If time permits, I may also discuss some recent extensions to the type and effect system for restrict.
Joint work with Tachio Terauchi, John Kodumal, and Alex Aiken.
Abstract: Increased use of optimistic data replication has led to increased interest in SYNCHRONIZATION technologies. These technologies are not only a fact of life in present-day networks; they are fascinating, and they raise a host of challenging scientific questions.
The goal of the Harmony project is to develop a generic framework for synchronizing tree-structured data--i.e., a tool for propagating updates between different copies, possibly stored in different formats, of tree-shaped data structures. For example, Harmony can be used to synchronize the bookmark files of several different web browsers, allowing bookmarks and bookmark folders to be added, deleted, edited, and reorganized by users running different browsers on disconnected machines. Other Harmony instances under development include synchronizers for calendars (Palm DateBook, ical, and iCalendar formats), address books, Keynote presentations, structured documents, file systems, and generic XML and HTML.
This talk offers a guided tour of the Harmony system, touching on
Harmony is joint work with Michael Greenwald, Jonathan Moore, and Alan Schmitt.