{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:14Z","timestamp":1773193514494,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"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":[[2021,1,4]]},"abstract":"<jats:p>We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.<\/jats:p>","DOI":"10.1145\/3434337","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Deciding reachability under persistent x86-TSO"],"prefix":"10.1145","volume":"5","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[{"name":"University of Paris, France"}]},{"given":"K. Narayan","family":"Kumar","sequence":"additional","affiliation":[{"name":"Chennai Mathematical Institute, India \/ CNRS UMI ReLaX, India"}]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[{"name":"Institute of Mathematical Sciences, India"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"353","article-title":"Stateless Model Checking for TSO and PSO. In TACAS (LNCS, Vol. 9035 )","author":"Abdulla P.A.","year":"2015","unstructured":"P.A. Abdulla , S. Aronis , M. Faouzi Atig , B. Jonsson , C. Leonardsson , and K. Sagonas . 2015 . Stateless Model Checking for TSO and PSO. In TACAS (LNCS, Vol. 9035 ) . Springer , 353 - 367 . P.A. Abdulla, S. Aronis, M. Faouzi Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. 2015. Stateless Model Checking for TSO and PSO. In TACAS (LNCS, Vol. 9035 ). Springer, 353-367.","journal-title":"Springer"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0275-0"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_2_1_4_1","volume-title":"NETYS 2020 (Lecture Notes in Computer Science). Springer.","author":"Abdulla Parosh Aziz","year":"2020","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Ahmed Bouajjani , Egor Derevenetc , Carl Leonardsson , and Roland Meyer . 2020 . Safety Verification under Power . In NETYS 2020 (Lecture Notes in Computer Science). Springer. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, and Roland Meyer. 2020. Safety Verification under Power. In NETYS 2020 (Lecture Notes in Computer Science). Springer."},{"key":"e_1_2_1_5_1","first-page":"56","article-title":"Context-Bounded Analysis for POWER","author":"Abdulla Parosh Aziz","year":"2017","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Ahmed Bouajjani , and Tuan Phong Ngo . 2017 b. Context-Bounded Analysis for POWER . In TACAS. 56 - 74 . Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2017b. Context-Bounded Analysis for POWER. In TACAS. 56-74.","journal-title":"TACAS."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(1:9)2018"},{"key":"e_1_2_1_7_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 CAV (LNCS , Vol . 9780 ). 134-156. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless Model Checking for POWER. In CAV (LNCS, Vol. 9780 ). 134-156."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287591"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_14_1","unstructured":"ARM. 2018. ARM architecture reference manual ARMv8 for ARMv8-A architecture profile (DDI 0487D.a).  ARM. 2018. ARM architecture reference manual ARMv8 for ARMv8-A architecture profile (DDI 0487D.a)."},{"key":"e_1_2_1_15_1","volume-title":"How to Build a Non-Volatile Memory Database Management System","author":"Arulraj Joy","unstructured":"Joy Arulraj and Andrew Pavlo . 2017. How to Build a Non-Volatile Memory Database Management System . In SIGMOD, Semih Salihoglu, Wenchao Zhou, Rada Chirkova, Jun Yang, and Dan Suciu (Eds.). ACM. Joy Arulraj and Andrew Pavlo. 2017. How to Build a Non-Volatile Memory Database Management System. In SIGMOD, Semih Salihoglu, Wenchao Zhou, Rada Chirkova, Jun Yang, and Dan Suciu (Eds.). ACM."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_2_1_18_1","volume-title":"CAV (LNCS","author":"Atig Mohamed Faouzi","unstructured":"Mohamed Faouzi Atig , Ahmed Bouajjani , and Gennaro Parlato . 2011. Getting Rid of Store-Bufers in TSO Analysis . In CAV (LNCS , Vol. 6806 ). Springer , 99-115. Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2011. Getting Rid of Store-Bufers in TSO Analysis. In CAV (LNCS, Vol. 6806 ). Springer, 99-115."},{"key":"e_1_2_1_19_1","volume-title":"FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. 21-38","author":"Atig Mohamed Faouzi","year":"2014","unstructured":"Mohamed Faouzi Atig , Ahmed Bouajjani , and Gennaro Parlato . 2014 . Context-Bounded Analysis of TSO Systems. In From Programs to Systems. The Systems perspective in Computing-ETAPS Workshop , FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. 21-38 . Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2014. Context-Bounded Analysis of TSO Systems. In From Programs to Systems. The Systems perspective in Computing-ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. 21-38."},{"key":"e_1_2_1_20_1","first-page":"55","article-title":"Mathematizing C+ + concurrency","author":"Batty M.","year":"2011","unstructured":"M. Batty , S. Owens , S. Sarkar , P. Sewell , and T. Weber . 2011 . Mathematizing C+ + concurrency . In POPL. ACM , 55 - 66 . M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. 2011. Mathematizing C+ + concurrency. In POPL. ACM, 55-66.","journal-title":"POPL. ACM"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000011"},{"key":"e_1_2_1_22_1","volume-title":"Larus","author":"Cohen Nachshon","year":"2018","unstructured":"Nachshon Cohen , David T. Aksun , and James R . Larus . 2018 . Object-oriented recovery for non-volatile memory. PACMPL 2, OOPSLA ( 2018 ). Nachshon Cohen, David T. Aksun, and James R. Larus. 2018. Object-oriented recovery for non-volatile memory. PACMPL 2, OOPSLA ( 2018 )."},{"key":"e_1_2_1_23_1","first-page":"20","article-title":"SATCheck: SAT-directed stateless model checking for SC and TSO","author":"Demsky Brian","year":"2015","unstructured":"Brian Demsky and Patrick Lam . 2015 . SATCheck: SAT-directed stateless model checking for SC and TSO . In OOPSLA. ACM , 20 - 36 . Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-directed stateless model checking for SC and TSO. In OOPSLA. ACM, 20-36.","journal-title":"OOPSLA. ACM"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_25_1","first-page":"608","article-title":"Modelling the ARMv8 architecture, operationally: concurrency and ISA","author":"Flur Shaked","year":"2016","unstructured":"Shaked Flur , Kathryn E. Gray , Christopher Pulte , Susmit Sarkar , Ali Sezgin , Luc Maranget , Will Deacon , and Peter Sewell . 2016 . Modelling the ARMv8 architecture, operationally: concurrency and ISA . In POPL. ACM , 608 - 621 . Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In POPL. ACM, 608-621.","journal-title":"POPL. ACM"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_1_27_1","unstructured":"Intel. 2019a. Architectures Software Developer's Manual (Combined Volumes). Software.intel.com.  Intel. 2019a. Architectures Software Developer's Manual (Combined Volumes). Software.intel.com."},{"key":"e_1_2_1_28_1","unstructured":"Intel (Ed.). 2019b. Intel 64 and IA-32 Architectures Software Developer's Manual (Combined Volumes). Intel.  Intel (Ed.). 2019b. Intel 64 and IA-32 Architectures Software Developer's Manual (Combined Volumes). Intel."},{"key":"e_1_2_1_29_1","unstructured":"Intel. 2019c. Intel Optane Technology. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/inteloptane-technology. html.  Intel. 2019c. Intel Optane Technology. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/inteloptane-technology. html."},{"key":"e_1_2_1_30_1","first-page":"175","article-title":"A promising semantics for relaxedmemory concurrency","volume":"2017","author":"Kang Jeehoon","year":"2017","unstructured":"Jeehoon Kang , Chung-Kil Hur , Ori Lahav , Viktor Vafeiadis , and Derek Dreyer . 2017 . A promising semantics for relaxedmemory concurrency . In POPL 2017. 175 - 189 . Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxedmemory concurrency. In POPL 2017. 175-189.","journal-title":"POPL"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434328"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Michalis Kokologiannakis Ori Lahav Konstantinos Sagonas and Viktor Vafeiadis. 2018. Efective stateless model checking for C\/C++ concurrency. PACMPL 2 ( 2018 ) 17 : 1-17 : 32.  Michalis Kokologiannakis Ori Lahav Konstantinos Sagonas and Viktor Vafeiadis. 2018. Efective stateless model checking for C\/C++ concurrency. PACMPL 2 ( 2018 ) 17 : 1-17 : 32.","DOI":"10.1145\/3158105"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360599"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_2_1_37_1","unstructured":"Sihang Liu Korakit Seemakhupt Yizhou Wei Thomas F. Wenisch Aasheesh Kolli and Samira Khan. 2020. Cross Failure Bug Detection in Persistent Memory Programs. In ASPLOS.  Sihang Liu Korakit Seemakhupt Yizhou Wei Thomas F. Wenisch Aasheesh Kolli and Samira Khan. 2020. Cross Failure Bug Detection in Persistent Memory Programs. In ASPLOS."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304015"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_1_40_1","first-page":"111","article-title":"An operational semantics for C\/C++11 concurrency","author":"Nienhuis Kyndylan","year":"2016","unstructured":"Kyndylan Nienhuis , Kayvan Memarian , and Peter Sewell . 2016 . An operational semantics for C\/C++11 concurrency . In OOPSLA. ACM , 111 - 128 . Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. 2016. An operational semantics for C\/C++11 concurrency. In OOPSLA. ACM, 111-128.","journal-title":"OOPSLA. ACM"},{"key":"e_1_2_1_41_1","volume-title":"Wenisch","author":"Pelley Steven","year":"2014","unstructured":"Steven Pelley , Peter M. Chen , and Thomas F . Wenisch . 2014 . Memory persistency. In ISCA. Steven Pelley, Peter M. Chen, and Thomas F. Wenisch. 2014. Memory persistency. In ISCA."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_1_46_1","volume-title":"Francesco Zappa Nardelli, and Magnus O. Myreen","author":"Sewell Peter","year":"2010","unstructured":"Peter Sewell , Susmit Sarkar , Scott Owens , Francesco Zappa Nardelli, and Magnus O. Myreen . 2010 . x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53, 7 ( 2010 ), 89-97. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53, 7 ( 2010 ), 89-97."},{"key":"e_1_2_1_47_1","unstructured":"Fei Xia Dejun Jiang Jin Xiong and Ninghui Sun. 2017. HiKV: A Hybrid Index Key-Value Store for DRAM-NVM Memory Systems. In USENIX ATC Dilma Da Silva and Bryan Ford (Eds.).  Fei Xia Dejun Jiang Jin Xiong and Ninghui Sun. 2017. HiKV: A Hybrid Index Key-Value Store for DRAM-NVM Memory Systems. In USENIX ATC Dilma Da Silva and Bryan Ford (Eds.)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434337","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434337"],"URL":"https:\/\/doi.org\/10.1145\/3434337","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}