Pointer Race Freedom
2016 (English)In: Verification, Model Checking, And Abstract Interpretation, VMCAI 2016, Springer, 2016, 393-412 p.Conference paper (Refereed)Text
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 accessor's 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 speedup of up to two orders of magnitude.
Place, publisher, year, edition, pages
Springer, 2016. 393-412 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9583
IdentifiersURN: urn:nbn:se:uu:diva-299664DOI: 10.1007/978-3-662-49122-5_19ISI: 000375148800019ISBN: 9783662491225; 9783662491218OAI: oai:DiVA.org:uu-299664DiVA: diva2:949900
17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), JAN 17-19, 2016, St Petersburg, FL