Seminar: Zeiger
Martin
Hofmann
Organisatorisches
Bei Interesse wird um Voranmeldung an Frau Nentwich-Mertel
gebeten.
Die Themenvergabe findet
bei der Vorbesprechung in der ersten Semesterwoche statt.
Zum Inhalt
Das Schreiben korrekter Programme, welche Zeiger verwenden, ist
bekanntlich eine knifflige Angelegenheit mit vielen Gelegenheiten
für hartnäckige Fehler, so z.B. unbeabsichtigte
Fernwirkungen durch Aliasing (verschiedene Zeiger verweisen auf
überlappende Bereiche) oder Memory Leaks.
In funktionalen Programmiersprachen dagegen
treten diese Probleme nur in sehr beschränktem Masse auf,
dafür hat man Effizienzverluste aufgrund der garbage collection in
Kauf zu nehmen.
Ausserdem implementieren Zeiger das abstrakte Konzept der
Identität: Objekte oder Datensätze bekommen durch ihre Speicheradresse eine eindeutige Kennung zugewiesen. Dies
spielt bei manchen Algorithmen (union-find, heapsort) eine Rolle und
stellt auch ein zentrales Konzept der objektorientierten
Programmierung dar.
In den letzten Jahren hat die formale Beschreibung der mit Zeigern
assoziierten Phänomene grosse Fortschritte gemacht; so gibt es
mittlerweile z.B.
-
Programmlogiken (Analoga zur Hoare Logik) für Zeiger,
- automatische Verfahren zur Überprüfung von
Zeigerinvarianten (etwa: Zeiger x verweist auf verkettete Liste),
- Alternativen zur garbage collection bei funktionalen Programmen,
- Logische Systeme für Namen und Identität,
- Formale und halbautomatische Verfahren zur Erkennung von
Aliasing,
Im Seminar wollen wir uns anhand einer Auswahl der u.a. Originalarbeiten einen
Überblick über dieses Themengebiet verschaffen.
Vorkenntnisse
Grundkenntnisse in der Logik; Kenntnis von C, sowie einer
funktionalen Programmiersprache (ersatzweise auch Java).
Literatur
- Rakesh Ghiya and Laurie J. Hendren. Is it a tree, a dag or a cyclic graph? a shape analysis for heap-directed pointers in C. In 23rd Annual ACM SIGACT-SIGPLAN Symposium on the Principles of Programming Languages, January 1996.
- Stephen A. Cook and Derek C. Oppen. An assertion language for data
structures. In Proc. POPL 1975. Kopie auf Anfrage.
- Ian Mason. Verification of programs that destructively manipulate
data. Science of Computer Programming, 10(2):177-210, 1988. Kopie auf Anfrage.
- On Garbage and Program Logic
Cristiano Calcagno, Peter O'Hearn
Proceedings of FOSSACS'01. Lokale Kopie
- Ian Stark. Names, equations, relations: Pratical ways to reason about
"new. Fundamenta Informaticae, 33:369-396, 1998. Lokale Kopie
- BI as an Assertion Language for Mutable Data Structures. Samin
Ishtiaq, Peter O'Hearn Proceedings of POPL'01. Lokale Kopie
- A Type System for Bounded Space and Functional In-Place Update, by
Martin Hofmann. Nordic Journal of Computing, 7(4), Winter 2000. Lokale Kopie
- Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps: Shape Analysis. CC
2000: 1-17. Lokale Kopie
- Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. In 23rd Annual ACM SIGACT-SIGPLAN Symposium on the Principles of Programming Languages, January 1996. Lokale Kopie
- Anders Møller, Michael I. Schwartzbach.
The Pointer Assertion Logic Engine. PLDI'01. Lokale Kopie
- Region-Based Memory Management, by Mads Tofte and Jean-Pierre
Talpin. Information and Computation 132(2):109-176, 1997. Lokale Kopie
- Type-Based Alias Analysis, by Amer Diwan, Kathryn McKinley, and Eliot
Moss. In Proceedings of PLDI'98, ACM SIGPLAN Conference on Programming
Language Design and Implementation, pages 106-117, 1998. Lokale Kopie
Lokale Kopie
- Representation Independence, Confinement, and Access Control.
A. Banerjee, D. Naumann. Proceedings of POPL'02. Lokale Kopie
- Robert P. Wilson and Monica S. Lam. Efficient context-sensitive pointer analysis for C programs. In SIGPLAN '95 Conference on Programming Language Design and Implementation, pages 1-12, 1995. SIGPLAN Notices, 30(6). Lokale Kopie
Last modified: Wed Jan 23 14:42:24 CET 2002