{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T01:20:44Z","timestamp":1776993644937,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":90,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,4,17]],"date-time":"2021-04-17T00:00:00Z","timestamp":1618617600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,4,19]]},"DOI":"10.1145\/3445814.3446748","type":"proceedings-article","created":{"date-parts":[[2021,4,11]],"date-time":"2021-04-11T17:06:26Z","timestamp":1618160786000},"page":"530-545","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["VSync: push-button verification and optimization for synchronization primitives on weak memory models"],"prefix":"10.1145","author":[{"given":"Jonas","family":"Oberhauser","sequence":"first","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Rafael Lourenco de Lima","family":"Chehab","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Diogo","family":"Behrens","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Ming","family":"Fu","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Antonio","family":"Paolillo","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Lilith","family":"Oberhauser","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Koustubha","family":"Bhat","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"given":"Yuzhong","family":"Wen","sequence":"additional","affiliation":[{"name":"Huawei, China"}]},{"given":"Haibo","family":"Chen","sequence":"additional","affiliation":[{"name":"Huawei, China \/ Shanghai Jiao Tong University, China"}]},{"given":"Jaeho","family":"Kim","sequence":"additional","affiliation":[{"name":"Huawei, Germany \/ Huawei, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"1999. spin_unlock optimization(i386). https:\/\/marc.info\/?l=linux-kernel&m= 94318921016232&w=2.  1999. spin_unlock optimization(i386). https:\/\/marc.info\/?l=linux-kernel&m= 94318921016232&w=2."},{"key":"e_1_3_2_1_2_1","unstructured":"2008. Linux Ticketlock. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=314cdbefd1fd0a7acf3780e9628465b77ea6a836.  2008. Linux Ticketlock. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=314cdbefd1fd0a7acf3780e9628465b77ea6a836."},{"key":"e_1_3_2_1_3_1","unstructured":"2018. Linux-Kernel Memory Model. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/ docs\/papers\/2018\/p0124r6.html.  2018. Linux-Kernel Memory Model. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/ docs\/papers\/2018\/p0124r6.html."},{"key":"e_1_3_2_1_4_1","unstructured":"2020. Await termination violation bug fix in DPDK. http:\/\/patches.dpdk.org\/ patch\/75983\/.  2020. Await termination violation bug fix in DPDK. http:\/\/patches.dpdk.org\/ patch\/75983\/."},{"key":"e_1_3_2_1_5_1","unstructured":"2020. CetiKOS MCS lock implementation-source code. https:\/\/certikos.github. io\/certikos-artifact\/html\/mcertikos.mcslock. MMCSLockAbsIntroCSource.html.  2020. CetiKOS MCS lock implementation-source code. https:\/\/certikos.github. io\/certikos-artifact\/html\/mcertikos.mcslock. MMCSLockAbsIntroCSource.html."},{"key":"e_1_3_2_1_6_1","unstructured":"2020. Clang: C Language Family Frontend for LLVM. https:\/\/clang.org.  2020. Clang: C Language Family Frontend for LLVM. https:\/\/clang.org."},{"key":"e_1_3_2_1_7_1","unstructured":"2020. musl libc: an implementation of the C standard library. https:\/\/musl.libc.org.  2020. musl libc: an implementation of the C standard library. https:\/\/musl.libc.org."},{"key":"e_1_3_2_1_8_1","unstructured":"2020. Mutual exclusion bug fix in seL4. https:\/\/github.com\/seL4\/seL4\/pull\/199\/ commits.  2020. Mutual exclusion bug fix in seL4. https:\/\/github.com\/seL4\/seL4\/pull\/199\/ commits."},{"key":"e_1_3_2_1_9_1","unstructured":"2020. openEuler. https:\/\/openeuler.org.  2020. openEuler. https:\/\/openeuler.org."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0275-0"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_4"},{"key":"e_1_3_2_1_13_1","volume-title":"Bengt Jonsson, and Carl Leonardsson.","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Bengt Jonsson, and Carl Leonardsson. 2016 . Stateless model checking for POWER. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing , Cham, 134-156. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless model checking for POWER. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 134-156."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_1_16_1","volume-title":"Concurrency kit. Retrieved November 8 ( 2015 )","author":"Bahra Samy Al","year":"2018","unstructured":"Samy Al Bahra . 2015. Concurrency kit. Retrieved November 8 ( 2015 ) , 2018 . https:\/\/github.com\/concurrencykit\/ck. Samy Al Bahra. 2015. Concurrency kit. Retrieved November 8 ( 2015 ), 2018. https:\/\/github.com\/concurrencykit\/ck."},{"key":"e_1_3_2_1_17_1","volume-title":"Don't Sit on the Fence","author":"Alglave Jade","unstructured":"Jade Alglave , Daniel Kroening , Vincent Nimal , and Daniel Poetzl . 2014. Don't Sit on the Fence . In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing , Cham , 508-524. Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. 2014. Don't Sit on the Fence. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 508-524."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13218-010-0005-7"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_21_1","unstructured":"Sebastian Burckhardt. 2007. Memory model sensitive analysis of concurrent data types. Dissertations available from ProQuest (01 2007 ).  Sebastian Burckhardt. 2007. Memory model sensitive analysis of concurrent data types. Dissertations available from ProQuest (01 2007 )."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854051"},{"key":"e_1_3_2_1_24_1","unstructured":"Ernie Cohen and Norbert Schirmer. 2009. A Better Reduction Theorem for Store Bufers. CoRR abs\/0909.4637 ( 2009 ). arXiv: 0909.4637 http:\/\/arxiv.org\/abs\/0909. 4637  Ernie Cohen and Norbert Schirmer. 2009. A Better Reduction Theorem for Store Bufers. CoRR abs\/0909.4637 ( 2009 ). arXiv: 0909.4637 http:\/\/arxiv.org\/abs\/0909. 4637"},{"key":"e_1_3_2_1_25_1","unstructured":"Jonathan Corbet. 2014. locks and qspinlocks. https:\/\/lwn.net\/Articles\/590243\/.  Jonathan Corbet. 2014. locks and qspinlocks. https:\/\/lwn.net\/Articles\/590243\/."},{"key":"e_1_3_2_1_26_1","unstructured":"Will Deacon. Feb 13 2018. locking\/qspinlock: Ensure node is initialized before updating prev->next. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=95bcade33a8a.  Will Deacon. Feb 13 2018. locking\/qspinlock: Ensure node is initialized before updating prev->next. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=95bcade33a8a."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29400-7_24"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2612669.2612696"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2686884"},{"key":"e_1_3_2_1_31_1","volume-title":"Futexes are tricky. Futexes are Tricky","author":"Drepper Ulrich","year":"2005","unstructured":"Ulrich Drepper . 2005. Futexes are tricky. Futexes are Tricky , Red Hat Inc , Japan 4 ( 2005 ). Ulrich Drepper. 2005. Futexes are tricky. Futexes are Tricky, Red Hat Inc, Japan 4 ( 2005 )."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/782814.782854"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.47"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_1_36_1","unstructured":"Linux Foundation. 2015. Data Plane Development Kit (DPDK). http:\/\/www. dpdk.org  Linux Foundation. 2015. Data Plane Development Kit (DPDK). http:\/\/www. dpdk.org"},{"key":"e_1_3_2_1_37_1","volume-title":"BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In International Conference on Computer Aided Verification. Springer, 355-365","author":"Gavrilenko Natalia","year":"2019","unstructured":"Natalia Gavrilenko , Hern\u00e1n Ponce- de Le\u00f3n , Florian Furbach , Keijo Heljanko , and Roland Meyer . 2019 . BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In International Conference on Computer Aided Verification. Springer, 355-365 . Natalia Gavrilenko, Hern\u00e1n Ponce-de Le\u00f3n, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2019. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In International Conference on Computer Aided Verification. Springer, 355-365."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) ( OSDI'16). USENIX Association, USA, 653-669","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) ( OSDI'16). USENIX Association, USA, 653-669 . Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) ( OSDI'16). USENIX Association, USA, 653-669."},{"key":"e_1_3_2_1_40_1","unstructured":"Maurice Herlihy and Nir Shavit. 2011. The art of multiprocessor programming. Morgan Kaufmann.  Maurice Herlihy and Nir Shavit. 2011. The art of multiprocessor programming. Morgan Kaufmann."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Mark A Hillebrand and Dirk C Leinenbach. 2009. Formal verification of a readerwriter lock implementation in C. Electronic Notes in Theoretical Computer Science 254 ( 2009 ) 123-141.  Mark A Hillebrand and Dirk C Leinenbach. 2009. Formal verification of a readerwriter lock implementation in C. Electronic Notes in Theoretical Computer Science 254 ( 2009 ) 123-141.","DOI":"10.1016\/j.entcs.2009.09.063"},{"key":"e_1_3_2_1_42_1","volume-title":"Design and validation of computer protocols","author":"Holzmann Gerard J","unstructured":"Gerard J Holzmann and William Slattery Lieberman . 1991. Design and validation of computer protocols . Vol. 512 . Prentice hall Englewood Clifs . Gerard J Holzmann and William Slattery Lieberman. 1991. Design and validation of computer protocols. Vol. 512. Prentice hall Englewood Clifs."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2891042"},{"key":"e_1_3_2_1_44_1","unstructured":"Huawei. 2019. Huawei Unveils Industry's Highest-Performance ARM-based CPU. https:\/\/www.huawei.com\/en\/news\/2019\/1\/huawei-unveils-highestperformance-arm-based-cpu.  Huawei. 2019. Huawei Unveils Industry's Highest-Performance ARM-based CPU. https:\/\/www.huawei.com\/en\/news\/2019\/1\/huawei-unveils-highestperformance-arm-based-cpu."},{"key":"e_1_3_2_1_45_1","unstructured":"ISO\/IEC. 2011. Committee Draft N1570 of C11 standard.  ISO\/IEC. 2011. Committee Draft N1570 of C11 standard."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1556444.1556453"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359629"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360599"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092287"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2261417.2261438"},{"key":"e_1_3_2_1_58_1","volume-title":"Kyoto Cabinet: A straightforward implementation of DBM","author":"Labs FAL","year":"2011","unstructured":"FAL Labs . 2011 . Kyoto Cabinet: A straightforward implementation of DBM . http:\/\/fallabs.com\/kyotocabinet. FAL Labs. 2011. Kyoto Cabinet: A straightforward implementation of DBM. http:\/\/fallabs.com\/kyotocabinet."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_1_60_1","first-page":"134","volume-title":"International journal on software tools for technology transfer 1, 1-2 ( 1997 )","author":"Larsen Kim G","unstructured":"Kim G Larsen , Paul Pettersson , and Wang Yi. 1997. UPPAAL in a nutshell . International journal on software tools for technology transfer 1, 1-2 ( 1997 ) , 134 - 152 . Kim G Larsen, Paul Pettersson, and Wang Yi. 1997. UPPAAL in a nutshell. International journal on software tools for technology transfer 1, 1-2 ( 1997 ), 134-152."},{"key":"e_1_3_2_1_61_1","volume-title":"Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C. In International Conference on Computer Aided Verification. Springer, 387-397","author":"Lau Stella","year":"2019","unstructured":"Stella Lau , Victor BF Gomes , Kayvan Memarian , Jean Pichon-Pharabod , and Peter Sewell . 2019 . Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C. In International Conference on Computer Aided Verification. Springer, 387-397 . Stella Lau, Victor BF Gomes, Kayvan Memarian, Jean Pichon-Pharabod, and Peter Sewell. 2019. Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C. In International Conference on Computer Aided Verification. Springer, 387-397."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374535"},{"key":"e_1_3_2_1_63_1","unstructured":"Waiman Long. Nov 10 2015. locking\/qspinlock: Use_acquire\/_release() versions of cmpxchg() & xchg(). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=64d816cba06c.  Waiman Long. Nov 10 2015. locking\/qspinlock: Use_acquire\/_release() versions of cmpxchg() & xchg(). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=64d816cba06c."},{"key":"e_1_3_2_1_64_1","unstructured":"Waiman Long and Peter Zijlstra. 2015. qspinlock code at version 4.4 of Linux Kernel. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/tree\/ kernel\/locking\/qspinlock.c?h=v4. 4.  Waiman Long and Peter Zijlstra. 2015. qspinlock code at version 4.4 of Linux Kernel. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/tree\/ kernel\/locking\/qspinlock.c?h=v4. 4."},{"key":"e_1_3_2_1_65_1","unstructured":"Waiman Long and Peter Zijlstra. 2020. qspinlock code at version 5.6 of Linux Kernel. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/tree\/ kernel\/locking\/qspinlock.c?h=v5. 6.  Waiman Long and Peter Zijlstra. 2020. qspinlock code at version 5.6 of Linux Kernel. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/tree\/ kernel\/locking\/qspinlock.c?h=v5. 6."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823285_84"},{"key":"e_1_3_2_1_68_1","volume-title":"An Axiomatic Memory Model for POWER Multiprocessors","author":"Mador-Haim Sela","unstructured":"Sela Mador-Haim , Luc Maranget , Susmit Sarkar , Kayvan Memarian , Jade Alglave , Scott Owens , Rajeev Alur , Milo M. K. Martin , Peter Sewell , and Derek Williams . 2012. An Axiomatic Memory Model for POWER Multiprocessors . In Computer Aided Verification, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 495-512. Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An Axiomatic Memory Model for POWER Multiprocessors. In Computer Aided Verification, P. Madhusudan and Sanjit A. Seshia (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 495-512."},{"key":"e_1_3_2_1_69_1","volume-title":"Symbolic Model Checking","author":"McMillan Kenneth L","unstructured":"Kenneth L McMillan . 1993. Symbolic model checking . In Symbolic Model Checking . Springer , 25-60. Kenneth L McMillan. 1993. Symbolic model checking. In Symbolic Model Checking. Springer, 25-60."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375625"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2806886"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29613-5_9"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43065-2"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2797022.2797042"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_1_83_1","volume-title":"The SPARC architecture manual (version 9)","author":"SPARC International Inc. 1994.","unstructured":"SPARC International Inc. 1994. The SPARC architecture manual (version 9) . Prentice-Hall . SPARC International Inc. 1994. The SPARC architecture manual (version 9). Prentice-Hall."},{"key":"e_1_3_2_1_84_1","unstructured":"Georgia Tech SS Lab. 2010. NUMA-aware Reader-Writer Implementation. https:\/\/github.com\/sslab-gatech\/shfllock\/blob\/master\/benchmarks\/kernelsyncstress\/locks\/cmcsmcsrw.c#L222.  Georgia Tech SS Lab. 2010. NUMA-aware Reader-Writer Implementation. https:\/\/github.com\/sslab-gatech\/shfllock\/blob\/master\/benchmarks\/kernelsyncstress\/locks\/cmcsmcsrw.c#L222."},{"key":"e_1_3_2_1_85_1","unstructured":"The Guardian. 2020. Apple ditches Intel for ARM processors in Mac computers with Big Sur. https:\/\/www.theguardian.com\/technology\/2020\/jun\/22\/appleditches-intel-for-arm-processors-in-big-sur-computers.  The Guardian. 2020. Apple ditches Intel for ARM processors in Mac computers with Big Sur. https:\/\/www.theguardian.com\/technology\/2020\/jun\/22\/appleditches-intel-for-arm-processors-in-big-sur-computers."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_2"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_1_88_1","volume-title":"Verifying Fence Elimination Optimisations","author":"Vafeiadis Viktor","unstructured":"Viktor Vafeiadis and Francesco Zappa Nardelli . 2011. Verifying Fence Elimination Optimisations . In Static Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 146-162. Viktor Vafeiadis and Francesco Zappa Nardelli. 2011. Verifying Fence Elimination Optimisations. In Static Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 146-162."},{"key":"e_1_3_2_1_89_1","unstructured":"Andrew Waterman and Krste Asanovi? (Eds.). 2019. The RISC-V Instruction Set Manual. https:\/\/content.riscv.org\/wp-content\/uploads\/2019\/06\/riscv-spec.pdf. Accessed: 2020-03-06.  Andrew Waterman and Krste Asanovi? (Eds.). 2019. The RISC-V Instruction Set Manual. https:\/\/content.riscv.org\/wp-content\/uploads\/2019\/06\/riscv-spec.pdf. Accessed: 2020-03-06."},{"key":"e_1_3_2_1_90_1","unstructured":"Pan Xinhui. Jun 3 2016. locking\/qspinlock: Use atomic_sub_return_release() in queued_spin_unlock(). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=ca50e426f96c.  Pan Xinhui. Jun 3 2016. locking\/qspinlock: Use atomic_sub_return_release() in queued_spin_unlock(). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/ linux.git\/commit\/?id=ca50e426f96c."},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Virtual USA","acronym":"ASPLOS '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3445814.3446748","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3445814.3446748","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:14Z","timestamp":1750195694000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3445814.3446748"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,17]]},"references-count":90,"alternative-id":["10.1145\/3445814.3446748","10.1145\/3445814"],"URL":"https:\/\/doi.org\/10.1145\/3445814.3446748","relation":{},"subject":[],"published":{"date-parts":[[2021,4,17]]},"assertion":[{"value":"2021-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}