一种基于贝叶斯网络的随机测试方法在Cache一致性验证中的设计与实现

随着集成电路设计复杂度指数级增长,功能验证已经越来越成为大规模芯片设计的瓶颈,而在多核处理器中,Cache一致性协议十分复杂,验证难度大。针对Cache一致性协议验证提出基于模拟验证的一种基于贝叶斯网络的随机测试生成方法,解决Cache一致性协议状态空间爆炸的问题。首先分析了Cache一致性协议及基于贝叶斯网络推理的CDG方法,并将CDG方法应用于Cache一致性的验证。以FT处理器中的Cache一致性协议验证为例,对比伪随机测试,使用CDG方法将覆盖率提高近30%。     

模型检测MESIF Cache一致性协议

在处理器从单核向多核演进的过程中,为了获得更好的性能和可扩展性,适用于多核处理器系统的Cache一致性协议变得越来越复杂。Cache一致性协议的验证一直是模型检测在工业界主要应用之一,被工业界和学术界关注。相对传统方法而言,微结构级的模型检测能够描述和验证更多的协议细节。利用NuSMV工具对Intel公司的MESIF Cache一致性协议进行模型检测在微结构层次上进行了建模,并对该协议进行模型检测,试验结果证明了此方法的有效性。     

基于目录的Cache一致性协议的可扩展性研究

基于CC-NUMA结构的DSM多处理器系统是大规模高性能并行计算机的一个实现方式,由于比监听协议具有更好的扩展性,系统多采用基于目录的Cache一致性协议。但是,随着系统规模的不断扩大,目录协议同样面临着可扩展性的问题。本文在分析影响目录协议可扩展性因素的基础上,对当前比较典型的几种目录组织形式从存储开销方面进行了讨论,最后提出了基于目录Cache的两级目录组织方案。     

CC-NUMA系统分布共享I/O的数据一致性维护

Cache一致性维护是构建共享存储多处理器系统的关键,分布共享I/O系统和I/O数据一致性维护的实现方式将直接影响CC-NUMA系统的性能.基于大规模CC-NUMA系统SCCMP (scalable cache coherence multi-processors),构造并实现了基于HyperTransport互连架构的分布共享I/O子系统,由硬件维护I/O设备DMA访问的数据一致性,解决分布式缓存一致性问题.重点分析了I/O访问对Cache协议的影响,介绍了I/O数据一致性维护策略和硬件实现机制,并基于FPGA验证平台进行了系统I/O性能分析与评测.     

CC-NUMA系统中一种块传输通讯机制的设计与实现

本文描述了一种CC-NUMA结点控制器内实现的通信机制,通信请求通过描述符进行提交,利用CC-NUMA硬件实现的Cache一致性协议,实现高性能的一致性数据传输。基于这种通信机制,实现了高速通信软件接口,使用用户级通信技术,将硬件的通讯功能抽象出来给应用层使用,在测试中获得了较好的性能。     

多核处理器Cache一致性协议关键技术研究

多核处理器规模的不断扩大和核间通信机制的日益复杂,使得Cache一致性维护变得更加困难。本文从多核处理器Cache一致性问题的产生背景出发,分析监听协议、目录协议、Token协议和Hammer协议的实现机制以及在多核环境中的优缺点,分别从一致性协议与片上互连结构协同设计、面向低功耗应用的协议优化策略、Cache一致性协议验证及容错机制等角度考虑,对未来多核处理器Cache一致性协议设计的发展趋势和技术挑战进行详细分析与讨论。     

基于总线监听的Cache一致性协议分析

片内多处理器系统是当前计算机体系结构研究的热点问题之一。与传统的多处理机系统一样,Cache一致性问题也是片内多处理器系统必须首先解决的问题。本文首先介绍了片内多处理器系统中的Cache一致性问题及其解决方法,然后着重讨论了两种基于总线监听的Cache一致性协议：MSI协议和MESI协议,并对它们进行了分析比较。     

CMP中Cache一致性协议的验证

CMP是处理器体系结构发展的一个重要方向,其中Cache一致性问题的验证是CMP设计中的一项重要课题。基于MESI一致性协议,本文建立了CMP的Cache一致性协议的验证模型,总结了三种验证方法——状态列举法、模型检验法和符号状态法,并给出了每一种方法的复杂性分析。     

一种Cache一致性协议验证中覆盖率驱动的随机验证方法

