Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN

Kosuke Matsumoto, Tomoharu Ugawa, and Tatsuya Abe. Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN. Journal of Information Processing, 26, pages 314–326, 2018. DOI:10.2197/ipsjjip.26.314

Modern multi-core CPUs might execute memory access instructions of programs out-of-order. However, the SPIN model checker does not check out-of-order executions: it only checks in-order executions. We have devel- oped a library for SPIN that enables checking such out-of-order executions with respect to two memory models, the total store ordering (TSO) and the partial store ordering (PSO). This library provides models of variables shared with multiple threads (shared variables), and read and write macros to access them. Nevertheless, this library has three problems. First, although SPIN accepts Linear Temporal Logic (LTL) formulas, which are used for representing prop- erties to be checked such as safety and liveness, our library did not support LTL formulas referring to shared variables. Secondly, guard statements, which are often used for blocking threads while a guard is not executable, cannot refer to shared variables. Finally, the user was unable to specify initial values of shared variables, but they are initialized with zero. As presented herein, we improved the library to resolve these problems. We produced models using our improved library and investigated the library performance.