Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/10313
Title: | Admit your weakness: Verifying correctness on TSO architectures |
Authors: | Smith, G Derrick, J Dongol, B |
Keywords: | Linearizability;Concurrent algorithms;Weak memory model;Total Store Order memory model |
Issue Date: | 2015 |
Publisher: | Springer International Publishing |
Citation: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8997: 364 - 383, (January 2015) |
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. |
Description: | “The final publication is available at http://link.springer.com/chapter/10.1007%2F978-3-319-15317-9_22 ”. |
URI: | http://link.springer.com/chapter/10.1007%2F978-3-319-15317-9_22 http://bura.brunel.ac.uk/handle/2438/10313 |
DOI: | http://dx.doi.org/10.1007/978-3-319-15317-9_22 |
ISBN: | 978-3-319-15316-2 |
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.