Model checking in a development workflow: A study on a
concurrent C++ hash table

D 2020

Model checking in a development workflow: A study on a concurrent C++ hash table

ROČKAI, Petr

Základní údaje

Originální název

Model checking in a development workflow: A study on a concurrent C++ hash table

Autoři

ROČKAI, Petr (703 Slovensko, garant, domácí)

Vydání

Cham, Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019), od s. 46-60, 15 s. 2020

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

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"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00116774

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-54993-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-54994-7_5

Klíčová slova anglicky

DIVINE; formal verification; model checking; C++; hash table; concurrency

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 10. 2020 02:50, RNDr. Petr Ročkai, Ph.D.

Anotace

V originále

In this paper, we report on our effort to design a fast, concurrent-safe hash table and implement it in C++, correctly. It is especially the latter that is the focus of this paper: concurrent data structures are notoriously hard to implement, and C++ is not known to be a particularly safe language. It however does offer unparalleled performance for the level of programming comfort it offers, especially in our area of interest – parallel workloads with intense interaction. For these reasons, we have enlisted the help of a software model checker (DIVINE) with the ability to directly check the C++ implementation. We discuss how such a heavyweight tool integrated with the engineering effort, what are the current limits of this approach and what kinds of assurances we obtained. Of course, we have applied the standard array of tools throughout the effort – unit testing, an interactive debugger, a memory error checker (valgrind) – in addition to the model checker, which puts us in an excellent position to weigh them against each other and point out where they complement each other.

Citovat

ROČKAI, Petr. Model checking in a development workflow: A study on a concurrent C++ hash table. In Nelma Moreira and Emil Sekerinski. Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019). Cham: Springer International Publishing, 2020, s. 46-60. ISBN 978-3-030-54993-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-54994-7_5.

@inproceedings{1688016,
   author = {Ročkai, Petr},
   address = {Cham},
   booktitle = {Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019)},
   doi = {http://dx.doi.org/10.1007/978-3-030-54994-7_5},
   editor = {Nelma Moreira and Emil Sekerinski},
   keywords = {DIVINE; formal verification; model checking; C++; hash table; concurrency},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-54993-0},
   note = {held as part of the Third World Congress on Formal Methods, FM 2019; to appear},
   pages = {46-60},
   publisher = {Springer International Publishing},
   title = {Model checking in a development workflow: A study on a concurrent C++ hash table},
   year = {2020}
}

TY  - JOUR
ID  - 1688016
AU  - Ročkai, Petr
PY  - 2020
TI  - Model checking in a development workflow: A study on a concurrent C++ hash table
PB  - Springer International Publishing
CY  - Cham
SN  - 9783030549930
N1  - held as part of the Third World Congress on Formal Methods, FM 2019; to appear
KW  - DIVINE
KW  - formal verification
KW  - model checking
KW  - C++
KW  - hash table
KW  - concurrency
N2  - In this paper, we report on our effort to design a fast, concurrent-safe hash table and implement it in C++, correctly. It is especially the latter that is the focus of this paper: concurrent data structures are notoriously hard to implement, and C++ is not known to be a particularly safe language. It however does offer unparalleled performance for the level of programming comfort it offers, especially in our area of interest – parallel workloads with intense interaction. For these reasons, we have enlisted the help of a software model checker (DIVINE) with the ability to directly check the C++ implementation. We discuss how such a heavyweight tool integrated with the engineering effort, what are the current limits of this approach and what kinds of assurances we obtained. Of course, we have applied the standard array of tools throughout the effort – unit testing, an interactive debugger, a memory error checker (valgrind) – in addition to the model checker, which puts us in an excellent position to weigh them against each other and point out where they complement each other.
ER  -

ROČKAI, Petr. Model checking in a development workflow: A study on a concurrent C++ hash table. In Nelma Moreira and Emil Sekerinski. \textit{Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019)}. Cham: Springer International Publishing, 2020, s.~46-60. ISBN~978-3-030-54993-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-54994-7\_{}5.

Podrobný výpis o publikaci