{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:34:58Z","timestamp":1791459298520,"version":"4.3.4"},"reference-count":89,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>The goal of this work is to improve the efficiency of bounded model checkers that are modular in the memory model.  \nOur first contribution is a static analysis for the given memory model that is performed as a preprocessing step and helps us significantly reduce the encoding size.  \nMemory model make use of relations to judge whether an execution is consistent. The analysis computes bounds on these relations: which pairs of events may or must be related.  \nWhat is new is that the bounds are relativized to the execution of events.  \nThis makes it possible to derive, for the first time, not only upper but also meaningful lower bounds.  \nAnother important feature is that the analysis can import information about the verification instance from external sources to improve its precision.  \nOur second contribution are new optimizations for the SMT encoding.  \nNotably, the lower bounds allow us to simplify the encoding of acyclicity constraints.  \nWe implemented our analysis and optimizations within a bounded model checker and evaluated it on challenging benchmarks.  \nThe evaluation shows up-to 40% reduction in verification time (including the analysis) over previous encodings.  \nOur optimizations allow us to efficiently check safety, liveness, and data race freedom in Linux kernel code.<\/jats:p>","DOI":"10.1145\/3622855","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1618-1647","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Static Analysis of Memory Models for SMT Encodings"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-8552","authenticated-orcid":false,"given":"Thomas","family":"Haas","sequence":"first","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3608-2584","authenticated-orcid":false,"given":"Ren\u00e9","family":"Maseli","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8830","authenticated-orcid":false,"given":"Hern\u00e1n","family":"Ponce de Le\u00f3n","sequence":"additional","affiliation":[{"name":"Huawei Dresden Research Center, Dresden, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2023. C11: Bad Locking and Races. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/c11_orig.cat#L17-L20 Accessed: 08\/12\/2023 \t\t\t\t  2023. C11: Bad Locking and Races. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/c11_orig.cat#L17-L20 Accessed: 08\/12\/2023"},{"key":"e_1_2_2_2_1","unstructured":"2023. KCSAN.  https:\/\/www.kernel.org\/doc\/html\/latest\/dev-tools\/kcsan.html \t\t\t\t  2023. KCSAN.  https:\/\/www.kernel.org\/doc\/html\/latest\/dev-tools\/kcsan.html"},{"key":"e_1_2_2_3_1","unstructured":"2023. Linux Memory Model: Locks. https:\/\/github.com\/torvalds\/linux\/blob\/master\/tools\/memory-model\/lock.cat#L39-L58 Accessed: 08\/12\/2023 \t\t\t\t  2023. Linux Memory Model: Locks. https:\/\/github.com\/torvalds\/linux\/blob\/master\/tools\/memory-model\/lock.cat#L39-L58 Accessed: 08\/12\/2023"},{"key":"e_1_2_2_4_1","unstructured":"2023. Linux Memory Model: RCU. https:\/\/github.com\/torvalds\/linux\/blob\/master\/tools\/memory-model\/linux-kernel.bell#L56-L73 Accessed: 08\/12\/2023 \t\t\t\t  2023. Linux Memory Model: RCU. https:\/\/github.com\/torvalds\/linux\/blob\/master\/tools\/memory-model\/linux-kernel.bell#L56-L73 Accessed: 08\/12\/2023"},{"key":"e_1_2_2_5_1","unstructured":"2023. Linux Memory Model: Sanitization. https:\/\/lkml.org\/lkml\/2023\/1\/18\/575 Accessed: 08\/12\/2023 \t\t\t\t  2023. Linux Memory Model: Sanitization. https:\/\/lkml.org\/lkml\/2023\/1\/18\/575 Accessed: 08\/12\/2023"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67087-0_4"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_1"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.1990.134502"},{"key":"e_1_2_2_11_1","unstructured":"Jade Alglave. 2010. A Shared Memory Poetics. L\u2019universit\u00e9 Paris Denis Diderot. \t\t\t\t  Jade Alglave. 2010. A Shared Memory Poetics. L\u2019universit\u00e9 Paris Denis Diderot."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009883"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994593"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_9"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/6012.15399"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3579849"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360568"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393664"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_45"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.43410"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_2_31_1","unstructured":"Jonathan Corbet. 2008. Ticket spinlocks.  https:\/\/lwn.net\/Articles\/267968\/ \t\t\t\t  Jonathan Corbet. 2008. Ticket spinlocks.  https:\/\/lwn.net\/Articles\/267968\/"},{"key":"e_1_2_2_32_1","unstructured":"Jonathan Corbet. 2013. C11 atomic variables and the kernel.  https:\/\/lwn.net\/Articles\/586838\/ \t\t\t\t  Jonathan Corbet. 2013. C11 atomic variables and the kernel.  https:\/\/lwn.net\/Articles\/586838\/"},{"key":"e_1_2_2_33_1","unstructured":"Jonathan Corbet. 2013. Improving ticket spinlocks.  https:\/\/lwn.net\/Articles\/531254\/ \t\t\t\t  Jonathan Corbet. 2013. Improving ticket spinlocks.  https:\/\/lwn.net\/Articles\/531254\/"},{"key":"e_1_2_2_34_1","unstructured":"Jonathan Corbet. 2014. MCS locks and qspinlocks.  https:\/\/lwn.net\/Articles\/590243\/ \t\t\t\t  Jonathan Corbet. 2014. MCS locks and qspinlocks.  https:\/\/lwn.net\/Articles\/590243\/"},{"key":"e_1_2_2_35_1","volume-title":"Principles of abstract interpretation","author":"Cousot P.","unstructured":"P. Cousot . 2021. Principles of abstract interpretation . MIT Press . P. Cousot. 2021. Principles of abstract interpretation. MIT Press."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_25"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814297"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3545117"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625970"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11558-0_10"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428214"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8313104"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563292"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44880-2_1"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_11"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571212"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519270.3538445"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993521"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505273"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485475"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446711"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040336"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30923-7_9"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115686"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2806886"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_2_2_73_1","volume-title":"Thomas Haas, Diogo Behrens, Rafael Lourenco de Lima Chehab, Ming Fu, and Roland Meyer.","author":"Paolillo Antonio","year":"2021","unstructured":"Antonio Paolillo , Hern\u00e1n Ponce de Le\u00f3n , Thomas Haas, Diogo Behrens, Rafael Lourenco de Lima Chehab, Ming Fu, and Roland Meyer. 2021 . Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. CoRR , abs\/2111.15240 (2021), arXiv:2111.15240. arxiv:2111.15240 Antonio Paolillo, Hern\u00e1n Ponce de Le\u00f3n, Thomas Haas, Diogo Behrens, Rafael Lourenco de Lima Chehab, Ming Fu, and Roland Meyer. 2021. Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. CoRR, abs\/2111.15240 (2021), arXiv:2111.15240. arxiv:2111.15240"},{"key":"e_1_2_2_74_1","volume-title":"SAS (LNCS","volume":"320","author":"de Le\u00f3n Hern\u00e1n Ponce","year":"2017","unstructured":"Hern\u00e1n Ponce de Le\u00f3n , Florian Furbach , Keijo Heljanko , and Roland Meyer . 2017 . Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models . In SAS (LNCS , Vol. 10422). Springer, 299\u2013 320 . Hern\u00e1n Ponce de Le\u00f3n, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2017. Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. In SAS (LNCS, Vol. 10422). Springer, 299\u2013320."},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i5.20530"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_2_80_1","unstructured":"Jaroslav Sevcik and Peter Sewell. 2011. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/ pes20\/cpp\/cpp0xmappings.html Accessed: 04\/07\/2023 \t\t\t\t  Jaroslav Sevcik and Peter Sewell. 2011. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/ pes20\/cpp\/cpp0xmappings.html Accessed: 04\/07\/2023"},{"key":"e_1_2_2_81_1","unstructured":"Alan Stern. 2023. tools: memory-model: Add rmw-sequences to the LKMM.  https:\/\/lkml.org\/lkml\/2022\/11\/16\/1555 \t\t\t\t  Alan Stern. 2023. tools: memory-model: Add rmw-sequences to the LKMM.  https:\/\/lkml.org\/lkml\/2022\/11\/16\/1555"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563321"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1971.10"},{"key":"e_1_2_2_84_1","volume-title":"A constraint solver for software engineering: finding models and cores of large relational specifications. Ph. D. Dissertation","author":"Torlak Emina","unstructured":"Emina Torlak . 2009. A constraint solver for software engineering: finding models and cores of large relational specifications. Ph. D. Dissertation . Massachusetts Institute of Technology , Cambridge, MA, USA . https:\/\/hdl.handle.net\/1721.1\/46789 Emina Torlak. 2009. A constraint solver for software engineering: finding models and cores of large relational specifications. Ph. D. Dissertation. Massachusetts Institute of Technology, Cambridge, MA, USA. https:\/\/hdl.handle.net\/1721.1\/46789"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806635"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_2_87_1","volume-title":"BBQ: A Block-based Bounded Queue for Exchanging Data and Profiling","author":"Wang Jiawei","year":"2022","unstructured":"Jiawei Wang , Diogo Behrens , Ming Fu , Lilith Oberhauser , Jonas Oberhauser , Jitang Lei , Geng Chen , Hermann H\u00e4rtig , and Haibo Chen . 2022 . BBQ: A Block-based Bounded Queue for Exchanging Data and Profiling . In ATC, Jiri Schindler and Noa Zilberman (Eds.). USENIX Association , 249\u2013262. https:\/\/www.usenix.org\/conference\/atc22\/presentation\/wang-jiawei Jiawei Wang, Diogo Behrens, Ming Fu, Lilith Oberhauser, Jonas Oberhauser, Jitang Lei, Geng Chen, Hermann H\u00e4rtig, and Haibo Chen. 2022. BBQ: A Block-based Bounded Queue for Exchanging Data and Profiling. In ATC, Jiri Schindler and Noa Zilberman (Eds.). USENIX Association, 249\u2013262. https:\/\/www.usenix.org\/conference\/atc22\/presentation\/wang-jiawei"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009838"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499938"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622855","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":89,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622855"],"URL":"https:\/\/doi.org\/10.1145\/3622855","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}