LTL Model Checking of Parallel Programs with Under-Approximated
TSO Memory Model

D 2013

LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model

BARNAT, Jiří, Luboš BRIM a Vojtěch HAVEL

Základní údaje

Originální název

LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model

Autoři

BARNAT, Jiří (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí) a Vojtěch HAVEL (203 Česká republika, garant, domácí)

Vydání

Barcelona, Proceedings of Application of Concurrency to System Design, 2013, od s. 51-59, 9 s. 2013

Nakladatel

IEEE Computer Society

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/13:00070191

Organizační jednotka

Fakulta informatiky

ISBN

978-0-7695-5035-0

ISSN

DOI

http://dx.doi.org/10.1109/ACSD.2013.8

UT WoS

000333827300006

Klíčová slova anglicky

LTL model checking; divine model checker; relaxed memory model

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2014 08:44, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Model checking of parallel programs under relaxed memory models has been so far limited to the verification of safety properties. Tools have been developed to automatically synthesise correct placement of synchronisation primitives to reinstate the sequential consistency. However, in practice it is not the sequential consistency that is demanded, but the correctness of the program with respect to its specification. In this paper, we introduce a new explicit-state Linear Temporal Logic model checking procedure that allows for full verification of programs under approximated Total Store Ordering memory model. We also present a workflow of automated procedure to place the synchronisation primitives into the system under inspection to make it satisfy the given specification under the approximated memory model. Our experimental evaluation has been conducted within DiVinE, our parallel and distributed-memory LTL model checker.

Návaznosti

LG13010, projekt VaV

Název: Zastoupení ČR v European Research Consortium for Informatics and Mathematics (Akronym: ERCIM-CZ)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Zastoupení ČR v European Research Consortium for Informatics and Mathematics

Citovat

BARNAT, Jiří, Luboš BRIM a Vojtěch HAVEL. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. In Juan E. Guerrero. Proceedings of Application of Concurrency to System Design, 2013. Barcelona: IEEE Computer Society, 2013, s. 51-59. ISBN 978-0-7695-5035-0. Dostupné z: https://dx.doi.org/10.1109/ACSD.2013.8.

@inproceedings{1130152,
   author = {Barnat, Jiří and Brim, Luboš and Havel, Vojtěch},
   address = {Barcelona},
   booktitle = {Proceedings of Application of Concurrency to System Design, 2013},
   doi = {http://dx.doi.org/10.1109/ACSD.2013.8},
   editor = {Juan E. Guerrero},
   keywords = {LTL model checking; divine model checker; relaxed memory model},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Barcelona},
   isbn = {978-0-7695-5035-0},
   pages = {51-59},
   publisher = {IEEE Computer Society},
   title = {LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model},
   year = {2013}
}

TY  - JOUR
ID  - 1130152
AU  - Barnat, Jiří - Brim, Luboš - Havel, Vojtěch
PY  - 2013
TI  - LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model
PB  - IEEE Computer Society
CY  - Barcelona
SN  - 9780769550350
KW  - LTL model checking
KW  - divine model checker
KW  - relaxed memory model
N2  - Model checking of parallel programs under relaxed memory models has been so far limited to the verification of safety properties. Tools have been developed to automatically synthesise correct placement of synchronisation primitives to reinstate the sequential consistency. However, in practice it is not the sequential consistency that is demanded, but the correctness of the program with respect to its specification. In this paper, we introduce a new explicit-state Linear Temporal Logic model checking procedure that allows for full verification of programs under approximated Total Store Ordering memory model. We also present a workflow of automated procedure to place the synchronisation primitives into the system under inspection to make it satisfy the given specification under the approximated memory model. Our experimental evaluation has been conducted within DiVinE, our parallel and distributed-memory LTL model checker.
ER  -

BARNAT, Jiří, Luboš BRIM a Vojtěch HAVEL. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. In Juan E. Guerrero. \textit{Proceedings of Application of Concurrency to System Design, 2013}. Barcelona: IEEE Computer Society, 2013, s.~51-59. ISBN~978-0-7695-5035-0. Dostupné z: https://dx.doi.org/10.1109/ACSD.2013.8.

Podrobný výpis o publikaci