{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,11]],"date-time":"2026-09-11T04:30:05Z","timestamp":1789101005470,"version":"build-2803163510"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2008,12,20]],"date-time":"2008-12-20T00:00:00Z","timestamp":1229731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGARCH Comput. Archit. News"],"published-print":{"date-parts":[[2008,12,20]]},"abstract":"<jats:p>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 algorithmsWe 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.<\/jats:p>","DOI":"10.1145\/1556444.1556453","type":"journal-article","created":{"date-parts":[[2009,6,24]],"date-time":"2009-06-24T16:47:07Z","timestamp":1245862027000},"page":"65-71","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["State-space exploration for concurrent algorithms under weak memory orderings"],"prefix":"10.1145","volume":"36","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[{"name":"Uppsala University, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,6,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_1_2_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Conf. on Computer Aided Verification","author":"Bouajjani A.","year":"2000"},{"key":"e_1_2_1_3_1","volume-title":"Univ. of Pennsylvania","author":"Burckhardt S.","year":"2007"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735832"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007945"},{"key":"e_1_2_1_8_1","volume-title":"Proc. TAP 2008, 2nd Int. Conf. Tests and Proofs","volume":"4966","author":"Ferrara P."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.12.001"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271800"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996848"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.752664"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375584"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2004.12.005"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095408.1095421"}],"container-title":["ACM SIGARCH Computer Architecture News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1556444.1556453","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1556444.1556453","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:38:46Z","timestamp":1750253926000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1556444.1556453"}},"subtitle":["(preliminary version)"],"short-title":[],"issued":{"date-parts":[[2008,12,20]]},"references-count":18,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2008,12,20]]}},"alternative-id":["10.1145\/1556444.1556453"],"URL":"https:\/\/doi.org\/10.1145\/1556444.1556453","relation":{},"ISSN":["0163-5964"],"issn-type":[{"value":"0163-5964","type":"print"}],"subject":[],"published":{"date-parts":[[2008,12,20]]},"assertion":[{"value":"2009-06-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}