Local Nontermination Detection for Parallel C++ Programs

D 2019

Local Nontermination Detection for Parallel C++ Programs

ŠTILL, Vladimír a Jiří BARNAT

Základní údaje

Originální název

Local Nontermination Detection for Parallel C++ Programs

Autoři

ŠTILL, Vladimír (203 Česká republika, garant, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Cham, International Conference on Software Engineering and Formal Methods, od s. 373-390, 18 s. 2019

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

Author's page Publisher's page

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107759

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-30445-4

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-30446-1_20

UT WoS

000716915400018

Klíčová slova anglicky

termination; nontermination; local nontermination; parallel programs; c++; model checking; DIVINE

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2020 00:04, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

One of the key problems with parallel programs is ensuring that they do not hang or wait indefinitely – i.e. there are no deadlocks, livelocks and the program proceeds towards its goals. In this work, we present a practical approach to detection of nonterminating sections of programs written in C or C++, and its implementation into the model checker. This complements the existing techniques for finding safety violations such as assertion failures and memory errors. Our approach makes it possible to detect partial deadlocks and livelocks, i.e. those situations in which some of the threads are progressing normally while the others are waiting indefinitely. The approach is also applicable to programs that do not terminate (such as daemons with infinite control loops) as it can be configured to check only for termination of selected sections of the program. The termination criteria can be user-provided, however, comes with the set of built-in termination criteria suited for the analysis of programs with mutexes and other common synchronisation primitives.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

MUNI/A/1018/2018, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

ŠTILL, Vladimír a Jiří BARNAT. Local Nontermination Detection for Parallel C++ Programs. In Ölveczky P., Salaün G. International Conference on Software Engineering and Formal Methods. Cham: Springer, 2019, s. 373-390. ISBN 978-3-030-30445-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-30446-1_20.

@inproceedings{1576677,
   author = {Štill, Vladimír and Barnat, Jiří},
   address = {Cham},
   booktitle = {International Conference on Software Engineering and Formal Methods},
   doi = {http://dx.doi.org/10.1007/978-3-030-30446-1_20},
   editor = {Ölveczky P., Salaün G.},
   keywords = {termination; nontermination; local nontermination; parallel programs; c++; model checking; DIVINE},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-30445-4},
   pages = {373-390},
   publisher = {Springer},
   title = {Local Nontermination Detection for Parallel C++ Programs},
   url = {https://divine.fi.muni.cz/2019/lnterm/},
   year = {2019}
}

TY  - JOUR
ID  - 1576677
AU  - Štill, Vladimír - Barnat, Jiří
PY  - 2019
TI  - Local Nontermination Detection for Parallel C++ Programs
PB  - Springer
CY  - Cham
SN  - 9783030304454
KW  - termination
KW  - nontermination
KW  - local nontermination
KW  - parallel programs
KW  - c++
KW  - model checking
KW  - DIVINE
UR  - https://divine.fi.muni.cz/2019/lnterm/
L2  - https://link.springer.com/chapter/10.1007/978-3-030-30446-1_20
N2  - One of the key problems with parallel programs is ensuring that they do not hang or wait indefinitely – i.e. there are no deadlocks, livelocks and the program proceeds towards its goals. In this work, we present a practical approach to detection of nonterminating sections of programs written in C or C++, and its implementation into the model checker. This complements the existing techniques for finding safety violations such as assertion failures and memory errors. Our approach makes it possible to detect partial deadlocks and livelocks, i.e. those situations in which some of the threads are progressing normally while the others are waiting indefinitely. The approach is also applicable to programs that do not terminate (such as daemons with infinite control loops) as it can be configured to check only for termination of selected sections of the program. The termination criteria can be user-provided, however, comes with the set of built-in termination criteria suited for the analysis of programs with mutexes and other common synchronisation primitives.
ER  -

ŠTILL, Vladimír a Jiří BARNAT. Local Nontermination Detection for Parallel C++ Programs. In Ölveczky P., Salaün G. \textit{International Conference on Software Engineering and Formal Methods}. Cham: Springer, 2019, s.~373-390. ISBN~978-3-030-30445-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-30446-1\_{}20.

Podrobný výpis o publikaci