Nitpicking c++ concurrency
Nitpicking c++ concurrency
复制标题
吹毛求疵的c并发
DOI：
10.1145/2003476.2003493
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Blanchette J
中科院分区：
文献类型：
--
作者：
Blanchette J
以前的工作在Isabelle/HOL中形式化了C++内存模型，以澄清所提出的标准的语义。在这里，我们使用模型查找器Nitpick来检查执行内存模型的石蕊测试程序，包括一个简单的锁定算法。Nitpick构建在Kodkod（Alloy的后端）上，但理解Isabelle更丰富的逻辑;因此它可以直接应用于C++内存模型。我们只需要给它一些提示，由于底层的SAT求解器，它的扩展性比Cppstory显式状态模型检查器好得多。这个案例研究启发了Nitpick中的优化，其他形式化现在可以从中受益。
Previous work formalized the C++ memory model in Isabelle/HOL in an effort to clarify the proposed standard's semantics. Here we employ the model finder Nitpick to check litmus test programs that exercise the memory model, including a simple locking algorithm. Nitpick is built on Kodkod (Alloy's backend) but understands Isabelle's richer logic; hence it can be applied directly to the C++ memory model. We only need to give it a few hints, and thanks to the underlying SAT solver it scales much better than the Cppmem explicit-state model checker. This case study inspired optimizations in Nitpick from which other formalizations can now benefit.
登录
查看更多内容
C 并发数学化：后 Rapperswil 模型
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
Mark Batty;Scott Owens;Susmit Sarkar;Peter Sewell;Tjark Weber
通讯作者：
Tjark Weber
代数数据类型的关系分析
DOI：
--
发表时间：
2005
期刊：
ESEC/FSE-13
影响因子：
--
作者：
Viktor Kunčak;D. Jackson
通讯作者：
D. Jackson
MemSAT：检查内存模型的公理规范
影响因子：
--
作者：
Emina Torlak;M. Vaziri;Julian T Dolby
通讯作者：
Julian T Dolby
Java 内存模型模拟器
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
Jeremy Manson;W. Pugh
通讯作者：
W. Pugh
Visual-MCM：可视化多个内存一致性模型上的执行历史
DOI：
--
发表时间：
1999
期刊：
ACPC Conference
影响因子：
--
作者：
A. Melo;S. C. Chagas
通讯作者：
S. C. Chagas