Model Checking Transactional Memory with Spin
Model Checking Transactional Memory with Spin
复制标题
使用 Spin 检查事务内存的模型
DOI：
10.1145/1400751.1400816
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
M. Tuttle
中科院分区：
文献类型：
--
作者：
J. O'Leary;Bratin Saha;M. Tuttle
我们使用Spin模型检查器来证明英特尔对软件事务内存的实现是正确的。该事务内存使我们能够在不显式使用锁的情况下编写正确同步的多线程程序。我们描述了我们的英特尔实施模式，我们在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.