随机验证技术是当今大规模集成电路仿真验证流程中的一项重要支撑技术,覆盖率驱动的随机测试生成方法是目前该领域研究的热点之一。针对Cache一致性协议的验证目标,介绍一种引入基于朴素贝叶斯模型的机器学习来完善基于覆盖率驱动的随机验证的方法,并结合相关的实际验证过程对该方法进行了分析和讨论。     

Pentium两级Cache一致性的实现

在简要介绍了维护多处理器系统中Cache一致性的MESI协议后,论述了Pentium计算机级1数据Cache具体采用的MESI协议,说明了Pentium两级Cache如何协调共同维护Cache的一致性。     

实现系统规模化的龙芯3号桥片设计与验证

CC-NUMA（高速缓存非均匀访存）系统应用在龙芯3A的处理器上,已得到了良好的性能体现,程序开发也有明显的简化。在维护片内和片间数据传输的稳定性和正确性的工作中,对基于一致性协议的片间互连结构进行分析和研究。为了构建更大规模的CC-NUMA系统而维护多处理器间的一致性。在片间利用互连桥片进行统一调度,从而保证跨系统访问和全局数据一致,并且实现了多核处理器在访存性能上的提升。所设计的桥片在部分结构上与龙芯3A二级缓存相似。通过定向和随机环境测试,验证了桥片在功能方面的正确性。     

基于不变量查找的German协议验证

提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.     

Model Checking Data Consistency for Cache Coherence Protocols

A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-orderμ-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.     

State space reduction in modeling checking parameterized cache coherence protocol by two-dimensional abstraction

Scalability of cache coherence protocol is a key component in future shared-memory multi-core or multi-processor systems. The state space explosion is the first hurdle while applying model-checking to scalable protocols. In order to validate parameterized cache coherence protocols effectively, we present a new method of reducing the state space of parameterized systems, two-dimensional abstraction (TDA). Drawing inspiration from the design principle of parameterized systems, an abstract model of an unbounded system is constructed out of finite states. The mathematical principles underlying TDA is presented. Theoretical reasoning demonstrates that TDA is correct and sound. An example of parameterized cache coherence protocol based on MESI illustrates how to produce a much smaller abstract model by TDA. We also demonstrate the power of our method by applying it to various well-known classes of protocols. During the development of TH-1A supercomputer system, TDA was used to verify the coherence protocol in FT-1000 CPU and showed the potential advantages in reducing the verification complexity.     

基于流分析与归纳不变式结合的German协议验证

German缓存一致性协议是用于共享内存的并发多处理器系统中的缓存一致性协议,对German协议进行形式化验证一直是学术界和工业界的热点.我们生成German协议的流图,对流程图的各个步骤进行详细的描述,并提出了流分析与归纳不变式结合对协议验证的方法,通过辅助不变式与协议流图的对应关系,从而进一步分析和验证German协议的正确性.     

Godson-T缓存一致性协议的Murphi建模和验证

Godson-T缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议．在Godson-T协议中,缓存一致性协议和存储一致性模型存在紧密的紧耦合关系,分析协议的一致性时发现该协议满足的缓存一致性不是强一致性,不满足传统意义上缓存透明的一致性要求．我们选取了Murphi模型检测工具作为我们建模的语言和验证工具．在对Godson-T缓存一致性协议建模的时候,由于协议的上述特点,我们需要对处理器核结点,高速缓存和内存作为一个整体建模,并成功地验证了协议的相关性质．     

Shared memory multiprocessor architectures for software IP routers

We propose new shared memory multiprocessor architectures and evaluate their performance for future Internet protocol (IP) routers based on symmetric multiprocessor (SMP) and cache coherent nonuniform memory access (CC-NUMA) paradigms. We also propose a benchmark application suite, RouterBench, which consists of four categories of applications representing key functions on the time-critical path of packet processing in routers. An execution driven simulation environment is created to evaluate SMP and CC-NUMA router architectures using this RouterBench. The execution driven simulation can produce accurate cycle-level execution time prediction and reveal the impact of various architectural parameters on the performance of routers. We port the FUNET trace and its routing table for use in our experiments. We find that the CC-NUMA architecture provides an excellent scalability for design of high-performance IP routers. Results also show that the CC-NUMA architecture can sustain good lookup performance, even at a high frequency of route updates.