Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2020-08-13

AUTHORS

Petr Ročkai

ABSTRACT

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. More... »

PAGES

46-60

Book

TITLE

Formal Methods. FM 2019 International Workshops

ISBN

978-3-030-54993-0
978-3-030-54994-7

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-54994-7_5

DOI

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

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1130066010


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ro\u010dkai", 
        "givenName": "Petr", 
        "id": "sg:person.07377571657.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2020-08-13", 
    "datePublishedReg": "2020-08-13", 
    "description": "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 \u2013 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 \u2013 unit testing, an interactive debugger, a memory error checker (valgrind) \u2013 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.", 
    "editor": [
      {
        "familyName": "Sekerinski", 
        "givenName": "Emil", 
        "type": "Person"
      }, 
      {
        "familyName": "Moreira", 
        "givenName": "Nelma", 
        "type": "Person"
      }, 
      {
        "familyName": "Oliveira", 
        "givenName": "Jos\u00e9 N.", 
        "type": "Person"
      }, 
      {
        "familyName": "Ratiu", 
        "givenName": "Daniel", 
        "type": "Person"
      }, 
      {
        "familyName": "Guidotti", 
        "givenName": "Riccardo", 
        "type": "Person"
      }, 
      {
        "familyName": "Farrell", 
        "givenName": "Marie", 
        "type": "Person"
      }, 
      {
        "familyName": "Luckcuck", 
        "givenName": "Matt", 
        "type": "Person"
      }, 
      {
        "familyName": "Marmsoler", 
        "givenName": "Diego", 
        "type": "Person"
      }, 
      {
        "familyName": "Campos", 
        "givenName": "Jos\u00e9", 
        "type": "Person"
      }, 
      {
        "familyName": "Astarte", 
        "givenName": "Troy", 
        "type": "Person"
      }, 
      {
        "familyName": "Gonnord", 
        "givenName": "Laure", 
        "type": "Person"
      }, 
      {
        "familyName": "Cerone", 
        "givenName": "Antonio", 
        "type": "Person"
      }, 
      {
        "familyName": "Couto", 
        "givenName": "Luis", 
        "type": "Person"
      }, 
      {
        "familyName": "Dongol", 
        "givenName": "Brijesh", 
        "type": "Person"
      }, 
      {
        "familyName": "Kutrib", 
        "givenName": "Martin", 
        "type": "Person"
      }, 
      {
        "familyName": "Monteiro", 
        "givenName": "Pedro", 
        "type": "Person"
      }, 
      {
        "familyName": "Delmas", 
        "givenName": "David", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-54994-7_5", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-030-54993-0", 
        "978-3-030-54994-7"
      ], 
      "name": "Formal Methods. FM 2019 International Workshops", 
      "type": "Book"
    }, 
    "keywords": [
      "hash table", 
      "model checker", 
      "software model checkers", 
      "concurrent data structures", 
      "programming comfort", 
      "interactive debugger", 
      "safe language", 
      "data structure", 
      "development workflow", 
      "error checker", 
      "checker", 
      "kind of assurance", 
      "unparalleled performance", 
      "engineering efforts", 
      "debugger", 
      "workflow", 
      "tool", 
      "workload", 
      "table", 
      "standard array", 
      "implementation", 
      "language", 
      "assurance", 
      "performance", 
      "efforts", 
      "help", 
      "kind", 
      "model", 
      "focus", 
      "comfort", 
      "intense interaction", 
      "testing", 
      "ability", 
      "current limits", 
      "array", 
      "position", 
      "area", 
      "reasons", 
      "interaction", 
      "structure", 
      "addition", 
      "levels", 
      "study", 
      "limit", 
      "excellent position", 
      "paper", 
      "approach"
    ], 
    "name": "Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table", 
    "pagination": "46-60", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1130066010"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-54994-7_5"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-54994-7_5", 
      "https://app.dimensions.ai/details/publication/pub.1130066010"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:16", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220804/entities/gbq_results/chapter/chapter_195.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-54994-7_5"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-54994-7_5'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-54994-7_5'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-54994-7_5'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-54994-7_5'


 

This table displays all metadata directly associated to this object as RDF triples.

