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.