Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/10220
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Derrick, J | - |
dc.contributor.author | Smith, G | - |
dc.contributor.author | Groves, L | - |
dc.contributor.author | Dongol, B | - |
dc.date.accessioned | 2015-02-13T12:21:18Z | - |
dc.date.available | 2014 | - |
dc.date.available | 2015-02-13T12:21:18Z | - |
dc.date.issued | 2014 | - |
dc.identifier.citation | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8855, 2014 | en_US |
dc.identifier.isbn | 9783319133379 | - |
dc.identifier.issn | 1611-3349 | - |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/10220 | - |
dc.description.abstract | Most approaches to verifying linearizability assume a sequentially consistent memory model, which is not always realised in practice. In this paper we study correctness on a weak memory model: the TSO (Total Store Order) memory model, which is implemented in x86 multicore architectures. Our central result is a proof method that simplifies proofs of linearizability on TSO. This is necessary since the use of local buffers in TSO adds considerably to the verification overhead on top of the already subtle linearizability proofs. The proof method involves constructing a coarse-grained abstraction as an intermediate layer between an abstract description and the concurrent algorithm. This allows the linearizability proof to be split into two smaller components, where the effect of the local buffers in TSO is dealt with at a higher level of abstraction than it would have been otherwise. | en_US |
dc.language.iso | en | en_US |
dc.publisher | Springer Verlag | en_US |
dc.subject | Linearizability | en_US |
dc.subject | TSO (Total Store Order) memory model | en_US |
dc.title | Using coarse-grained abstractions to verify linearizability on TSO architectures | en_US |
dc.type | Article | en_US |
dc.relation.isPartOf | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | - |
dc.relation.isPartOf | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | - |
pubs.volume | 8855 | - |
pubs.volume | 8855 | - |
pubs.organisational-data | /Brunel | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division/College of Engineering, Design and Physical Sciences | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division/College of Engineering, Design and Physical Sciences/Dept of Computer Science | - |
pubs.organisational-data | /Brunel/Brunel Staff by College/Department/Division/College of Engineering, Design and Physical Sciences/Dept of Computer Science/Computer Science | - |
Appears in Collections: | Dept of Electronic and Electrical Engineering Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 257.24 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.