On Correctness of Data Structures under Reads-Write Concurrency View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2014

AUTHORS

Kfir Lev-Ari , Gregory Chockler , Idit Keidar

ABSTRACT

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

PAGES

273-287

Book

TITLE

Distributed Computing

ISBN

978-3-662-45173-1
978-3-662-45174-8

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-45174-8_19

DOI

http://dx.doi.org/10.1007/978-3-662-45174-8_19

DIMENSIONS

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


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": "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

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-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
 




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


...