Přístupnostní navigace
E-application
Search Search Close
Publication detail
HOLÍK, L. MEYER, R. WOLF, S. HAZIZA, F.
Original Title
Pointer Race Freedom
Type
conference paper
Language
English
Original 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.
Keywords
pointer race pointer race freedom garbage collecting semantics memory managed semantics thread modular reasoning
Authors
HOLÍK, L.; MEYER, R.; WOLF, S.; HAZIZA, F.
Released
7. 1. 2016
Publisher
Springer Verlag
Location
Berlin
ISBN
978-3-662-49121-8
Book
Verification, Model Checking, and Abstract Interpretation (VMCAI)
Edition
Lecture Notes in Computer Science
Pages from
393
Pages to
412
Pages count
20
URL
http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19
BibTex
@inproceedings{BUT130931, author="Lukáš {Holík} and Roland {Meyer} and Sebastian {Wolf} and Frédéric {Haziza}", title="Pointer Race Freedom", booktitle="Verification, Model Checking, and Abstract Interpretation (VMCAI)", year="2016", series="Lecture Notes in Computer Science", volume="9583", pages="393--412", publisher="Springer Verlag", address="Berlin", doi="10.1007/978-3-662-49122-5\{_}19", isbn="978-3-662-49121-8", url="http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19" }