Faculty of Information Technology, BUT

Publication Details

Pointer Race Freedom

HAZIZA Frédéric, HOLÍK Lukáš, MEYER Roland and WOLF Sebastian. Pointer Race Freedom. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 9583. Berlin: Springer Verlag, 2016, pp. 393-412. ISBN 978-3-662-49121-8. Available from: http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19
Czech title
Absence ukazatelových závodů
Type
conference paper
Language
english
Authors
Haziza Frédéric (Uppsala)
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Meyer Roland (UNIKL)
Wolf Sebastian (UNIKL)
URL
Keywords
pointer race
pointer race freedom

garbage collecting semantics
memory managed semantics
thread modular reasoning
Abstract
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessors control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of up to two orders of magnitude.
Annotation
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessors control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of up to two orders of magnitude.
Published
2016
Pages
393-412
Proceedings
Verification, Model Checking, and Abstract Interpretation (VMCAI)
Series
Lecture Notes in Computer Science
Volume
9583
Conference
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)/Symposium on Principles of Programming Languages (POPL 2016), St. Petersburg, Florida, US
ISBN
978-3-662-49121-8
Publisher
Springer Verlag
Place
Berlin, DE
DOI
BibTeX
@INPROCEEDINGS{FITPUB11065,
   author = "Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k and Roland Meyer and Sebastian Wolf",
   title = "Pointer Race Freedom",
   pages = "393--412",
   booktitle = "Verification, Model Checking, and Abstract Interpretation (VMCAI)",
   series = "Lecture Notes in Computer Science",
   volume = 9583,
   year = 2016,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-662-49121-8",
   doi = "10.1007/978-3-662-49122-5\_19",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11065"
}
Back to top