Model Checking Transactional Memory with Spin
John W. O’Leary, B. Saha, Mark R. Tuttle · 2009
We used the Spin model checker to show that Intel's implementation of software transactional memory is correct. Transactional memory makes it possible to write properly-synchronized multi-threaded programs without the explicit use of locks. We describe our model of Intel's implementation, our experience with Spin, what we have shown, and what obstacles remain to showing more.