uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Pointer Race Freedom
Uppsala University, Disciplinary Domain of Science and Technology, Biology, Department of Cell and Molecular Biology, Computational Biology and Bioinformatics. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Brno Univ Technol, CS-61090 Brno, Czech Republic..
Univ Kaiserslautern, D-67663 Kaiserslautern, Germany..
Univ Kaiserslautern, D-67663 Kaiserslautern, Germany..
2016 (English)In: Verification, Model Checking, And Abstract Interpretation, VMCAI 2016, Springer, 2016, 393-412 p.Conference paper (Refereed)Text
Abstract [en]

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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9583
National Category
Computer Engineering
Identifiers
URN: urn:nbn:se:uu:diva-299664DOI: 10.1007/978-3-662-49122-5_19ISI: 000375148800019ISBN: 9783662491225; 9783662491218OAI: oai:DiVA.org:uu-299664DiVA: diva2:949900
Conference
17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), JAN 17-19, 2016, St Petersburg, FL
Available from: 2016-07-25 Created: 2016-07-25 Last updated: 2016-07-25Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Haziza, FrédéricHolík, Lukás
By organisation
Computational Biology and BioinformaticsDepartment of Information TechnologyComputer Systems
Computer Engineering

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 108 hits
ReferencesLink to record
Permanent link

Direct link