186 TRIPLES      22 PREDICATES      71 URIs      64 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-54994-7_5 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author Nc02c9eb582ca4f57a272c2d031af056a
4 schema:datePublished 2020-08-13
5 schema:datePublishedReg 2020-08-13
6 schema:description 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.
7 schema:editor N2cab77f654824b4f916897050907fb14
8 schema:genre chapter
9 schema:isAccessibleForFree false
10 schema:isPartOf N402a240c518c4e5e82dd92fb79287fd4
11 schema:keywords ability
12 addition
13 approach
14 area
15 array
16 assurance
17 checker
18 comfort
19 concurrent data structures
20 current limits
21 data structure
22 debugger
23 development workflow
24 efforts
25 engineering efforts
26 error checker
27 excellent position
28 focus
29 hash table
30 help
31 implementation
32 intense interaction
33 interaction
34 interactive debugger
35 kind
36 kind of assurance
37 language
38 levels
39 limit
40 model
41 model checker
42 paper
43 performance
44 position
45 programming comfort
46 reasons
47 safe language
48 software model checkers
49 standard array
50 structure
51 study
52 table
53 testing
54 tool
55 unparalleled performance
56 workflow
57 workload
58 schema:name Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table
59 schema:pagination 46-60
60 schema:productId N167e4291543a4721827f863772daa70d
61 N1b9b354a79de44afb457dfcf438a06dd
62 schema:publisher N645a73cb4cf9451791d0f214697c6a65
63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1130066010
64 https://doi.org/10.1007/978-3-030-54994-7_5
65 schema:sdDatePublished 2022-08-04T17:16
66 schema:sdLicense https://scigraph.springernature.com/explorer/license/
67 schema:sdPublisher N9476a8c8012e425a9963464f934af554
68 schema:url https://doi.org/10.1007/978-3-030-54994-7_5
69 sgo:license sg:explorer/license/
70 sgo:sdDataset chapters
71 rdf:type schema:Chapter
72 N0a3a4f635482425d9b1c5ebdf84e3a87 rdf:first N3a44df3f3281426ab18a594399bd5cd6
73 rdf:rest Nbced853965924431a94deb1cb6baf635
74 N167e4291543a4721827f863772daa70d schema:name doi
75 schema:value 10.1007/978-3-030-54994-7_5
76 rdf:type schema:PropertyValue
77 N1b9b354a79de44afb457dfcf438a06dd schema:name dimensions_id
78 schema:value pub.1130066010
79 rdf:type schema:PropertyValue
80 N231feea3e43c47e8924320b55168afaf rdf:first Nc5ae90c5e96043c2ac01a9d064becce0
81 rdf:rest N36222942b959451c8a48cae8a138fb95
82 N263ff8feb028464d92afa6f795a8b795 schema:familyName Luckcuck
83 schema:givenName Matt
84 rdf:type schema:Person
85 N272bdceaab1e48b38193e692010bfc59 rdf:first Na3c59ba329194e97a550f09cd7a705c2
86 rdf:rest N7ab5214c23f84dc49b4c66144286512c
87 N282c7cfca0844ae2861db8c0cec6b0f8 schema:familyName Ratiu
88 schema:givenName Daniel
89 rdf:type schema:Person
90 N2b16e37cc5584de3a4e751c6f1f4e4ea schema:familyName Kutrib
91 schema:givenName Martin
92 rdf:type schema:Person
93 N2cab77f654824b4f916897050907fb14 rdf:first N828bb95a1f9544ddbdf3422816027877
94 rdf:rest Nc67d7a7dd5ce47a3a58eb3f468742123
95 N321900a2d32a45d6920c5181162f1269 rdf:first Nd31f6d1bf4af49d4809ea33ffd417e44
96 rdf:rest N81c7943abc71465c87d95fb55df36b43
97 N36222942b959451c8a48cae8a138fb95 rdf:first N67c211a4059f4ee192435861474d5e95
98 rdf:rest N0a3a4f635482425d9b1c5ebdf84e3a87
99 N3a44df3f3281426ab18a594399bd5cd6 schema:familyName Gonnord
100 schema:givenName Laure
101 rdf:type schema:Person
102 N3af0b5a6421e41219f4e32a65ed1e7c6 schema:familyName Couto
103 schema:givenName Luis
104 rdf:type schema:Person
105 N402a240c518c4e5e82dd92fb79287fd4 schema:isbn 978-3-030-54993-0
106 978-3-030-54994-7
107 schema:name Formal Methods. FM 2019 International Workshops
108 rdf:type schema:Book
109 N469736edc3f14a269b832281c42a6039 schema:familyName Marmsoler
110 schema:givenName Diego
111 rdf:type schema:Person
112 N557071bb8a424408a1a94a847b6a444f schema:familyName Guidotti
113 schema:givenName Riccardo
114 rdf:type schema:Person
115 N5f8c849298e341469b36f19fa6b215a9 rdf:first Ne03a61fe834b4dc8823d53bcbb9f3ce0
116 rdf:rest N67a6f260199240d1948133cfd2a64450
117 N5f90bd0cbcc14e57a2ee197b37c99441 schema:familyName Moreira
118 schema:givenName Nelma
119 rdf:type schema:Person
120 N62712316afff493ea0d831afed2d6d31 schema:familyName Delmas
121 schema:givenName David
122 rdf:type schema:Person
123 N645a73cb4cf9451791d0f214697c6a65 schema:name Springer Nature
124 rdf:type schema:Organisation
125 N67a6f260199240d1948133cfd2a64450 rdf:first N2b16e37cc5584de3a4e751c6f1f4e4ea
126 rdf:rest N8dc564ef891f4fa281344679f1be11bf
127 N67c211a4059f4ee192435861474d5e95 schema:familyName Astarte
128 schema:givenName Troy
129 rdf:type schema:Person
130 N695d0d5a31ee408c989391ec670d386b schema:familyName Cerone
131 schema:givenName Antonio
132 rdf:type schema:Person
133 N75aa93612f014b3a8ea608af630958a8 rdf:first N62712316afff493ea0d831afed2d6d31
134 rdf:rest rdf:nil
135 N7ab5214c23f84dc49b4c66144286512c rdf:first N282c7cfca0844ae2861db8c0cec6b0f8
136 rdf:rest N8b8b707dd716405c8fcb12223dd92969
137 N81c7943abc71465c87d95fb55df36b43 rdf:first N263ff8feb028464d92afa6f795a8b795
138 rdf:rest Nf34f7813b0e74027be7a77bd87c29251
139 N828bb95a1f9544ddbdf3422816027877 schema:familyName Sekerinski
140 schema:givenName Emil
141 rdf:type schema:Person
142 N89ed1cdfe65c42f583431d01b5d756cc rdf:first N3af0b5a6421e41219f4e32a65ed1e7c6
143 rdf:rest N5f8c849298e341469b36f19fa6b215a9
144 N8b8b707dd716405c8fcb12223dd92969 rdf:first N557071bb8a424408a1a94a847b6a444f
145 rdf:rest N321900a2d32a45d6920c5181162f1269
146 N8dc564ef891f4fa281344679f1be11bf rdf:first Ne7d6d9234e0346a285065ded9865a306
147 rdf:rest N75aa93612f014b3a8ea608af630958a8
148 N9476a8c8012e425a9963464f934af554 schema:name Springer Nature - SN SciGraph project
149 rdf:type schema:Organization
150 Na3c59ba329194e97a550f09cd7a705c2 schema:familyName Oliveira
151 schema:givenName José N.
152 rdf:type schema:Person
153 Nbced853965924431a94deb1cb6baf635 rdf:first N695d0d5a31ee408c989391ec670d386b
154 rdf:rest N89ed1cdfe65c42f583431d01b5d756cc
155 Nc02c9eb582ca4f57a272c2d031af056a rdf:first sg:person.07377571657.86
156 rdf:rest rdf:nil
157 Nc5ae90c5e96043c2ac01a9d064becce0 schema:familyName Campos
158 schema:givenName José
159 rdf:type schema:Person
160 Nc67d7a7dd5ce47a3a58eb3f468742123 rdf:first N5f90bd0cbcc14e57a2ee197b37c99441
161 rdf:rest N272bdceaab1e48b38193e692010bfc59
162 Nd31f6d1bf4af49d4809ea33ffd417e44 schema:familyName Farrell
163 schema:givenName Marie
164 rdf:type schema:Person
165 Ne03a61fe834b4dc8823d53bcbb9f3ce0 schema:familyName Dongol
166 schema:givenName Brijesh
167 rdf:type schema:Person
168 Ne7d6d9234e0346a285065ded9865a306 schema:familyName Monteiro
169 schema:givenName Pedro
170 rdf:type schema:Person
171 Nf34f7813b0e74027be7a77bd87c29251 rdf:first N469736edc3f14a269b832281c42a6039
172 rdf:rest N231feea3e43c47e8924320b55168afaf
173 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
174 schema:name Information and Computing Sciences
175 rdf:type schema:DefinedTerm
176 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
177 schema:name Computer Software
178 rdf:type schema:DefinedTerm
179 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
180 schema:familyName Ročkai
181 schema:givenName Petr
182 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
183 rdf:type schema:Person
184 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
185 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
186 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...