Pointer Race Freedom

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

Pointer Race Freedom

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GP13-37876P" target="_blank" >GP13-37876P: Verification of Infinite State Systems Based on Finite Automata</a><br>

Continuities

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

Publication year

2016

Confidentiality

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

Article name in the collection

Verification, Model Checking, and Abstract Interpretation (VMCAI)

ISBN

978-3-662-49121-8

ISSN

—

e-ISSN

—

Number of pages

20

Pages from-to

393-412

Publisher name

Springer Verlag

Place of publication

Berlin

Event location

St. Petersburg, Florida

Event date

Jan 17, 2016

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000375148800019