{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:27Z","timestamp":1750220847310,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003825","name":"Magyar Tudom\u00e1nyos Akad\u00e9mia","doi-asserted-by":"crossref","award":["LP2015-12"],"award-info":[{"award-number":["LP2015-12"]}],"id":[{"id":"10.13039\/501100003825","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the na\u00efve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.<\/jats:p>","DOI":"10.1145\/3358238","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Will My Program Break on This Faulty Processor?"],"prefix":"10.1145","volume":"18","author":[{"given":"Levente","family":"Bajczi","sequence":"first","affiliation":[{"name":"Fault Tolerant Systems Research Group, Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[{"name":"Fault Tolerant Systems Research Group, Department of Measurement and Information Systems, Budapest University of Technology and Economics, Hungary and MTA-BME Lend\u00fclet Cyber-physical Systems Research Group, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[{"name":"Fault Tolerant Systems Research Group, Department of Measurement and Information Systems, Budapest University of Technology and Economics, Hungary and MTA-BME Lend\u00fclet Cyber-physical Systems Research Group, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Bengt Jonsson, and Tuan Phong Ngo.","author":"Abdulla Parosh Aziz","year":"2018","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Bengt Jonsson, and Tuan Phong Ngo. 2018 . Optimal stateless model checking under the release-acquire semantics. PACMPL 2, OOPSLA ( 2018), 135:1--135:29. DOI:https:\/\/doi.org\/10.1145\/3276505 Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018. Optimal stateless model checking under the release-acquire semantics. PACMPL 2, OOPSLA (2018), 135:1--135:29. DOI:https:\/\/doi.org\/10.1145\/3276505"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594347"},{"key":"e_1_2_1_4_1","unstructured":"ARM Limited. 2011. Cortex--A9 MPCore\u2122 Programmer Advice Notice: Read-after-read Hazards (Arm Reference 761319) (1 ed.). ARM Limited. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.uan0004a\/UAN0004A_a9_read_read.pdf.  ARM Limited. 2011. Cortex--A9 MPCore\u2122 Programmer Advice Notice: Read-after-read Hazards (Arm Reference 761319) (1 ed.). ARM Limited. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.uan0004a\/UAN0004A_a9_read_read.pdf."},{"key":"e_1_2_1_5_1","unstructured":"ARM Limited. 2011. Cortex\u2122--A9 MPCore\u00ae: Technical Reference Manual (7 ed.). ARM Limited. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ddi0407g\/DDI0407G_cortex_a9_mpcore_r3p0_trm.pdf.  ARM Limited. 2011. Cortex\u2122--A9 MPCore\u00ae: Technical Reference Manual (7 ed.). ARM Limited. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ddi0407g\/DDI0407G_cortex_a9_mpcore_r3p0_trm.pdf."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_8_1","volume-title":"CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Springer, 334--342","author":"Cavada Roberto","year":"2014","unstructured":"Roberto Cavada , Alessandro Cimatti , Michele Dorigatti , Alberto Griggio , Alessandro Mariotti , Andrea Micheli , Sergio Mover , Marco Roveri , and Stefano Tonetta . 2014 . The nuXmv symbolic model checker. In Computer Aided Verification - 26th International Conference , CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Springer, 334--342 . DOI:https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22 Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv symbolic model checker. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Springer, 334--342. DOI:https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"e_1_2_1_9_1","volume-title":"POPL","author":"Chakraborty Soham","year":"2019","unstructured":"Soham Chakraborty and Viktor Vafeiadis . 2019. Grounding thin-air reads with event structures. PACMPL 3 , POPL ( 2019 ), 70:1--70:28. DOI:https:\/\/doi.org\/10.1145\/3290383 Soham Chakraborty and Viktor Vafeiadis. 2019. Grounding thin-air reads with event structures. PACMPL 3, POPL (2019), 70:1--70:28. DOI:https:\/\/doi.org\/10.1145\/3290383"},{"key":"e_1_2_1_10_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2001","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 2001 . Model Checking. MIT Press . http:\/\/books.google.de\/books?id=Nmc4wEaLXFEC. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2001. Model Checking. MIT Press. http:\/\/books.google.de\/books?id=Nmc4wEaLXFEC."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 13th Annual Symposium on Computer Architecture","author":"Dubois Michel","year":"1986","unstructured":"Michel Dubois , Christoph Scheurich , and Faye A. Briggs . 1986. Memory access buffering in multiprocessors . In Proceedings of the 13th Annual Symposium on Computer Architecture , Tokyo, Japan , June 1986 . IEEE Computer Society, 434--442. https:\/\/dl.acm.org\/citation.cfm?id=17406 Michel Dubois, Christoph Scheurich, and Faye A. Briggs. 1986. Memory access buffering in multiprocessors. In Proceedings of the 13th Annual Symposium on Computer Architecture, Tokyo, Japan, June 1986. IEEE Computer Society, 434--442. https:\/\/dl.acm.org\/citation.cfm?id=17406"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/90994.91002"},{"volume-title":"The SPIN Model Checker - Primer and Reference Manual","author":"Holzmann Gerard J.","key":"e_1_2_1_15_1","unstructured":"Gerard J. Holzmann . 2004. The SPIN Model Checker - Primer and Reference Manual . Addison-Wesley . Gerard J. Holzmann. 2004. The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley."},{"volume-title":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual","author":"Intel Corporation","key":"e_1_2_1_16_1","unstructured":"Intel Corporation . 2015. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual . Intel Corporation . Intel Corporation. 2015. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. Intel Corporation."},{"key":"e_1_2_1_17_1","first-page":"201x","article-title":"Programming Languages --- C - Committee Draft","volume":"9899","author":"IEC.","year":"2010","unstructured":"ISO\/ IEC. 2010 . Programming Languages --- C - Committee Draft . ISO\/IEC. ISO\/IEC 9899 : 201x . ISO\/IEC. 2010. Programming Languages --- C - Committee Draft. ISO\/IEC. ISO\/IEC 9899:201x.","journal-title":"ISO\/IEC. ISO\/IEC"},{"key":"e_1_2_1_18_1","volume-title":"Spectre attacks: Exploiting speculative execution. meltdownattack.com","author":"Kocher Paul","year":"2018","unstructured":"Paul Kocher , Daniel Genkin , Daniel Gruss , Werner Haas , Mike Hamburg , Moritz Lipp , Stefan Mangard , Thomas Prescher , Michael Schwarz , and Yuval Yarom . 2018. Spectre attacks: Exploiting speculative execution. meltdownattack.com ( 2018 ). https:\/\/spectreattack.com\/spectre.pdf. Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2018. Spectre attacks: Exploiting speculative execution. meltdownattack.com (2018). https:\/\/spectreattack.com\/spectre.pdf."},{"key":"e_1_2_1_19_1","volume-title":"POPL","author":"Kokologiannakis Michalis","year":"2018","unstructured":"Michalis Kokologiannakis , Ori Lahav , Konstantinos Sagonas , and Viktor Vafeiadis . 2018. Effective stateless model checking for C\/C++ concurrency. PACMPL 2 , POPL ( 2018 ), 17:1--17:32. DOI:https:\/\/doi.org\/10.1145\/3158105 Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2018. Effective stateless model checking for C\/C++ concurrency. PACMPL 2, POPL (2018), 17:1--17:32. DOI:https:\/\/doi.org\/10.1145\/3158105"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872399"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830782"},{"key":"e_1_2_1_25_1","volume-title":"POPL","author":"Podkopaev Anton","year":"2019","unstructured":"Anton Podkopaev , Ori Lahav , and Viktor Vafeiadis . 2019. Bridging the gap between programming languages and hardware weak memory models. PACMPL 3 , POPL ( 2019 ), 69:1--69:31. DOI:https:\/\/doi.org\/10.1145\/3290382 Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2019. Bridging the gap between programming languages and hardware weak memory models. PACMPL 3, POPL (2019), 69:1--69:31. DOI:https:\/\/doi.org\/10.1145\/3290382"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"volume-title":"Formal specification of memory models","author":"Sindhu Pradeep S.","key":"e_1_2_1_27_1","unstructured":"Pradeep S. Sindhu , Jean-Marc Frailong , and Michel Cekleov . 1992. Formal specification of memory models . In Scalable Shared Memory Multiprocessors, Michel Dubois and Shreekant Thakkar (Eds.). Springer US , Boston, MA , 25--41. DOI:https:\/\/doi.org\/10.1007\/978-1-4615-3604-8_2 Pradeep S. Sindhu, Jean-Marc Frailong, and Michel Cekleov. 1992. Formal specification of memory models. In Scalable Shared Memory Multiprocessors, Michel Dubois and Shreekant Thakkar (Eds.). Springer US, Boston, MA, 25--41. DOI:https:\/\/doi.org\/10.1007\/978-1-4615-3604-8_2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037719"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358238","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358238","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358238"}},"subtitle":["Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software"],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":27,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358238"],"URL":"https:\/\/doi.org\/10.1145\/3358238","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}