Model Checking Transactional Memory with Spin

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.