Ontology type: schema:Chapter
2020-08-13
AUTHORS ABSTRACTIn 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... »
PAGES46-60
Formal Methods. FM 2019 International Workshops
ISBN
978-3-030-54993-0
978-3-030-54994-7
http://scigraph.springernature.com/pub.10.1007/978-3-030-54994-7_5
DOIhttp://dx.doi.org/10.1007/978-3-030-54994-7_5
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1130066010
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
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