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

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

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

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

RCC高速缓存一致性协议的带参验证

Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统,对此协议的带参验证是一个很大的挑战。 Cubicle是最近出现的基于SMT求解器的带参模型检测工具。我们使用了Cubicle带参模型检测工具,成功对RCC协议进行了建模和验证。实验结果表明, RCC协议在结点个数为任意规模时均满足协议的各种安全性质。     

一类异构多智能体系统有向图下的广义平均一致性分析

本文对有向图下离散时间一阶二阶混合的异构多智能体系统广义平均一致性问题进行研究.首先给出了该异构系统广义平均一致性的基本概念.在此基础上,针对平均一致性研究中对交互拓扑为平衡网络的局限,提出了一种基于辅助变量的线性一致性协议,对每一个智能体增加一个辅助变量,用于记录个体的状态更新.采用图论、非负矩阵理论、特征值扰动等方法进行分析证明,表明该协议使得异构多智能体系统在任意强连通有向图下达到广义平均一致性.并对收敛值的性质进行了分析.最后,通过仿真对该结论进行了验证.     

遥感图像渐进式传输的GPU并行加速研究

遥感图像的渐进式传输大大提高了数据响应效率,但同时也增加了数据接收端的计算量。为进一步提高数据传输效率,研究了基于可编程图形硬件GPU的并行加速方法,通过小波逆变换的GPU并行化来加速图像重构,并通过纹理查找表来提高数据读取效率,利用离线渲染缓存Pbuffer来保存多层小波变换的中间计算结果,进一步提高了并行效率。最后,通过实验验证了该方法的有效性。     

片上多核处理器Cache一致性协议优化研究综述

现代晶体管技术在单芯片上集成多个处理器已经成为现实.近年来,随着多核处理器集成核数的不断增加,高速缓存的一致性问题凸显出来,已成为多核处理器的性能瓶颈之一,亟待解决.本文介绍了片上多核处理器一致性问题的由来.总结了多核时代高速缓存一致性协议设计的关键问题,综述了近年来学术界对一致性的研究.从程序访存行为模式、目录组织结构、一致性粒度、一致性协议流量、目录协议的可扩展性等方面,阐述了近年来缓存一致性协议性能优化的方向.对目前片上多核处理器缓存一致性协议设计中存在的问题进行了讨论,并指出了未来进一步研究的方向.     

基于动态分析的软件不变量综合技术

软件不变量是软件的重要属性，在软件验证、软件调试和软件测试等领域有重要作用.自20世纪末以来，基于动态分析的不变量综合技术成为相关领域的一个研究热点，并且取得了一定的进展.本文收集了90篇相关论文对该领域进行系统总结.基于动态分析的不变量综合技术是该领域的核心问题，本文提出了”学习者-预言”框架统一描述相关方法，并且在此框架内根据学习者的归纳方法将综合技术大致分为4类，分别是基于模板穷举的方法、基于数值计算的方法、基于统计学习的方法以及基于符号执行的方法.其次，本文讨论基于动态分析综合的不变量在软件验证和软件工程等领域的重要应用.随后，总结不变量生成技术中常用的实验对象程序和开源的不变量综合工具.最后，总结该领域并展望未来的研究方向.     

NTCIP协议一致性测试工具研究及实现

通过分析NTCIP协议一致性测试工具的现状,发现该协议一致性测试工具在国内的空白局面,因此通过分析NTCIP协议族及其协议验证方法,发现NTCIP协议是通过SNMP协议发送和接受报文,基于上述理论,设计开发了NTCIP协议一致性测试工具。本文介绍了基于SNMP协议的NTCIP协议一致性测试的研究工作,并介绍了该研究中设计和实现的协议一致性检测工具,该工具主要应用了SNMP++进行开发,实现了MIB文件的解析、MIB树的生成、SNMP报文组包发送接收及其验证和测试用例管理等功能,本工具通过SNMP协议发送和接受NTCIP报文,验证结果的正确性,在该领域填补了国内空白。     

基于PCIE的数字信号处理板设计与实现

介绍了一种数字信号处理算法评估验证平台的设计实现方法。该平台可通过软件进行配置,通过板卡上的大容量缓存对被测算法的输入、输出以及计算过程进行采集,并通过PCIE协议将采集结果上传至计算机,以使用户能够利用高级算法设计验证工具检验被测算法的有效性。     

