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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00070191" target="_blank" >RIV/00216224:14330/13:00070191 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1109/ACSD.2013.8" target="_blank" >http://dx.doi.org/10.1109/ACSD.2013.8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ACSD.2013.8" target="_blank" >10.1109/ACSD.2013.8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/LG13010" target="_blank" >LG13010: Zastoupení ČR v European Research Consortium for Informatics and Mathematics</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2013

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

Proceedings of Application of Concurrency to System Design, 2013

ISBN

9780769550350

ISSN

1550-4808

e-ISSN

—

Počet stran výsledku

9

Strana od-do

51-59

Název nakladatele

IEEE Computer Society

Místo vydání

Barcelona

Místo konání akce

Barcelona

Datum konání akce

1. 1. 2013

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

WRD - Celosvětová akce

Kód UT WoS článku

—