A sound and complete definition of linearizability on weak memory models.
Linearizability is the standard correctness notion for concurrent objects, i.e., objects designed to be accessed simultaneously by multiple threads. In this paper, we explain why the original definition of linearizability is not applicable to code running on the weak memory models supported by modern multicore architectures, and provide an alternative definition which is applicable. In contrast to earlier work, our definition is proved to be both sound and complete. Furthermore, while earlier work has focussed on linearizability for the TSO (Total Store Order) architecture, ours is applicable to any existing weak memory model. We illustrate how it can be used to prove the correctness of a simple case study on the widely used TSO, Power and ARM architectures.
Publisher URL: http://arxiv.org/abs/1802.04954
DOI: arXiv:1802.04954v1
Keeping up-to-date with research can feel impossible, with papers being published faster than you'll ever be able to read them. That's where Researcher comes in: we're simplifying discovery and making important discussions happen. With over 19,000 sources, including peer-reviewed journals, preprints, blogs, universities, podcasts and Live events across 10 research areas, you'll never miss what's important to you. It's like social media, but better. Oh, and we should mention - it's free.
Researcher displays publicly available abstracts and doesn’t host any full article content. If the content is open access, we will direct clicks from the abstracts to the publisher website and display the PDF copy on our platform. Clicks to view the full text will be directed to the publisher website, where only users with subscriptions or access through their institution are able to view the full article.