温和一致性代理复制机制MCARM

提出了一种新的复制机制：温和一致性代理复制机制（MCARM）。MCARM采用了主节点的复制管理器与辅助节点的MSS-Agent协调工作的架构,吸取严格一致性协议和弱一致性协议的优势,又避开其局限性和复杂性,更好地适应移动计算环境的要求,并能与缓存失效策略CISBMA协同工作,较好满足了移动应用的需求。     

Design and formal verification of a hierarchical cache coherence protocol for NoC based multiprocessors

Advancement in semiconductor technology is allowing to pack more and more processing cores on a single die and scalable directory based protocols are needed for maintaining cache coherence. Most of the currently available directory based protocols are designed for mesh based topology and have the problem of delay and scalability. Cluster based coherence protocol is a better option than flat directory based protocol but the problem of mesh based topology is still exits. On the other hand, tree based topology takes fewer hop counts compared to mesh based topology. In this paper we give a hierarchical cache coherence protocol based on tree based topology. We divide the processing cores into clusters and each cluster shares a higher-level cache. At the next level we form clusters of caches connected to yet another higher-level cache. This is continued up to the top level cache/memory. We give various architectural placements that can benefit from the protocol; hop-count comparison; and memory overhead requirements. Finally, we formally verify the protocol using the Mur? tool.     

Formal automatic verification of cache coherence in multiprocessors with relaxed memory models

State-based, formal methods have been successfully applied to the automatic verification of cache coherence in sequentially consistent systems. However, coherence in shared memory multiprocessors under a relaxed memory model is much more complex to verify automatically. With relaxed memory models, incoming invalidations and outgoing updates can be delayed in each cache while processors are allowed to race ahead. This buffering of memory accesses considerably increases the amount of state in each cache and the complexity of protocol interactions. Moreover, because caches can hold inconsistent copies of the same data for long periods of time, coherence cannot be verified by simply checking that cached copies are identical at all times. This paper makes two major contributions. First, we demonstrate how to model and verify cache coherence under a relaxed memory model in the context of state-based verification methods. Frameworks for modeling the hardware and for generating correct memory access sequences driving the hardware model are developed. We also show correctness properties which must be verified on the hardware model. Second, we demonstrate a successful application of a state-based verification tool called SSM for the verification of the delayed protocol, an aggressive protocol for relaxed memory models. SSM is based on an abstraction technique preserving the properties to verify. We show that with classical, explicit approaches the verification of cache coherence is realistically unfeasible because of the state space explosion problem, whereas SSM is able to verify protocols both at both behavioral and message-passing levels.     

High Performance Software Coherence for Current and Future Architectures

Shared memory provides an attractive and intuitive programming model for large-scale parallel computing, but requires a coherence mechanism to allow caching for performance while ensuring that processors do not use stale data in their computation. Implementation options range from distributed shared memory emulations on networks of workstations to tightly coupled fully cache-coherent distributed shared memory multiprocessors. Previous work indicates that performance varies dramatically from one end of this spectrum to the other. Hardware cache coherence is fast, but also costly and time-consuming to design and implement, while DSM systems provide acceptable performance on only a limit class of applications. We claim that an intermediate hardware option-memory-mapped network interfaces that support a global physical address space, without cache coherence-can provide most of the performance benefits of fully cache-coherent hardware, at a fraction of the cost. To support this claim we present a software coherence protocol that runs on this class of machines, and use simulation to conduct a performance study. We look at both programming and architectural issues in the context of software and hardware coherence protocols. Our results suggest that software coherence on NCC-NUMA machines in a more cost-effective approach to large-scale shared-memory multiprocessing than either pure distributed shared memory or hardware cache coherence.     

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.     

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.     

存储模型仿真器的设计与实现

存储一致性问题和高速缓存一致性问题是共享存储并行计算机中两个最关键的问题,通过仿真器对它们进行了量化研究,设计并实现了一个存储模型仿真器MMS．基于MMS仿真了不同并行机结构模型下多种存储一致性模型的行为;针对不同类型的计算问题比较了不同的存储一致性模型,并对实验结果进行了分析;实现了几个不同的高速缓存一致性协议,并比较了它们的性能．     

模型检测MESIF Cache一致性协议

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