Conference paper

HAZIZA Frédéric, HOLÍK Lukáš, MEYER Roland and WOLF Sebastian. Pointer Race Freedom. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). 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
Publication language:english
Original title:Pointer Race Freedom
Title (cs):Absence ukazatelových závodů
Pages:393-412
Proceedings:Verification, Model Checking, and Abstract Interpretation (VMCAI)
Conference:International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)/Symposium on Principles of Programming Languages (POPL 2016)
Series:LNCS 9583
Place:Berlin, DE
Year:2016
URL:http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19
ISBN:978-3-662-49121-8
DOI:10.1007/978-3-662-49122-5_19
Publisher:Springer Verlag
Keywords
pointer race
pointer race freedom

garbage collecting semantics
memory managed semantics
thread modular reasoning
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.
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.
BibTeX:
@INPROCEEDINGS{
   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 = {LNCS 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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=11065}
}

Your IPv4 address: 34.201.121.213
Switch to https