uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Automated Verification of Linearization Policies
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Verification Group)
2016 (English)In: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, 2016Conference paper, Published paper (Other academic)
Abstract [en]

We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.

Place, publisher, year, edition, pages
2016.
National Category
Computer Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-305226DOI: 10.1007/978-3-662-53413-7_4ISI: 000388924600004ISBN: 9783662534120 (print)ISBN: 9783662534137 (print)OAI: oai:DiVA.org:uu-305226DiVA: diva2:1034785
Conference
23rd International Symposium, SAS 2016
Available from: 2016-10-13 Created: 2016-10-13 Last updated: 2017-01-02Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Abdulla, ParoshJonsson, BengtTrinh, Cong Quy

Search in DiVA

By author/editor
Abdulla, ParoshJonsson, BengtTrinh, Cong Quy
By organisation
Computer Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 473 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf