2nd MM-NET Workshop on
Analytical Techniques for Memory Management
University of Kent at Canterbury
15th May 2003

The second UK Memory Management Workshop, on Analytical Techniques for Memory Management, was held at the Computing Laboratory of the University of Kent on 15 May 2003. Topics of interest for this workshop included but were not limited to static prediction and bounding of memory usage, garbage collection supported by compile-time techniques and memory management models. Twenty-one members of the Network and visitors attended the workshop.

Presentations from the workshop will be provided here to form an informal proceedings. We intend to approach speakers to form an edited formal proceedings at a later date. Some support for travel costs for UK personnel may be available (please contact Richard Jones).

Abstracts

Note that the htm files produced by PowerPoint appear to be browser-dependant. They work with Internet Explorer but not with my version of Opera, for example.

Greg Morrissett, Type-Safe Memory Management in Cyclone: Regions and Beyond
The Cyclone project is a type-safe dialect of C which features an advanced type system (polymorphism, regions, …), an intra-procedural flow analysis (def. assignment,…), new language features (tagged unions, fat pointers,…) and run-time checks (array bounds checks,…). In this talk, I describe Cyclone's approach to Region-based Memory Management and how Cyclone integrates unique pointers. [htm] [ppt]

Noah Torp-Smith, Proving Correctness of a Garbage Collector via Local Reasoning
We outline what is meant by correctness of a copying garbage collector, and employ separation logics to formally specify correctness. We then prove that our implementation meets its specification, using the logic we have given, and auxiliary variables. [pdf]

Cristiano Calcagno, A Modular Pointer Checker
Separation Logic is an extension of Hoare Logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The talk is about computational properties of fragments of Separation Logic. Firstly a semantic approach is presented, based on reduction of validity to model checking via a finite model property. Secondly, a direct approach is presented - in the spirit of type checking - for a fragment of Separation Logic based on programming patterns emerging after experimentation with an automatic tool on small pointer-manipulating programs.

Martyn Honeyford, Post-Mortem Memory Profiling using Perl
Explanation and demonstration of a simple memory profiling technique using Perl. Involves utilising existing application trace (or adding application trace, if necessary) to monitor and record memory usage during execution. This trace is then analysed using Perl to gather information regarding the memory usage of the application. I have used this technique during developement and maintenance of one of our products to discover some interesting information including (size and location of) memory leaks and (size and location of) peak memory usage across a number of platforms (inc Windows, PocketPC and PalmOS). I plan to add a simple graphing facility next to chart memory usage throughout the application lifetime. This technique has a number of advantages over (often commercial) alternatives. In particular; 1)it is applicable to a large number of platforms, 2)it is applicable to a large number of languages (I've used it to analyse C apps, but it could be used to analyse any language where memory is allocated and freed manually - including C++), and 3)it does not require a special build (and is therefore of particular use in analysing released products in real customer situations). [htm] [ppt]

Pedro Vasconcelos, Space Cost analysis using sized types
We present an analysis for compile-time prediction of space or time costs for a simple, statically typed functional language with lists and naturals. The analysis is done by annotating types with sizes and inferring cost expressions for program fragments, including polymorphic and higher-order functions. This work is being developed in the context of the Hume project, which
aims at providing a functionally inspired language for hard real-time and resource-bounded systems. [ppt]

Andy King, Synchronisation Analysis
Java is increasingly used for multi-threaded server applications running on large multiprocessors. Mutator threads must be synchronised, typically by rolling forward to a safe-point, before a garbage collection (GC) can commence. Such synchronisation may comprise up to 23% of GC time for heavily multi-threaded applications. We have designed and incorporated into a production Java virtual machine an analys is that identifies which objects may escape the thread that allocated them and a memory manager that exploits this knowledge to eliminate most GC synchronisa tion. Our system provides the following novel contributions. The heap is divided into shared and thread-local regions, each of which can be col lected independently and without synchronisation. No unbounded write-barrier operations are required. Our analysis is fast and compositional; it supports dynamic class loading. [ppt]

Organisers

The workshop organisers are:

MM-NET is generously sponsored by the UK's Engineering and Physical Sciences Research Council (EPSRC).

Problems with this page?
Contact the mm-net webmaster
Last modified Tuesday, May 6, 2003