Formal models of distributed memory management

Cristian Ungureanu, Benjamin Goldberg

Research output: Contribution to conferencePaperpeer-review


We develop an abstract model of memory management in distributed systems. The model is low-level enough so that we can express communication, allocation and garbage collection, but otherwise hides many of the lower-level details of an actual implementation. Recently, such formal models have been developed for memory management in a functional, sequential setting. The models are rewriting systems whose terms are programs. Programs have both the `code' (control string) and the `store' syntactically apparent. Evaluation is expressed as conditional rewriting and includes store operations. Garbage collection becomes a rewriting relation that removes part of the store without affecting the behavior of the program. Distribution adds another dimension to an already complex problem. By using techniques developed for communicating and concurrent systems, we extend their work to a distributed environment. Sending and receiving messages is also made apparent at the syntactic level. A very general garbage collection rule based on reachability is introduced and proved correct. Now proving correct a specific collection strategy is reduced to showing that the relation between programs defined by the strategy is a sub-relation of the general relation. Any actual implementation which is capable of providing the transitions (including their atomicity constraints) specified by the strategy is therefore correct. This model allows us to specify and prove correct in a compact manner two garbage collectors; the first one does a simple garbage collection local to a node. The second garbage collector uses migration of data in order to be able to reclaim inter-node cyclic garbage.

Original languageEnglish (US)
Number of pages12
StatePublished - 1997
EventProceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming, ICFP - Amsterdam, Neth
Duration: Jun 9 1997Jun 11 1997


OtherProceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming, ICFP
CityAmsterdam, Neth

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Formal models of distributed memory management'. Together they form a unique fingerprint.

Cite this