Information-flow models for shared memory with an application to the PowerPC architecture
Information-flow models for shared memory with an application to the PowerPC architecture
复制标题
DOI：
10.1109/tpds.2003.1199067
复制
发表时间：
2003-05-01
影响因子：
5.3
通讯作者：
Shurek, G
中科院分区：
文献类型：
--
作者：
Adir, A;Attiya, H;Shurek, G
本文介绍了一个通用框架，用于定义指令、程序以及它们在多处理器环境中通过操作实例化的语义。该框架通过从读操作到写操作的“读取自”映射来捕捉多处理器程序中操作之间的信息流。在操作上定义了两种基本关系：实例化某个处理器程序的操作之间的程序顺序，以及每个共享内存模型特有的视图顺序。一个操作不能从“隐藏的”过去读取，也不能从未来读取；可以相对于程序顺序或视图顺序来检查未来和过去的因果关系。共享内存模型针对给定程序指定资源状态的允许转换。内存模型应该通过引用多处理器在程序员可见的接口中的保证行为来反映程序员的观点。该模型不应规定实现应遵循的设计实践。我们的框架允许架构师揭示共享内存架构所引发的编程视图；它为探索编程接口限制的程序员服务，并指导架构级别的验证。该框架适用于复杂的商业架构，因为它能够捕捉微妙的编程接口细节，揭示底层激进的微架构机制。作为示例，我们在我们的框架内定义了PowerPC架构所支持的共享内存模型。
This paper introduces a generic framework for defining instructions, programs, and the semantics of their instantiation by operations in a multiprocessor environment. The framework captures information flow between operations in a multiprocessor program by means of a reads from mapping from read operations to write operations. Two fundamental relations are defined on the operations: a program order between operations which instantiate the program of some processor and view orders which are specific to each shared memory model. An operation cannot read from the "hidden" pastor from the future; the future and the past causality can be examined either relative to the program order or relative to the view orders. A shared memory model specifies, for a given program, the permissible transformation of resource states. The memory model should reflect the programmer's view by citing the guaranteed behavior of the multiprocessor in the interface visible to the programmer. The model should refrain from dictating the design practices that should be followed by the implementation. Our framework allows an architect to reveal the programming view induced by a shared-memory architecture; it serves programmers exploring the limits of the programming interface and guides architecture-level verification. The framework is applicable for complex, commercial architectures as it can capture subtle programming-interface details, exposing the underlying aggressive microarchitecture mechanisms. As an illustration, we define the shared memory model supported by the PowerPC architecture, within our framework.