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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published paper (Refereed)
Resource type
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; 9783662491218 (print)OAI: 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

Altmetric score

Total: 435 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf