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

Direct link
State-space exploration for concurrent algorithms under weak memory orderings
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2008 (English)In: SIGARCH Computer Architecture News, ISSN 0163-5964, E-ISSN 0163-5694, Vol. 36, no 5, 65-71 p.Article in journal (Refereed) Published
Abstract [en]

Several concurrent implementations of familiar data abstractions such as queues, sets, or maps typically do not follow locking disciplines, and often use lock-free synchronization to gain performance. Since such algorithms are exposed to a weak memory model, they are notoriously hard  to get correct, as witnessed by many bugs found in published algorithms We outline a technique for analyzing correctness of concurrent algorithms under weak memory models, in which a model checker is used to search for correctness violations. The algorithm to be analyzed is transformed into a form where statements may be reordered according to a particular weak memory ordering. The transformed algorithm can then be analyzed by a model-checking tool, e.g., by enumerative state exploration. We illustrate the approach on a small example of a queue, which allows an enqueue operation to be concurrent with a dequeue operation, which we analyze with respect to the RMO memory model defined in SPARC v9.

Place, publisher, year, edition, pages
2008. Vol. 36, no 5, 65-71 p.
Keyword [en]
Concurrent programs, formal verification, weak memory models
URN: urn:nbn:se:uu:diva-112802DOI: 10.1145/1556444.1556453OAI: oai:DiVA.org:uu-112802DiVA: diva2:288073
automated verification of highly concurrent algorithmsUPMARC
Swedish Research Council
Available from: 2010-01-20 Created: 2010-01-20 Last updated: 2011-01-21Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Jonsson, Bengt
By organisation
Computer Systems
In the same journal
SIGARCH Computer Architecture News

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 224 hits
ReferencesLink to record
Permanent link

Direct link