Weak Memory Models as LLVM-to-LLVM Transformations View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016

AUTHORS

Vladimír Štill , Petr Ročkai , Jiří Barnat

ABSTRACT

Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs’ use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency. In our workflow, a C or C++ program is translated into LLVM bitcode, which is then automatically extended with store buffer emulation. After this transformation, the extended LLVM bitcode is model-checked against safety and/or liveness properties with our explicit-state model checker DIVINE. More... »

PAGES

144-155

Book

TITLE

Mathematical and Engineering Methods in Computer Science

ISBN

978-3-319-29816-0
978-3-319-29817-7

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-29817-7_13

DOI

http://dx.doi.org/10.1007/978-3-319-29817-7_13

DIMENSIONS

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


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": "Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u0160till", 
        "givenName": "Vladim\u00edr", 
        "id": "sg:person.016057731543.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University Brno, 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"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Barnat", 
        "givenName": "Ji\u0159\u00ed", 
        "id": "sg:person.011367557177.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2016", 
    "datePublishedReg": "2016-01-01", 
    "description": "Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs\u2019 use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency. In our workflow, a C or C++ program is translated into LLVM bitcode, which is then automatically extended with store buffer emulation. After this transformation, the extended LLVM bitcode is model-checked against safety and/or liveness properties with our explicit-state model checker DIVINE.", 
    "editor": [
      {
        "familyName": "Kofro\u0148", 
        "givenName": "Jan", 
        "type": "Person"
      }, 
      {
        "familyName": "Vojnar", 
        "givenName": "Tom\u00e1\u0161", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-29817-7_13", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-29816-0", 
        "978-3-319-29817-7"
      ], 
      "name": "Mathematical and Engineering Methods in Computer Science", 
      "type": "Book"
    }, 
    "keywords": [
      "data races", 
      "LLVM bitcode", 
      "memory model", 
      "relaxed memory models", 
      "same memory location", 
      "weak memory models", 
      "software bugs", 
      "formal verification", 
      "model checker", 
      "such bugs", 
      "source code", 
      "individual CPUs", 
      "multiple threads", 
      "typical tasks", 
      "liveness properties", 
      "memory locations", 
      "sequential consistency", 
      "bugs", 
      "verification", 
      "new approach", 
      "matter of fact", 
      "LLVM", 
      "CPU", 
      "checker", 
      "workflow", 
      "emulation", 
      "task", 
      "code", 
      "threads", 
      "model", 
      "detection", 
      "program", 
      "consistency", 
      "situation", 
      "transformation", 
      "location", 
      "use", 
      "safety", 
      "fact", 
      "properties", 
      "matter", 
      "race", 
      "absence", 
      "divine", 
      "paper", 
      "approach"
    ], 
    "name": "Weak Memory Models as LLVM-to-LLVM Transformations", 
    "pagination": "144-155", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1031634952"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-29817-7_13"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-29817-7_13", 
      "https://app.dimensions.ai/details/publication/pub.1031634952"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:14", 
    "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_13.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-29817-7_13"
  }
]
 

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-319-29817-7_13'

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-319-29817-7_13'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-29817-7_13'

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-319-29817-7_13'


 

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

124 TRIPLES      22 PREDICATES      71 URIs      64 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-29817-7_13 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N34d0e1745b8a4f6d9f973eab2263ed37
4 schema:datePublished 2016
5 schema:datePublishedReg 2016-01-01
6 schema:description Data races are among the most difficult software bugs to discover. They arise from multiple threads accessing the same memory location, a situation which is often hard to discern from source code alone. Detection of such bugs is further complicated by individual CPUs’ use of relaxed memory models. As a matter of fact, proving absence of data races is a typical task for automated formal verification. In this paper, we present a new approach for verification of multi-threaded C and C++ programs under weakened memory models (using store buffer emulation), using an unmodified model checker that assumes Sequential Consistency. In our workflow, a C or C++ program is translated into LLVM bitcode, which is then automatically extended with store buffer emulation. After this transformation, the extended LLVM bitcode is model-checked against safety and/or liveness properties with our explicit-state model checker DIVINE.
7 schema:editor Nfc3bc4b0bac141309aa51071dc7a585f
8 schema:genre chapter
9 schema:isAccessibleForFree false
10 schema:isPartOf N71b287644e8c4bc0a96590472361c30b
11 schema:keywords CPU
12 LLVM
13 LLVM bitcode
14 absence
15 approach
16 bugs
17 checker
18 code
19 consistency
20 data races
21 detection
22 divine
23 emulation
24 fact
25 formal verification
26 individual CPUs
27 liveness properties
28 location
29 matter
30 matter of fact
31 memory locations
32 memory model
33 model
34 model checker
35 multiple threads
36 new approach
37 paper
38 program
39 properties
40 race
41 relaxed memory models
42 safety
43 same memory location
44 sequential consistency
45 situation
46 software bugs
47 source code
48 such bugs
49 task
50 threads
51 transformation
52 typical tasks
53 use
54 verification
55 weak memory models
56 workflow
57 schema:name Weak Memory Models as LLVM-to-LLVM Transformations
58 schema:pagination 144-155
59 schema:productId N96d8de5942704f00abb1e40ebef3c758
60 Nb35762720e644361a1ad6c15a985a2b4
61 schema:publisher N37dae54bf06240aa8ab6dd7393647611
62 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031634952
63 https://doi.org/10.1007/978-3-319-29817-7_13
64 schema:sdDatePublished 2022-08-04T17:14
65 schema:sdLicense https://scigraph.springernature.com/explorer/license/
66 schema:sdPublisher N74252fd34b91478b9c78f8c02e93422b
67 schema:url https://doi.org/10.1007/978-3-319-29817-7_13
68 sgo:license sg:explorer/license/
69 sgo:sdDataset chapters
70 rdf:type schema:Chapter
71 N34d0e1745b8a4f6d9f973eab2263ed37 rdf:first sg:person.016057731543.01
72 rdf:rest Nad1b4ba206824074adc494a30f0ddfd7
73 N37dae54bf06240aa8ab6dd7393647611 schema:name Springer Nature
74 rdf:type schema:Organisation
75 N71b287644e8c4bc0a96590472361c30b schema:isbn 978-3-319-29816-0
76 978-3-319-29817-7
77 schema:name Mathematical and Engineering Methods in Computer Science
78 rdf:type schema:Book
79 N74252fd34b91478b9c78f8c02e93422b schema:name Springer Nature - SN SciGraph project
80 rdf:type schema:Organization
81 N8803a18c338e44e993a46359f2dc650b rdf:first sg:person.011367557177.46
82 rdf:rest rdf:nil
83 N96d8de5942704f00abb1e40ebef3c758 schema:name doi
84 schema:value 10.1007/978-3-319-29817-7_13
85 rdf:type schema:PropertyValue
86 Na74ae876427b4dd1aeb581cd5f9ed8d9 rdf:first Ne1877a76ef50468caaf9bb1ee04aac4b
87 rdf:rest rdf:nil
88 Nad1b4ba206824074adc494a30f0ddfd7 rdf:first sg:person.07377571657.86
89 rdf:rest N8803a18c338e44e993a46359f2dc650b
90 Nb35762720e644361a1ad6c15a985a2b4 schema:name dimensions_id
91 schema:value pub.1031634952
92 rdf:type schema:PropertyValue
93 Nb766c20774ca4258b2252ddad5db113f schema:familyName Kofroň
94 schema:givenName Jan
95 rdf:type schema:Person
96 Ne1877a76ef50468caaf9bb1ee04aac4b schema:familyName Vojnar
97 schema:givenName Tomáš
98 rdf:type schema:Person
99 Nfc3bc4b0bac141309aa51071dc7a585f rdf:first Nb766c20774ca4258b2252ddad5db113f
100 rdf:rest Na74ae876427b4dd1aeb581cd5f9ed8d9
101 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
102 schema:name Information and Computing Sciences
103 rdf:type schema:DefinedTerm
104 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
105 schema:name Computer Software
106 rdf:type schema:DefinedTerm
107 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
108 schema:familyName Barnat
109 schema:givenName Jiří
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
111 rdf:type schema:Person
112 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
113 schema:familyName Štill
114 schema:givenName Vladimír
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
116 rdf:type schema:Person
117 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
118 schema:familyName Ročkai
119 schema:givenName Petr
120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
121 rdf:type schema:Person
122 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic
123 schema:name Faculty of Informatics, Masaryk University Brno, Brno, Czech Republic
124 rdf:type schema:Organization
 




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


...