Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/10313
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Smith, G | - |
dc.contributor.author | Derrick, J | - |
dc.contributor.author | Dongol, B | - |
dc.date.accessioned | 2015-03-02T16:00:27Z | - |
dc.date.available | 2015 | - |
dc.date.available | 2015-03-02T16:00:27Z | - |
dc.date.issued | 2015 | - |
dc.identifier.citation | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8997: 364 - 383, (January 2015) | en_US |
dc.identifier.isbn | 978-3-319-15316-2 | - |
dc.identifier.uri | http://link.springer.com/chapter/10.1007%2F978-3-319-15317-9_22 | - |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/10313 | - |
dc.description | “The final publication is available at http://link.springer.com/chapter/10.1007%2F978-3-319-15317-9_22 ”. | en_US |
dc.description.abstract | Linearizability has become the standard correctness criterion for fine-grained non-atomic concurrent algorithms, however, most approaches assume a sequentially consistent memory model, which is not always realised in practice. In this paper we study the correctness of concurrent algorithms on a weak memory model: the TSO (Total Store Order) memory model, which is commonly implemented by multicore architectures. Here, linearizability is often too strict, and hence, we prove a weaker criterion, quiescent consistency instead. Like linearizability, quiescent consistency is compositional making it an ideal correctness criterion in a component-based context. We demonstrate how to model a typical concurrent algorithm, seqlock, and prove it quiescent consistent using a simulation-based approach. Previous approaches to proving correctness on TSO architectures have been based on linearizabilty which makes it necessary to modify the algorithm’s high-level requirements. Our approach is the first, to our knowledge, for proving correctness without the need for such a modification. | en_US |
dc.format.extent | 364 - 383 | - |
dc.format.extent | 364 - 383 | - |
dc.language.iso | en | en_US |
dc.publisher | Springer International Publishing | en_US |
dc.subject | Linearizability | en_US |
dc.subject | Concurrent algorithms | en_US |
dc.subject | Weak memory model | en_US |
dc.subject | Total Store Order memory model | en_US |
dc.title | Admit your weakness: Verifying correctness on TSO architectures | en_US |
dc.type | Article | en_US |
dc.identifier.doi | http://dx.doi.org/10.1007/978-3-319-15317-9_22 | - |
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 | 8997 | - |
pubs.volume | 8997 | - |
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 Computer Science Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 291.06 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.