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", 
      "correctness guarantees", 
      "concurrent updates", 
      "sequential execution", 
      "concurrency", 
      "correctness", 
      "popular approach", 
      "new framework", 
      "framework", 
      "linearizability", 
      "update", 
      "execution", 
      "operation", 
      "guarantees", 
      "implementation", 
      "more general criteria", 
      "validation", 
      "performance", 
      "abstract conditions", 
      "notion", 
      "list", 
      "general criteria", 
      "parallel", 
      "regularity", 
      "structure", 
      "point", 
      "new conditions", 
      "time", 
      "variety", 
      "variables", 
      "state", 
      "criteria", 
      "validity", 
      "practice", 
      "values", 
      "base conditions", 
      "conditions", 
      "presence", 
      "approach", 
      "paper", 
      "reads-write concurrency", 
      "read-set validation", 
      "read-only operation", 
      "Lamport's notion"
    ], 
    "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-01-01T19:17", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_30.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.

123 TRIPLES      23 PREDICATES      72 URIs      65 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 N16cebe6e5bfe4424ac7184c4ce9a86b0
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 N53d1677186f74a9594e55087c94fb823
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N61ce571ec54b4a619614292ccf253df5
12 schema:keywords Lamport's notion
13 abstract conditions
14 approach
15 arbitrary data structures
16 base conditions
17 concurrency
18 concurrent updates
19 conditions
20 correctness
21 correctness guarantees
22 criteria
23 data structure
24 execution
25 framework
26 general criteria
27 guarantees
28 implementation
29 linearizability
30 list
31 more general criteria
32 new conditions
33 new framework
34 notion
35 operation
36 paper
37 parallel
38 performance
39 point
40 popular approach
41 practice
42 presence
43 read-only operation
44 read-set validation
45 reads-write concurrency
46 regularity
47 sequential execution
48 state
49 structure
50 time
51 update
52 validation
53 validity
54 values
55 variables
56 variety
57 variety of implementations
58 schema:name On Correctness of Data Structures under Reads-Write Concurrency
59 schema:pagination 273-287
60 schema:productId Nb186a8d996b442b0852c7a2559e69904
61 Nd72f5f12af4b418fb9fe4ec5355cc2a1
62 schema:publisher N8824038d5eb746849cc47e0bbb54f0a3
63 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021461795
64 https://doi.org/10.1007/978-3-662-45174-8_19
65 schema:sdDatePublished 2022-01-01T19:17
66 schema:sdLicense https://scigraph.springernature.com/explorer/license/
67 schema:sdPublisher N0855b8d443054810a3e64be213849020
68 schema:url https://doi.org/10.1007/978-3-662-45174-8_19
69 sgo:license sg:explorer/license/
70 sgo:sdDataset chapters
71 rdf:type schema:Chapter
72 N0855b8d443054810a3e64be213849020 schema:name Springer Nature - SN SciGraph project
73 rdf:type schema:Organization
74 N16cebe6e5bfe4424ac7184c4ce9a86b0 rdf:first sg:person.015102252173.54
75 rdf:rest Nfc101712200c460090c5ea5d771f00e0
76 N53d1677186f74a9594e55087c94fb823 rdf:first Ne11957de466e437ebdc1c23e724a5f7e
77 rdf:rest rdf:nil
78 N61ce571ec54b4a619614292ccf253df5 schema:isbn 978-3-662-45173-1
79 978-3-662-45174-8
80 schema:name Distributed Computing
81 rdf:type schema:Book
82 N8824038d5eb746849cc47e0bbb54f0a3 schema:name Springer Nature
83 rdf:type schema:Organisation
84 Nb186a8d996b442b0852c7a2559e69904 schema:name dimensions_id
85 schema:value pub.1021461795
86 rdf:type schema:PropertyValue
87 Nd72f5f12af4b418fb9fe4ec5355cc2a1 schema:name doi
88 schema:value 10.1007/978-3-662-45174-8_19
89 rdf:type schema:PropertyValue
90 Ne11957de466e437ebdc1c23e724a5f7e schema:familyName Kuhn
91 schema:givenName Fabian
92 rdf:type schema:Person
93 Nf6a651a96cfc42a58f45efd31e9ceafb rdf:first sg:person.07674464077.03
94 rdf:rest rdf:nil
95 Nfc101712200c460090c5ea5d771f00e0 rdf:first sg:person.015624006737.84
96 rdf:rest Nf6a651a96cfc42a58f45efd31e9ceafb
97 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
98 schema:name Information and Computing Sciences
99 rdf:type schema:DefinedTerm
100 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
101 schema:name Computer Software
102 rdf:type schema:DefinedTerm
103 sg:person.015102252173.54 schema:affiliation grid-institutes:grid.6451.6
104 schema:familyName Lev-Ari
105 schema:givenName Kfir
106 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015102252173.54
107 rdf:type schema:Person
108 sg:person.015624006737.84 schema:affiliation grid-institutes:grid.4970.a
109 schema:familyName Chockler
110 schema:givenName Gregory
111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015624006737.84
112 rdf:type schema:Person
113 sg:person.07674464077.03 schema:affiliation grid-institutes:grid.6451.6
114 schema:familyName Keidar
115 schema:givenName Idit
116 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07674464077.03
117 rdf:type schema:Person
118 grid-institutes:grid.4970.a schema:alternateName CS Department, Royal Holloway, UK
119 schema:name CS Department, Royal Holloway, UK
120 rdf:type schema:Organization
121 grid-institutes:grid.6451.6 schema:alternateName EE Department, Technion, Israel
122 schema:name EE Department, Technion, Israel
123 rdf:type schema:Organization
 




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


...