Detail publikačního výsledku

Pointer Race Freedom

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

Originální název

Pointer Race Freedom

Anglický název

Pointer Race Freedom

Druh

Stať ve sborníku v databázi WoS či Scopus

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.

Anglický 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

Klíčová slova v angličtině

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.

Rok RIV

2017

Vydáno

07.01.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

Svazek

9583

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