Ontology type: schema:Chapter
2014
AUTHORSKfir Lev-Ari , Gregory Chockler , Idit Keidar
ABSTRACTWe study the correctness of shared data structures under reads-write concurrency. A popular approach to ensuring correctness of read-only operations in the presence of concurrent update, is read-set validation, which checks that all read variables have not changed since they were first read. In practice, this approach is often too conservative, which adversely affects performance. In this paper, we introduce a new framework for reasoning about correctness of data structures under reads-write concurrency, which replaces validation of the entire read-set with more general criteria. Namely, instead of verifying that all read shared variables still hold the values read from them, we verify abstract conditions over the shared variables, which we call base conditions. We show that reading values that satisfy some base condition at every point in time implies correctness of read-only operations executing in parallel with updates. Somewhat surprisingly, the resulting correctness guarantee is not equivalent to linearizability, and is instead captured through two new conditions: validity and regularity. Roughly speaking, the former requires that a read-only operation never reaches a state unreachable in a sequential execution; the latter generalizes Lamport’s notion of regularity for arbitrary data structures, and is weaker than linearizability. We further extend our framework to capture also linearizability. We illustrate how our framework can be applied for reasoning about correctness of a variety of implementations of data structures such as linked lists. More... »
PAGES273-287
Distributed Computing
ISBN
978-3-662-45173-1
978-3-662-45174-8
http://scigraph.springernature.com/pub.10.1007/978-3-662-45174-8_19
DOIhttp://dx.doi.org/10.1007/978-3-662-45174-8_19
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1021461795
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": "EE Department, Technion, Israel",
"id": "http://www.grid.ac/institutes/grid.6451.6",
"name": [
"EE Department, Technion, Israel"
],
"type": "Organization"
},
"familyName": "Lev-Ari",
"givenName": "Kfir",
"id": "sg:person.015102252173.54",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015102252173.54"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "CS Department, Royal Holloway, UK",
"id": "http://www.grid.ac/institutes/grid.4970.a",
"name": [
"CS Department, Royal Holloway, UK"
],
"type": "Organization"
},
"familyName": "Chockler",
"givenName": "Gregory",
"id": "sg:person.015624006737.84",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015624006737.84"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "EE Department, Technion, Israel",
"id": "http://www.grid.ac/institutes/grid.6451.6",
"name": [
"EE Department, Technion, Israel"
],
"type": "Organization"
},
"familyName": "Keidar",
"givenName": "Idit",
"id": "sg:person.07674464077.03",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07674464077.03"
],
"type": "Person"
}
],
"datePublished": "2014",
"datePublishedReg": "2014-01-01",
"description": "We study the correctness of shared data structures under reads-write concurrency. A popular approach to ensuring correctness of read-only operations in the presence of concurrent update, is read-set validation, which checks that all read variables have not changed since they were first read. In practice, this approach is often too conservative, which adversely affects performance. In this paper, we introduce a new framework for reasoning about correctness of data structures under reads-write concurrency, which replaces validation of the entire read-set with more general criteria. Namely, instead of verifying that all read shared variables still hold the values read from them, we verify abstract conditions over the shared variables, which we call base conditions. We show that reading values that satisfy some base condition at every point in time implies correctness of read-only operations executing in parallel with updates. Somewhat surprisingly, the resulting correctness guarantee is not equivalent to linearizability, and is instead captured through two new conditions: validity and regularity. Roughly speaking, the former requires that a read-only operation never reaches a state unreachable in a sequential execution; the latter generalizes Lamport\u2019s notion of regularity for arbitrary data structures, and is weaker than linearizability. We further extend our framework to capture also linearizability. We illustrate how our framework can be applied for reasoning about correctness of a variety of implementations of data structures such as linked lists.",
"editor": [
{
"familyName": "Kuhn",
"givenName": "Fabian",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/978-3-662-45174-8_19",
"inLanguage": "en",
"isAccessibleForFree": false,
"isPartOf": {
"isbn": [
"978-3-662-45173-1",
"978-3-662-45174-8"
],
"name": "Distributed Computing",
"type": "Book"
},
"keywords": [
"data structure",
"arbitrary data structures",
"variety of implementations",
"concurrent updates",
"correctness guarantees",
"sequential execution",
"concurrency",
"correctness",
"popular approach",
"new framework",
"framework",
"linearizability",
"update",
"execution",
"operation",
"guarantees",
"implementation",
"more general criteria",
"validation",
"abstract conditions",
"performance",
"notion",
"list",
"parallel",
"general criteria",
"new conditions",
"regularity",
"structure",
"variety",
"point",
"time",
"variables",
"state",
"practice",
"criteria",
"validity",
"values",
"base conditions",
"conditions",
"presence",
"approach",
"paper"
],
"name": "On Correctness of Data Structures under Reads-Write Concurrency",
"pagination": "273-287",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1021461795"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/978-3-662-45174-8_19"
]
}
],
"publisher": {
"name": "Springer Nature",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/978-3-662-45174-8_19",
"https://app.dimensions.ai/details/publication/pub.1021461795"
],
"sdDataset": "chapters",
"sdDatePublished": "2022-05-10T10:47",
"sdLicense": "https://scigraph.springernature.com/explorer/license/",
"sdPublisher": {
"name": "Springer Nature - SN SciGraph project",
"type": "Organization"
},
"sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_323.jsonl",
"type": "Chapter",
"url": "https://doi.org/10.1007/978-3-662-45174-8_19"
}
]
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-662-45174-8_19'
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-662-45174-8_19'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-45174-8_19'
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-662-45174-8_19'
This table displays all metadata directly associated to this object as RDF triples.
119 TRIPLES
23 PREDICATES
68 URIs
61 LITERALS
7 BLANK NODES
Subject | Predicate | Object | |
---|---|---|---|
1 | sg:pub.10.1007/978-3-662-45174-8_19 | schema:about | anzsrc-for:08 |
2 | ″ | ″ | anzsrc-for:0803 |
3 | ″ | schema:author | N4a5e409a592049bd9c097e5c6cd99062 |
4 | ″ | schema:datePublished | 2014 |
5 | ″ | schema:datePublishedReg | 2014-01-01 |
6 | ″ | schema:description | We study the correctness of shared data structures under reads-write concurrency. A popular approach to ensuring correctness of read-only operations in the presence of concurrent update, is read-set validation, which checks that all read variables have not changed since they were first read. In practice, this approach is often too conservative, which adversely affects performance. In this paper, we introduce a new framework for reasoning about correctness of data structures under reads-write concurrency, which replaces validation of the entire read-set with more general criteria. Namely, instead of verifying that all read shared variables still hold the values read from them, we verify abstract conditions over the shared variables, which we call base conditions. We show that reading values that satisfy some base condition at every point in time implies correctness of read-only operations executing in parallel with updates. Somewhat surprisingly, the resulting correctness guarantee is not equivalent to linearizability, and is instead captured through two new conditions: validity and regularity. Roughly speaking, the former requires that a read-only operation never reaches a state unreachable in a sequential execution; the latter generalizes Lamport’s notion of regularity for arbitrary data structures, and is weaker than linearizability. We further extend our framework to capture also linearizability. We illustrate how our framework can be applied for reasoning about correctness of a variety of implementations of data structures such as linked lists. |
7 | ″ | schema:editor | N0e60cff25a3240cead26e7a42e897c83 |
8 | ″ | schema:genre | chapter |
9 | ″ | schema:inLanguage | en |
10 | ″ | schema:isAccessibleForFree | false |
11 | ″ | schema:isPartOf | N949f362a195a4fca9f39f62ab9bc7714 |
12 | ″ | schema:keywords | abstract conditions |
13 | ″ | ″ | approach |
14 | ″ | ″ | arbitrary data structures |
15 | ″ | ″ | base conditions |
16 | ″ | ″ | concurrency |
17 | ″ | ″ | concurrent updates |
18 | ″ | ″ | conditions |
19 | ″ | ″ | correctness |
20 | ″ | ″ | correctness guarantees |
21 | ″ | ″ | criteria |
22 | ″ | ″ | data structure |
23 | ″ | ″ | execution |
24 | ″ | ″ | framework |
25 | ″ | ″ | general criteria |
26 | ″ | ″ | guarantees |
27 | ″ | ″ | implementation |
28 | ″ | ″ | linearizability |
29 | ″ | ″ | list |
30 | ″ | ″ | more general criteria |
31 | ″ | ″ | new conditions |
32 | ″ | ″ | new framework |
33 | ″ | ″ | notion |
34 | ″ | ″ | operation |
35 | ″ | ″ | paper |
36 | ″ | ″ | parallel |
37 | ″ | ″ | performance |
38 | ″ | ″ | point |
39 | ″ | ″ | popular approach |
40 | ″ | ″ | practice |
41 | ″ | ″ | presence |
42 | ″ | ″ | regularity |
43 | ″ | ″ | sequential execution |
44 | ″ | ″ | state |
45 | ″ | ″ | structure |
46 | ″ | ″ | time |
47 | ″ | ″ | update |
48 | ″ | ″ | validation |
49 | ″ | ″ | validity |
50 | ″ | ″ | values |
51 | ″ | ″ | variables |
52 | ″ | ″ | variety |
53 | ″ | ″ | variety of implementations |
54 | ″ | schema:name | On Correctness of Data Structures under Reads-Write Concurrency |
55 | ″ | schema:pagination | 273-287 |
56 | ″ | schema:productId | N4d1b4599bc2b4495acd11e02b361fc7d |
57 | ″ | ″ | Nd4dfe428159e43dab06a41fe8746fb48 |
58 | ″ | schema:publisher | N07138c298dd8490d9c1a146d56e7d342 |
59 | ″ | schema:sameAs | https://app.dimensions.ai/details/publication/pub.1021461795 |
60 | ″ | ″ | https://doi.org/10.1007/978-3-662-45174-8_19 |
61 | ″ | schema:sdDatePublished | 2022-05-10T10:47 |
62 | ″ | schema:sdLicense | https://scigraph.springernature.com/explorer/license/ |
63 | ″ | schema:sdPublisher | Nb54cba9cf88146a6a1fbabf086273be9 |
64 | ″ | schema:url | https://doi.org/10.1007/978-3-662-45174-8_19 |
65 | ″ | sgo:license | sg:explorer/license/ |
66 | ″ | sgo:sdDataset | chapters |
67 | ″ | rdf:type | schema:Chapter |
68 | N07138c298dd8490d9c1a146d56e7d342 | schema:name | Springer Nature |
69 | ″ | rdf:type | schema:Organisation |
70 | N0e60cff25a3240cead26e7a42e897c83 | rdf:first | N1852c91fcee64ecf951390dd6cb10961 |
71 | ″ | rdf:rest | rdf:nil |
72 | N1852c91fcee64ecf951390dd6cb10961 | schema:familyName | Kuhn |
73 | ″ | schema:givenName | Fabian |
74 | ″ | rdf:type | schema:Person |
75 | N4a5e409a592049bd9c097e5c6cd99062 | rdf:first | sg:person.015102252173.54 |
76 | ″ | rdf:rest | Ncfd507e47bcb4d16b5d1f5e7dec3dc2e |
77 | N4d1b4599bc2b4495acd11e02b361fc7d | schema:name | dimensions_id |
78 | ″ | schema:value | pub.1021461795 |
79 | ″ | rdf:type | schema:PropertyValue |
80 | N949f362a195a4fca9f39f62ab9bc7714 | schema:isbn | 978-3-662-45173-1 |
81 | ″ | ″ | 978-3-662-45174-8 |
82 | ″ | schema:name | Distributed Computing |
83 | ″ | rdf:type | schema:Book |
84 | Nb54cba9cf88146a6a1fbabf086273be9 | schema:name | Springer Nature - SN SciGraph project |
85 | ″ | rdf:type | schema:Organization |
86 | Ncfd507e47bcb4d16b5d1f5e7dec3dc2e | rdf:first | sg:person.015624006737.84 |
87 | ″ | rdf:rest | Nd3681f3f41664ca4b62deb01185c6f2f |
88 | Nd3681f3f41664ca4b62deb01185c6f2f | rdf:first | sg:person.07674464077.03 |
89 | ″ | rdf:rest | rdf:nil |
90 | Nd4dfe428159e43dab06a41fe8746fb48 | schema:name | doi |
91 | ″ | schema:value | 10.1007/978-3-662-45174-8_19 |
92 | ″ | rdf:type | schema:PropertyValue |
93 | anzsrc-for:08 | schema:inDefinedTermSet | anzsrc-for: |
94 | ″ | schema:name | Information and Computing Sciences |
95 | ″ | rdf:type | schema:DefinedTerm |
96 | anzsrc-for:0803 | schema:inDefinedTermSet | anzsrc-for: |
97 | ″ | schema:name | Computer Software |
98 | ″ | rdf:type | schema:DefinedTerm |
99 | sg:person.015102252173.54 | schema:affiliation | grid-institutes:grid.6451.6 |
100 | ″ | schema:familyName | Lev-Ari |
101 | ″ | schema:givenName | Kfir |
102 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015102252173.54 |
103 | ″ | rdf:type | schema:Person |
104 | sg:person.015624006737.84 | schema:affiliation | grid-institutes:grid.4970.a |
105 | ″ | schema:familyName | Chockler |
106 | ″ | schema:givenName | Gregory |
107 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015624006737.84 |
108 | ″ | rdf:type | schema:Person |
109 | sg:person.07674464077.03 | schema:affiliation | grid-institutes:grid.6451.6 |
110 | ″ | schema:familyName | Keidar |
111 | ″ | schema:givenName | Idit |
112 | ″ | schema:sameAs | https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07674464077.03 |
113 | ″ | rdf:type | schema:Person |
114 | grid-institutes:grid.4970.a | schema:alternateName | CS Department, Royal Holloway, UK |
115 | ″ | schema:name | CS Department, Royal Holloway, UK |
116 | ″ | rdf:type | schema:Organization |
117 | grid-institutes:grid.6451.6 | schema:alternateName | EE Department, Technion, Israel |
118 | ″ | schema:name | EE Department, Technion, Israel |
119 | ″ | rdf:type | schema:Organization |