摘要
German缓存一致性协议是用于共享内存的并发多处理器系统中的缓存一致性协议,对German协议进行形式化验证一直是学术界和工业界的热点.我们生成German协议的流图,对流程图的各个步骤进行详细的描述,并提出了流分析与归纳不变式结合对协议验证的方法,通过辅助不变式与协议流图的对应关系,从而进一步分析和验证German协议的正确性.
German cache coherence protocol is used in parallel multi-processor systems, and the verification of German protocol has always been a hot spot in international industry and academia. We generate the flow chart of German protocol and describe each step of the flow chart. Besides, we present a method to verify the cache coherence protocol by flow analysis and inductive invariants in this paper. By searching for the relations between the invariants and the flow chart of German protocol, we can further analyze and verify the correctness of German protocol.
作者
张瑜
孙文辉
ZHANG Yu SUN Wen-Hui(School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China)
出处
《计算机系统应用》
2017年第10期156-160,共5页
Computer Systems & Applications
基金
国家自然科学基金(61672503)
关键词
缓存一致性协议
流分析
归纳不变式
形式化验证
cache coherence protocol
flow analysis
inductive invariants
formal verification
