{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:42:25Z","timestamp":1779392545595,"version":"3.53.1"},"reference-count":26,"publisher":"World Scientific Pub Co Pte Ltd","issue":"01","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62032024"],"award-info":[{"award-number":["62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Open Project of Shanghai Key Laboratory of Trustworthy Computing, the Fundamental Research Funds for the Central Universities","award":["2232024D-26"],"award-info":[{"award-number":["2232024D-26"]}]},{"name":"Digital Silk Road Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J CIRCUIT SYST COMP"],"published-print":{"date-parts":[[2026,1,15]]},"abstract":"<jats:p>Modern hardware architectures and mainstream programming languages employ relaxed memory models for efficiency purposes. However, these memory models may bring in many behaviors which do not adhere to people\u2019s intuition. In addition, different relaxed memory models produce different relaxed behaviors. The existing facts make the verification of the multi-threaded programs running against these models more difficult. In this paper, we are committed to proposing a general framework for modeling and verifying programs over various relaxed memory models, and we take the MCA ARMv8 architecture as an example. This architecture allows out-of-order execution through thread-local out-of-order, speculative execution and thread-local buffering. Above all, through analyzing the dependencies among statements, any program under MCA ARMv8 is translated into a unified form, which has the ability to describe each program under various memory models. Then, we model the translated programs with the formal specification language TLA[Formula: see text], and verify three properties, namely Reordering, Read-after-write elimination and Barriers, by the model checker TLC. Our verification results indicate that these properties align with the specification of MCA ARMv8. This not only validates the effectiveness of our method but also provides a more consistent approach for ensuring program correctness across a wide range of memory models.<\/jats:p>","DOI":"10.1142\/s0218126625300089","type":"journal-article","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T03:22:40Z","timestamp":1745983360000},"source":"Crossref","is-referenced-by-count":1,"title":["Specifying and Verifying Programs Over the MCA ARMv8 Architecture with TLA+"],"prefix":"10.1142","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9006-6219","authenticated-orcid":false,"given":"Lili","family":"Xiao","sequence":"first","affiliation":[{"name":"Donghua University, Shanghai, P. R. China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3266-0084","authenticated-orcid":false,"given":"Zhiru","family":"Hou","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, P. R. China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, P. R. China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1303-2760","authenticated-orcid":false,"given":"Mengda","family":"He","sequence":"additional","affiliation":[{"name":"Teesside University, Middlesbrough, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3028-8191","authenticated-orcid":false,"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[{"name":"Xidian University, Xi\u2019an, P. R. China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"219","published-online":{"date-parts":[[2025,6,23]]},"reference":[{"key":"S0218126625300089BIB001","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"S0218126625300089BIB002","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"S0218126625300089BIB003","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"S0218126625300089BIB004","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"S0218126625300089BIB005","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"S0218126625300089BIB006","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"S0218126625300089BIB008","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"S0218126625300089BIB009","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"S0218126625300089BIB010","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"S0218126625300089BIB011","first-page":"10:1","volume":"15","author":"Kavanagh R.","year":"2019","journal-title":"Logical Methods Comput. Sci."},{"key":"S0218126625300089BIB012","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002"},{"key":"S0218126625300089BIB013","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"S0218126625300089BIB014","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"S0218126625300089BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_32"},{"key":"S0218126625300089BIB016","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"S0218126625300089BIB017","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-021-1616-1"},{"key":"S0218126625300089BIB018","doi-asserted-by":"publisher","DOI":"10.1145\/3580285"},{"key":"S0218126625300089BIB019","doi-asserted-by":"publisher","DOI":"10.1145\/3545117"},{"key":"S0218126625300089BIB020","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2024.103225"},{"key":"S0218126625300089BIB021","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-66673-5_11"},{"key":"S0218126625300089BIB022","doi-asserted-by":"publisher","DOI":"10.1145\/3579835"},{"key":"S0218126625300089BIB023","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"S0218126625300089BIB024","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-020-0538-7"},{"key":"S0218126625300089BIB025","first-page":"1332","volume":"31","author":"Ji Y.","year":"2020","journal-title":"J. Softw."},{"key":"S0218126625300089BIB026","first-page":"2336","volume":"31","author":"Yi X.","year":"2020","journal-title":"J. Softw."},{"key":"S0218126625300089BIB027","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2024.3437344"}],"container-title":["Journal of Circuits, Systems and Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218126625300089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T07:55:06Z","timestamp":1761638106000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218126625300089"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,23]]},"references-count":26,"journal-issue":{"issue":"01","published-print":{"date-parts":[[2026,1,15]]}},"alternative-id":["10.1142\/S0218126625300089"],"URL":"https:\/\/doi.org\/10.1142\/s0218126625300089","relation":{},"ISSN":["0218-1266","1793-6454"],"issn-type":[{"value":"0218-1266","type":"print"},{"value":"1793-6454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,23]]},"article-number":"2530008"}}