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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00116774" target="_blank" >RIV/00216224:14330/20:00116774 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-54994-7_5" target="_blank" >http://dx.doi.org/10.1007/978-3-030-54994-7_5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-54994-7_5" target="_blank" >10.1007/978-3-030-54994-7_5</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2020

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

Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019)

ISBN

9783030549930

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

46-60

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Místo konání akce

Porto

Datum konání akce

1. 1. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

—