Pointer Race Freedom

Název česky

Absence ukazatelových závodů

Typ

článek ve sborníku konference

Jazyk

anglicky

Autoři

Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Meyer Roland, Prof. Dr.
Wolf Sebastian (FIT)
Haziza Frédéric

URL

http://link.springer.com/chapter/10.1007%2F978-3-662-49122-5_19

Klíčová slova

ukazatelový závod svoboda od ukazatelových závodů modulární verifikace

Abstrakt

Navrhujem pojem ukazatelový závod, analogický známému pojmu datový závod, a studujeme jeho semantické důsledky. Ukazujeme, jak je jej možné použít k zefetktivnění verifikace paralelních programů rozdělením verifikačního úsilí na 1) ověření, že program neobsahuje ukazatelové závody, a 2) ověření původní vlastnosti s pomocí předpokladu z bodu 1.

Anotace

Navrhujem pojem ukazatelový závod, analogický známému pojmu datový závod, a studujeme jeho semantické důsledky. Ukazujeme, jak je jej možné použít k zefetktivnění verifikace paralelních programů rozdělením verifikačního úsilí na 1) ověření, že program neobsahuje ukazatelové závody, a 2) ověření původní vlastnosti s pomocí předpokladu z bodu 1.

Rok

2016

Strany

393–412

Sborník

Verification, Model Checking, and Abstract Interpretation (VMCAI)

Řada

Lecture Notes in Computer Science

Svazek

9583

ISBN

978-3-662-49121-8

Vydavatel

Springer Verlag

Místo

Berlin

DOI

10.1007/978-3-662-49122-5_19

UT WoS

000375148800019

EID Scopus

2-s2.0-84955241220

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