Treffer: Specifying and Verifying Programs Over the MCA ARMv8 Architecture with TLA+.

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's 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 + , 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. [ABSTRACT FROM AUTHOR]

Copyright of Journal of Circuits, Systems & Computers is the property of World Scientific Publishing Company and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)