{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T18:11:11Z","timestamp":1758823871379,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T00:00:00Z","timestamp":1374537600000},"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":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2013,7,23]]},"abstract":"<jats:p>Modeling parallel algorithms at the architecture level enables exploring side-effects of the weakly ordered nature of modern processors. Formal verification of such models with model-checking can ensure that algorithm guarantees will hold even in the presence of the most aggressive compiler and processor optimizations.<\/jats:p>\n          <jats:p>This paper proposes a virtual architecture to model the effects of such optimizations. It first presents the OoOmem framework to model out-of-order memory accesses. It then presents the OoOisched framework to model the effects of out-of-order instruction scheduling.<\/jats:p>\n          <jats:p>These two frameworks are explained and tested using weaklyordered memory interaction scenarios known to be affected by weak ordering. Then, modeling of user-level RCU (Read- Copy Update) synchronization algorithms is presented. It uses the virtual architecture proposed to verify that the RCU guarantees are indeed respected.<\/jats:p>","DOI":"10.1145\/2506164.2506174","type":"journal-article","created":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T19:12:41Z","timestamp":1374779561000},"page":"51-65","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Multi-core systems modeling for formal verification of parallel algorithms"],"prefix":"10.1145","volume":"47","author":[{"given":"Mathieu","family":"Desnoyers","sequence":"first","affiliation":[{"name":"EfficiOS Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul E.","family":"McKenney","sequence":"additional","affiliation":[{"name":"IBM Linux Technnoology Center"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel R.","family":"Dagenais","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique, Montreal"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,7,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Berard B. Bidoit M. Finkel A. Laroussinie F. Petit A. Petrucci L. and Schnoebelen P. 2001. Systems and Software Verification Model-Checking Techniques and Tools. Springer-Verlag New York NY USA.   Berard B. Bidoit M. Finkel A. Laroussinie F. Petit A. Petrucci L. and Schnoebelen P. 2001. Systems and Software Verification Model-Checking Techniques and Tools. Springer-Verlag New York NY USA.","DOI":"10.1007\/978-3-662-04558-9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_2_1_8_1","unstructured":"Fu C.-Y. Jennings M. D. Larin S. Y. and Conte T. M. 1998a. Software-only value speculation scheduling. Tech. rep. Department of Electric & Computer Engineering North Carolina State University Raleigh NC.  Fu C.-Y. Jennings M. D. Larin S. Y. and Conte T. M. 1998a. Software-only value speculation scheduling. Tech. rep. Department of Electric & Computer Engineering North Carolina State University Raleigh NC."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/384265.291058"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","key":"e_1_2_1_11_1","unstructured":"Holzmann , G. J. 2003. The Spin Model Checker: Primer and Reference Manual . Addison-Wesley , Boston, MA, USA . Holzmann, G. J. 2003. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Boston, MA, USA."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/28641.28650"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.755465"},{"key":"e_1_2_1_14_1","first-page":"137","article-title":"Memory ordering in modern microprocessors, part II","volume":"1","author":"McKenney P. E.","year":"2005","unstructured":"McKenney , P. E. 2005 . Memory ordering in modern microprocessors, part II . Linux Journal 1 , 137 (September), 78--82. Available: http:\/\/www.linuxjournal.com\/article\/8212 {Viewed June 3, 2009}. McKenney, P. E. 2005. Memory ordering in modern microprocessors, part II. Linux Journal 1, 137 (September), 78--82. Available: http:\/\/www.linuxjournal.com\/article\/8212 {Viewed June 3, 2009}.","journal-title":"Linux Journal"},{"key":"e_1_2_1_15_1","unstructured":"McKenney P. E. 2007a. C++ data-dependency ordering: Atomics. http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2359.html.  McKenney P. E. 2007a. C++ data-dependency ordering: Atomics. http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2359.html."},{"key":"e_1_2_1_16_1","unstructured":"McKenney P. E. 2007b. C++ data-dependency ordering: Function annotation. http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2361.html.  McKenney P. E. 2007b. C++ data-dependency ordering: Function annotation. http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2361.html."},{"key":"e_1_2_1_17_1","unstructured":"McKenney P. E. 2007c. C++ data-dependency ordering: Memory model. http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2360.html.  McKenney P. E. 2007c. C++ data-dependency ordering: Memory model. http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2360.html."},{"key":"e_1_2_1_18_1","unstructured":"McKenney P. E. 2007d. Using Promela and Spin to verify parallel algorithms. Linux Weekly News Available: http:\/\/lwn.net\/Articles\/243851\/.  McKenney P. E. 2007d. Using Promela and Spin to verify parallel algorithms. Linux Weekly News Available: http:\/\/lwn.net\/Articles\/243851\/."},{"key":"e_1_2_1_19_1","unstructured":"McKenney P. E. and Rostedt S. 2008. Integrating and validating dynticks and preemptable RCU. Available: http:\/\/lwn.net\/Articles\/279077\/ {Viewed April 24 2008}.  McKenney P. E. and Rostedt S. 2008. Integrating and validating dynticks and preemptable RCU. Available: http:\/\/lwn.net\/Articles\/279077\/ {Viewed April 24 2008}."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.752664"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121262"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"volume-title":"Handbook of theoretical computer science (vol. B): formal models and semantics","author":"van Leeuwen J.","key":"e_1_2_1_25_1","unstructured":"van Leeuwen , J. 1990. Handbook of theoretical computer science (vol. B): formal models and semantics . MIT Press , Cambridge, MA, USA . van Leeuwen, J. 1990. Handbook of theoretical computer science (vol. B): formal models and semantics. MIT Press, Cambridge, MA, USA."}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2506164.2506174","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2506164.2506174","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:43Z","timestamp":1750231723000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2506164.2506174"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,23]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,7,23]]}},"alternative-id":["10.1145\/2506164.2506174"],"URL":"https:\/\/doi.org\/10.1145\/2506164.2506174","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2013,7,23]]},"assertion":[{"value":"2013-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}