Memory Models for Architects and Compiler Writers

提出了一种新的内存模型，称为提交-调和栅栏（CRF），并展示了如何将其他内存模型描述为它的限制版本。CRF内存模型的设计使其既易于架构师实现，又足够丰富，以至于高级并行语言的编译器可以将其用作目标机器语言。这个建议是用来调查的。CRF与现代微处理器的集成；在分布式共享内存系统（DSM）中实现CRF的自适应协议；将高级多线程编程模型（如Cilk）有效地转换为CRF。这项研究的影响将是消除过多的依赖于实现的内存模型，并为架构师和编译器作者提供一个稳定的接口。支持CRF的微架构和缓存一致性协议的发展可能会对工业产生直接影响，因为这些变化可以在不损失软件兼容性的情况下合并到PC和服务器中。本提案的另一个主题是使用基于术语重写系统（TRS）的新的形式化框架来描述计算机系统。TRS最大的吸引力在于它对设计师的自然性。trs框架在验证系统属性时很有用。也可以从TRS合成硬件。统一的综合和验证框架可能对当前的设计实践产生重大影响。

A new memory model called Commit-Reconcile \& Fences (CRF) ispresented, and it is shown how other memory models can be described asrestricted versions of it. The CRF memory model has been designed sothat it is both easy for architects to implement, and rich enough thatcompilers for high-level parallel languages can use it as a targetmachine language. This proposal is for investigating 1. theintegration of CRF into modern microprocessors, 2. adaptive protocolsfor implementing CRF in Distributed Shared memory Systems (DSM) and3. efficient translation of high-level multithreaded programmingmodels (e.g. Cilk) into CRF. The impact of this research would be to eliminate a plethora ofimplementation-dependent memory models, and to provide a stableinterface for architects and compiler writers. The development ofmicro-architectures and cache-coherence protocols to support CRF couldhave an immediate impact on industry because these changes can beincorporated in PC's and servers without the loss of softwarecompatibility.Another theme in this proposal is the use of a new formal frameworkbased on Term Rewriting Systems (TRS) for describing computer systems.The biggest appeal of TRS's is its naturalness for designers. The TRSframework is useful in verification of system properties. It is alsopossible to synthesize hardware from TRS's. A unified synthesis andverification framework is likely to have a big impact on currentdesign practices.