State-space exploration for concurrent algorithms under weak memory orderings
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
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.
Concurrent programs, formal verification, weak memory models
IdentifiersURN: urn:nbn:se:uu:diva-112802DOI: 10.1145/1556444.1556453OAI: oai:DiVA.org:uu-112802DiVA: diva2:288073
Projectsautomated verification of highly concurrent algorithmsUPMARC
FunderSwedish Research Council