Detail publikace

Pointer Race Freedom

HOLÍK, L. MEYER, R. WOLF, S. HAZIZA, F.

Originální název

Pointer Race Freedom

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

pointer race pointer race freedom garbage collecting semantics memory managed semantics thread modular reasoning

Autoři

HOLÍK, L.; MEYER, R.; WOLF, S.; HAZIZA, F.

Vydáno

7. 1. 2016

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-662-49121-8

Kniha

Verification, Model Checking, and Abstract Interpretation (VMCAI)

Edice

Lecture Notes in Computer Science

Strany od

393

Strany do

412

Strany počet

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"
}