SPACE 2004 Second workshop on SEMANTICS, PROGRAM ANALYSIS, AND COMPUTING ENVIRONMENTS FOR MEMORY MANAGEMENT January 12, 2004 Venice, Italy, January, 2004 Sponsored by ACM/SIGPLAN. In cooperation with EAPLS.

Memory management is a difficult engineering task. We desperately need new tools and analyses that can identify memory management errors in low-level C/C++ code, such as dereferencing a pointer to an object that has been recycled or failing to reclaim an object. We also need new data structures and algorithms to avoid overheads such as fragmentation and synchronization. High-level languages such as Java or ML insulate the programmer from many of these problems through automatic memory management techniques (e.g., garbage collection). But standard GC techniques are not always suitable for all domains. For instance, programmers for embedded and real-time systems need static guarantees about resource requirements that are difficult to meet with standard collection algorithms. New languages, logics, analyses, and type systems are needed that let us reason about the management of memory, time, and other critical resources. The aim of this workshop is to bring together researchers for a fruitful exchange of ideas on semantics, program analysis and computing environments for memory management.

SCOPE: Topics of interest include but are not limited to:

• alternative memory management strategies (.e.g, region- or reap-based)
• memory management for constrained (embedded, real-time, etc.) systems
• analyses for optimization of memory management
• analyses for faults in manual memory management
• types, semantics, logics, and calculi for memory management
• applications of statically controlled memory management
• empirical results for new or existing memory management strategies

TIME AND PLACE: The workshop takes place Monday, January 12th, 2004 in Venice at the Ca' Dolfin Auditorium, University of Venice. It is co-located with POPL 2004, which takes place January 14-16, 2004.

FORMAT: The workshop will consist of:

• 25-minute presentations by authors of selected, peer-reviewed papers
• 10-minute short presentations (non-peer reviewed)
• two 45-minute invited talks (to be determined)
• a series of "5-minute madness" talks as time permits

The long papers will be selected by a program committee and only "lightly" reviewed. Our goal in selecting papers is to meet our time requirements and present a balanced program. We hope to include all of the short presentations, but may be forced to select a subset depending on the number of submissions. Again, our goal is to have a productive, interactive workshop.

At lunch-time, participants will be able to sign up for a "5-minute madness" talk slot (as time permits). These talks will be limited to at most 2 viewgraphs and are meant to give a brief, perhaps provocative, viewpoint on the research issues in memory management and to spark conversation. A moderator will limit time according to the excitement generated by the presentation.

INFORMAL PROCEEDINGS: We will distribute an informal proceedings at the workshop only. We do not consider the proceedings to be a formal (citable) publication so that any works in progress presented here may be submitted later for formal publication.

The informal proceedings for the workshop will consist of the accepted long papers, and titles and abstracts for the short presentations. Updated post-workshop proceedings will include the list the 5-minute madness talks presented.

INVITED SPEAKERS:

• Uday Reddy (University of Birmingham, UK)
• David Walker (Princeton University, USA)

PROGRAM:

8:30 - 10:15

• Uday Reddy: Semantic models of Storage (invited talk)
• Stefan Monnier: Typed Regions (long talk; pdf)
• Richard Bornat, Cristiano Calcagno, and Peter O'Hearn: Local Reasoning, Separation, and Aliasing (long talk)

10:15 - 10:45 Coffee/tea break

10:45 - 12:30

• Matthew Fluet: Monadic Regions (short talk; ppt)
• Robert Atkey: A Calculus for Resource Relationships (short talk; pdf)
• Lozes Etienne: Separation Logic Preserves the Expressive Power of Classical Logic (short talk)
• Ivana Mijajlovic and Noah Torp-Smith: Refinement in Separation Context (short talk; pdf)
• Edgar G. Daylight, Bart Demoen, and Francky Catthor: Formally Specifying Dynamic Data Structures for Embedded Software Design: An Initial Approach (short talk)
• Roberto Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, Line Jakubiec: A Functional Scenerio for Bytecode Verification of Space Bounds (short talk; pdf)
• Andrew Kennedy and Don Syme: Combining Generics, Pre-Compilation and Sharing Between Software-Based Processes (short talk)

