Informace o publikaci
Model checking in a development workflow: A study on a concurrent C++ hash table
| Autoři | |
|---|---|
| Rok publikování | 2020 |
| Druh | Článek ve sborníku |
| Konference | Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-030-54994-7_5 |
| Klíčová slova | DIVINE; formal verification; model checking; C++; hash table; concurrency |
| Popis | 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. |