Formal Specification of Memory Models
Formal Specification of Memory Models
复制标题
DOI：
10.1007/978-1-4615-3604-8_2
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
P. Sindhu;J. Frailong;M. Cekleov
中科院分区：
文献类型：
--
作者：
P. Sindhu;J. Frailong;M. Cekleov
我们介绍了一个形式化的框架，用于描述共享存储多处理器的存储系统行为。该框架中的规范是公理的，因此避免了大多数现有规范中固有的歧义，这些规范是非正式的。该框架可以方便地构造硬件实现的正确性论证和生成关键程序片段的证明。通过提供一种可以指定一系列存储器模型的公共语言，该框架还允许比较现有的模型并便于探索可能的模型的空间。通过三个例子说明了该框架：著名的强一致性模型，以及由Sun Microsystem的SPARC体系结构定义的两个商店有序模型TSO和PSO。后两个模型就是使用该框架开发的。
We introduce a formal framework for specifying the behavior of memory systems for shared memory multiprocessors. Specifications in this framework are axiomatic, thereby avoiding ambiguities inherent in most existing specifications, which are informal. The framework makes it convenient to construct correctness arguments for hardware implementations and to generate proofs of critical program fragments. By providing a common language in which a range of memory models can be specified, the framework also permits comparison of existing models and facilitates exploration of the space of possible models. The framework is illustrated with three examples: the well-known Strong Consistency model, and two store ordered models TSO and PSO defined by the Sun Microsystem’s SPARC architecture. The latter two models were developed using this framework.