005 |
|
19991110072144.9 |
035 |
|
|aAAI9819805
|
035 |
|
|a(UnM)AAI9819805
|
040 |
|
|aTWNTU|cTWNTU|dTWNTU
|
095 |
|
|aNTTTCL|bN|cN000008|d008|pNR|fFRANK|zNR|m0|tDDC
|
100 |
1
|
|aUNGUREANU, CRISTIAN.
|
245 |
10
|
|aFORMAL MODELS OF DISTRIBUTED MEMORY MANAGEMENT (GARBAGE COLLECTION).
|
300 |
|
|a107 p.
|
500 |
|
|aSource: Dissertation Abstracts International, Volume: 58-12, Section: B, page: 6676.
|
500 |
|
|aAdviser: BENJAMIN GOLDBERG.
|
502 |
|
|aThesis (PH.D.)--NEW YORK UNIVERSITY, 1998.
|
520 |
|
|aAutomatic memory management, or garbage collection, is a valuable service, significantly freeing programmer's resources. Programmers can rely on the language implementation to find and deallocate unneeded objects while also ensuring memory safety: no program will use dangling pointers. Although garbage collectors come with their problems (e.g. run-time costs, possibly additional synchronization costs in concurrent systems) the benefits usually outweigh the drawbacks if the collector indeed ensures memory safety. Unfortunately, the correctness of the garbage collector is very rarely proved in a satisfactory manner, this happens not only because of the complexity of the strategies used, but also because of the lack of a simple model of memory operations.
|
520 |
|
|aIn this dissertation, we are presenting a model suitable for reasoning about memory management in concurrent and distributed systems. The model provides a suitable level of abstraction: it 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. Using it, we can give compact, and provably correct, characterizations of garbage collection algorithms in distributed systems.
|
520 |
|
|aThe models are rewriting systems whose terms are programs in which the "code", the "store" and the "communication" are syntactically apparent. Evaluation is expressed as conditional rewriting and includes store and communication operations. Using techniques developed for communicating and concurrent systems we give a semantics suitable for proving equivalence of such programs. Garbage collection becomes a rewriting relation that removes part of the store without affecting the behavior of the program.
|
520 |
|
|aWe introduce and prove correct a very general garbage collection rule based on reachability; any actual implementation which is capable of providing the transitions (including their atomicity constraints) specified by the strategy is therefore correct. We give examples of such specific implementations, and show how their correctness follows from the correctness of the general relation.
|
590 |
|
|aSchool code: 0146.
|
650 |
4
|
|aComputer Science.
|
690 |
|
|a0984
|
710 |
20
|
|aNEW YORK UNIVERSITY.
|
773 |
0
|
|tDissertation Abstracts International|g58-12B.
|
790 |
|
|a0146
|
790 |
10
|
|aGOLDBERG, BENJAMIN,|eadvisor.
|
791 |
|
|aPH.D.
|
792 |
|
|a1998
|
809 |
|
|d008|tDDC|pNR
|
856 |
40
|
|uhttp://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=9819805
|