A Constructive Approach for Proving Data Structures’ Linearizability View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2015-11-05

AUTHORS

Kfir Lev-Ari , Gregory Chockler , Idit Keidar

ABSTRACT

We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified. More... »

PAGES

356-370

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-48653-5_24

DOI

http://dx.doi.org/10.1007/978-3-662-48653-5_24

DIMENSIONS

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


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/0806", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information Systems", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "EE Department, Technion \u2013 Israel Institute of Technology, Haifa, Israel", 
          "id": "http://www.grid.ac/institutes/grid.6451.6", 
          "name": [
            "EE Department, Technion \u2013 Israel Institute of Technology, Haifa, 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 University of London, Egham, UK", 
          "id": "http://www.grid.ac/institutes/grid.4970.a", 
          "name": [
            "CS Department, Royal Holloway University of London, Egham, 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 \u2013 Israel Institute of Technology, Haifa, Israel", 
          "id": "http://www.grid.ac/institutes/grid.6451.6", 
          "name": [
            "EE Department, Technion \u2013 Israel Institute of Technology, Haifa, 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": "2015-11-05", 
    "datePublishedReg": "2015-11-05", 
    "description": "We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.", 
    "editor": [
      {
        "familyName": "Moses", 
        "givenName": "Yoram", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-48653-5_24", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-662-48652-8", 
        "978-3-662-48653-5"
      ], 
      "name": "Distributed Computing", 
      "type": "Book"
    }, 
    "keywords": [
      "data structure", 
      "concurrent data structures", 
      "list implementation", 
      "set abstraction", 
      "prior work", 
      "linearization points", 
      "correctness", 
      "constructive approach", 
      "linearizability", 
      "sequential runs", 
      "comprehensive methodology", 
      "abstraction", 
      "methodology", 
      "implementation", 
      "key theorem", 
      "roadmap", 
      "sufficient conditions", 
      "work", 
      "point", 
      "structure", 
      "run", 
      "theorem", 
      "conditions", 
      "properties", 
      "contrast", 
      "approach", 
      "popular Lazy List implementation", 
      "Lazy List implementation", 
      "concurrent set abstraction", 
      "Proving Data Structures"
    ], 
    "name": "A Constructive Approach for Proving Data Structures\u2019 Linearizability", 
    "pagination": "356-370", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1021133142"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-48653-5_24"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-48653-5_24", 
      "https://app.dimensions.ai/details/publication/pub.1021133142"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-01-01T19:10", 
    "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_17.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-48653-5_24"
  }
]
 

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-48653-5_24'

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-48653-5_24'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-48653-5_24'

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-48653-5_24'


 

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

107 TRIPLES      23 PREDICATES      55 URIs      48 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-48653-5_24 schema:about anzsrc-for:08
2 anzsrc-for:0806
3 schema:author N7850b05872dd425eae693835c2a26598
4 schema:datePublished 2015-11-05
5 schema:datePublishedReg 2015-11-05
6 schema:description We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.
7 schema:editor Nd5e162b21998418c8998dcb91d5a0339
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N09521cda8494421980a4b2438667d027
12 schema:keywords Lazy List implementation
13 Proving Data Structures
14 abstraction
15 approach
16 comprehensive methodology
17 concurrent data structures
18 concurrent set abstraction
19 conditions
20 constructive approach
21 contrast
22 correctness
23 data structure
24 implementation
25 key theorem
26 linearizability
27 linearization points
28 list implementation
29 methodology
30 point
31 popular Lazy List implementation
32 prior work
33 properties
34 roadmap
35 run
36 sequential runs
37 set abstraction
38 structure
39 sufficient conditions
40 theorem
41 work
42 schema:name A Constructive Approach for Proving Data Structures’ Linearizability
43 schema:pagination 356-370
44 schema:productId N0ecc39ebd2d1474496267238f4139fee
45 N4a74a049b52c41cf97532f3e7c4a35d5
46 schema:publisher N1198ae8b689d4f95a89164d96cb541ce
47 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021133142
48 https://doi.org/10.1007/978-3-662-48653-5_24
49 schema:sdDatePublished 2022-01-01T19:10
50 schema:sdLicense https://scigraph.springernature.com/explorer/license/
51 schema:sdPublisher N892bbba9e58045f6b7bf4a75cd8ca711
52 schema:url https://doi.org/10.1007/978-3-662-48653-5_24
53 sgo:license sg:explorer/license/
54 sgo:sdDataset chapters
55 rdf:type schema:Chapter
56 N09521cda8494421980a4b2438667d027 schema:isbn 978-3-662-48652-8
57 978-3-662-48653-5
58 schema:name Distributed Computing
59 rdf:type schema:Book
60 N0e867cae39be4a259909a9d4e92061ae schema:familyName Moses
61 schema:givenName Yoram
62 rdf:type schema:Person
63 N0ecc39ebd2d1474496267238f4139fee schema:name doi
64 schema:value 10.1007/978-3-662-48653-5_24
65 rdf:type schema:PropertyValue
66 N1198ae8b689d4f95a89164d96cb541ce schema:name Springer Nature
67 rdf:type schema:Organisation
68 N4a74a049b52c41cf97532f3e7c4a35d5 schema:name dimensions_id
69 schema:value pub.1021133142
70 rdf:type schema:PropertyValue
71 N7850b05872dd425eae693835c2a26598 rdf:first sg:person.015102252173.54
72 rdf:rest N7da3df733cbf47b1bcef5e739870aa4b
73 N7da3df733cbf47b1bcef5e739870aa4b rdf:first sg:person.015624006737.84
74 rdf:rest Ndc3bc6922674426b99891f4bdd7f480b
75 N892bbba9e58045f6b7bf4a75cd8ca711 schema:name Springer Nature - SN SciGraph project
76 rdf:type schema:Organization
77 Nd5e162b21998418c8998dcb91d5a0339 rdf:first N0e867cae39be4a259909a9d4e92061ae
78 rdf:rest rdf:nil
79 Ndc3bc6922674426b99891f4bdd7f480b rdf:first sg:person.07674464077.03
80 rdf:rest rdf:nil
81 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
82 schema:name Information and Computing Sciences
83 rdf:type schema:DefinedTerm
84 anzsrc-for:0806 schema:inDefinedTermSet anzsrc-for:
85 schema:name Information Systems
86 rdf:type schema:DefinedTerm
87 sg:person.015102252173.54 schema:affiliation grid-institutes:grid.6451.6
88 schema:familyName Lev-Ari
89 schema:givenName Kfir
90 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015102252173.54
91 rdf:type schema:Person
92 sg:person.015624006737.84 schema:affiliation grid-institutes:grid.4970.a
93 schema:familyName Chockler
94 schema:givenName Gregory
95 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015624006737.84
96 rdf:type schema:Person
97 sg:person.07674464077.03 schema:affiliation grid-institutes:grid.6451.6
98 schema:familyName Keidar
99 schema:givenName Idit
100 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07674464077.03
101 rdf:type schema:Person
102 grid-institutes:grid.4970.a schema:alternateName CS Department, Royal Holloway University of London, Egham, UK
103 schema:name CS Department, Royal Holloway University of London, Egham, UK
104 rdf:type schema:Organization
105 grid-institutes:grid.6451.6 schema:alternateName EE Department, Technion – Israel Institute of Technology, Haifa, Israel
106 schema:name EE Department, Technion – Israel Institute of Technology, Haifa, Israel
107 rdf:type schema:Organization
 




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


...