Pointer Race Freedom

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F16%3APU121587" target="_blank" >RIV/00216305:26230/16:PU121587 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-49122-5_19" target="_blank" >10.1007/978-3-662-49122-5_19</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Pointer Race Freedom

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Pointer Race Freedom

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GP13-37876P" target="_blank" >GP13-37876P: Verifikace nekonečně stavových systémů založená na konečných automatech</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Verification, Model Checking, and Abstract Interpretation (VMCAI)

ISBN

978-3-662-49121-8

ISSN

—

e-ISSN

—

Počet stran výsledku

20

Strana od-do

393-412

Název nakladatele

Springer Verlag

Místo vydání

Berlin

Místo konání akce

St. Petersburg, Florida

Datum konání akce

17. 1. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000375148800019