PrideMM：一种面向松弛内存模型的求解器
计算机科学中的逻辑
2019-01-03 v1 编程语言
摘要
松弛内存模型以微妙著称。为了便于研究，人们已经为公理化内存模型开发了若干专用模拟器。我们展示了如何使用 SO 求解器来模拟公理化内存模型。此外，我们展示了如何使用 MSO 求解器来模拟基于事件结构的内存模型。最后，我们提出了一个构建于 QBF 求解器之上的 SO 求解器。
引用
@article{arxiv.1901.00428,
title = {PrideMM: A Solver for Relaxed Memory Models},
author = {Simon Cooksey and Sarah Harris and Mark Batty and Radu Grigore and Mikoláš Janota},
journal= {arXiv preprint arXiv:1901.00428},
year = {2019}
}