12:30 - 14:00 Lunch

13:45 - 14:00 Sign-up for 5-minute madness presentations

14:00 - 15:45

• David Walker, Stacks, Heaps and Regions: One Logic to Bind Them (invited talk; ppt)
• Chris Hawblitzel, Edward Wei, Heng Huang, Eric Krupski, and Lea Wittie: Low-Level Linear Memory Management (long talk)
• Matthew Fluet and Daniel Wang: Implementation and Performance Evaluation of a Safe Runtime System in Cyclone (long talk; ppt)

15:45 - 16:15 Break

16:15 - 17:50

• Steffen Jost: lfd_infer: An Implementation of a Static Inference on Heap Space Usage (short talk; pdf)
• Nicholas Nethercote and Jeremy Fitzhardinge: Bounds-Checking Entire Programs without Recompiling (short talk)
• David Detlefs: Automatic Inference of Reference-Count Invariants (short talk; pdf)
• Oukseh Lee and Kwangkeun Yi: Experiments on the Effectiveness of an Automatic Insertion of Safe Memory Reuses into ML-like Programs (short talk; ppt)
• Michael Hicks, Dan Grossman, and Trevor Jim: Combining Garbage Collection and Safe Manual Memory Management (short talk; ppt)
• Daniel Spoonhower, Guy Blelloch, and Robert Harper: Incremental Copying Collection with Pinning (Progress Report) (short talk; pdf)

17:50 - 18:00 Short break

18:00 - 19:00 5-minute madness talks

• David Bacon
• Dan Grossman:

  Waving one's hands about memory safety is unsatisfying because we have largely failed to give a compelling definition of memory safety. However, we have compelling definitions of encapsulation (i.e., ADTs), so we should argue that memory-management should preserve encapsulation. In particular, it must be possible for an abstraction to create and maintain private (i.e., encapsulated) space. At minimum, this requires that no usable aliases to freshly allocated space exist. Ensuring this is good motivation for what we do.

• Martin Hofmann
• Richard Bornat
• Peter O'Hearn
• John Reynolds:

  We all believe in our hearts that types are just a limited form of propositions - restricted to obtain decidability. But we are far from devising usable logics and type systems that make this evident. On the one hand, only propositions are rich enough to express program correctness, as opposed to safety properties. On the other, only types extend to higher-order. There is also a semantic problem: Types denote partial equivalence relations on the domain of values, but propositions only denote subsets. Where are the equivalences that propositions should denote?

• Dave Detlefs

19:00 - 20:00 Free time (Bar, hotel, etc.)

20:00 - 2X:00 Dinner

The dinner is at "Trattoria Antica Besseta", Santa Croce 1395, Salizada de Ca' Zusto.

INFORMATION: Please refer to the workshop home page at http://www.diku.dk/topps/space2004/ or subscribe to the low-volume mailinglist at http://mailman.itu.dk/mailman/listinfo/space (which is exclusively dedicated to SPACE) for up-to-date information on location, invited talks, participation, etc.

REGISTRATION: For information on registration, accommodations etc, please refer to the POPL 2004 conference web pages.

GENERAL CHAIRS:

• Fritz Henglein, Dept. of Computer Science, University of Copenhagen
• Peter O'Hearn, Dept. of Computer Science, Queen Mary, University of London

PROGRAM COMMITTEE:

• Cristiano Calcagno Dept. of Computing, Imperial College of Science, UK
• Amer Diwan, Dept. of Computer Science, University of Colorado, Boulder, USA
• Manuel Fähndrich, Microsoft Research, Redmond, USA
• Richard Jones, Computing Laboratory, University of Kent, UK (chair)
• Greg Morrisett, Dept. of Computer Science, Cornell University, USA (chair)
• Henning Niss, IT University of Copenhagen, Denmark
• Hongseok Yang, School of Computer Science & Engineering, Seoul National University, Korea