计算机科学与技术专业毕业论文[精品论文]多处理机系统cache一致性协议模型检验关键技术研究

计算机科学与技术专业毕业论文[精品论文]多处理机系统cache一致性协议模型检验关键技术研究内容摘要：

L*公式弱保持，足以验证原始系统。 建立的具有真并发语义的参数化系统的形式化模型，适合描述一般意义上的并发系统，更具通用性和适用性。 理论推导和 Cache 一致性协议抽象实例都验证了 TDA 的正确性和合理性。 针对面向协议实现级的低层次验证脱节问题，本文开展了 RTL 级 Cache一致性协议模型检验研究。 在决策图模型的基础上，提出了利用约束逻辑编程对协议的 Verilog 描述进行谓词抽象的方法。 与基于 SAT 的方法相比，不需要将字级约束展开为位级约束，求解效率显著提高，并且提供了一个统一的框架用于描述各种约束。 结合工程需要，本文研究了高性能计算机的 Cache 一致性协议模型，以及协议的主要特点与主要性质，构建了面向高性能计算机的 Cache 协议模型检验平台 HVPCP，从高层协议级与 RTL 实现级两个层次实现 Cache 一致性协议的显式和隐式模型检验。 Cache 一致性协议是实现多处理机系 统的关键，不仅直接决定多处理机系统的正确性，而且对系统的规模和性能有着至关重要的影响。 日益增大的系统规模、存储一致性模型的多样性、互连网络延迟的不确定性、多核技术的迅猛发展等诸多因素交织在一起，使 Cache 一致性协议异常复杂，协议的状态空间出现爆炸，导致 Cache 一致性协议的功能验证非常困难，面临许多迫切需要解决的技术问题。 论文针对 Cache 一致性协议验证中的状态空间爆炸问题，结合新一代高效能并行计算机系统的研制，开展 Cache 一致性协议模型检验关键技术的研究。 以建立基于二维抽象的模型检验理论框架体系 为目标，面向显式和隐式两种模式、高层协议级和低层实现级两个层次，多角度展开研究，利用并行应用的数据访问特性和共享模式等领域知识设计恰当的优化方法，实现了高效的面向并行计算机系统Cache 协议模型检验平台，并能较好地扩展到大规模系统。 针对显式模型检验工具可达状态空间组织和维护存在的问题，本文提出了基于整型指针与Fibonacci 散列的可达状态空间组织方法，实现了一个高效的显式模型检验原型系统，在确保验证正确的同时有效缩短了验证时间，并且在系统规范不可满足的情况下能够给出反例，有助于系统设计人员快速定位错 误。 针对 Cache 协议状态空间爆炸的问题，本文分析了并行应用的数据访问特性和共享模式，提出了共享集合伪临界值的概念，有效优化了目录 Cache 协议状态空间，并提出了解决小概率的宽共享事件的方法。 实验数据表明，基于伪临界值的协议模型优化，能够有效缩小目录 Cache 协议的状态空间，加快验证速度，提高验证大规模 Cache协议的能力。 为支持可扩展 Cache 一致性协议的验证，本文提出了一个通用的参数化协议二维抽象框架 TDA，从构成系统状态空间的二维方向分别进行抽象，最大限度地剔除了原始系统中的冗余信息。 TDA模型关于单索引 ACTL*公式弱保持，足以验证原始系统。 建立的具有真并发语义的参数化系统的形式化模型，适合描述一般意义上的并发系统，更具通用性和适用性。 理论推导和 Cache 一致性协议抽象实例都验证了 TDA 的正确性和合理性。 针对面向协议实现级的低层次验证脱节问题，本文开展了 RTL 级 Cache 一致性协议模型检验研究。 在决策图模型的基础上，提出了利用约束逻辑编程对协议的 Verilog 描述进行谓词抽象的方法。 与基于 SAT 的方法相比，不需要将字级约束展开为位级约束，求解效率显著提高，并且提供了一个统一的框架用于 描述各种约束。 结合工程需要，本文研究了高性能计算机的 Cache 一致性协议模型，以及协议的主要特点与主要性质，构建了面向高性能计算机的 Cache 协议模型检验平台 HVPCP，从高层协议级与 RTL 实现级两个层次实现 Cache 一致性协议的显式和隐式模型检验。 Cache 一致性协议是实现多处理机系统的关键，不仅直接决定多处理机系统的正确性，而且对系统的规模和性能有着至关重要的影响。 日益增大的系统规模、存储一致性模型的多样性、互连网络延迟的不确定性、多核技术的迅猛发展等诸多因素交织在一起，使 Cache 一致性协议异 常复杂，协议的状态空间出现爆炸，导致 Cache 一致性协议的功能验证非常困难，面临许多迫切需要解决的技术问题。 论文针对 Cache 一致性协议验证中的状态空间爆炸问题，结合新一代高效能并行计算机系统的研制，开展 Cache 一致性协议模型检验关键技术的研究。 以建立基于二维抽象的模型检验理论框架体系为目标，面向显式和隐式两种模式、高层协议级和低层实现级两个层次，多角度展开研究，利用并行应用的数据访问特性和共享模式等领域知识设计恰当的优化方法，实现了高效的面向并行计算机系统Cache 协议模型检验平台，并能较好地扩展 到大规模系统。 针对显式模型检验工具可达状态空间组织和维护存在的问题，本文提出了基于整型指针与Fibonacci 散列的可达状态空间组织方法，实现了一个高效的显式模型检验原型系统，在确保验证正确的同时有效缩短了验证时间，并且在系统规范不可满足的情况下能够给出反例，有助于系统设计人员快速定位错误。 针对 Cache 协议状态空间爆炸的问题，本文分析了并行应用的数据访问特性和共享模式，提出了共享集合伪临界值的概念，有效优化了目录 Cache 协议状态空间，并提出了解决小概率的宽共享事件的方法。 实验数据表明，基于伪 临界值的协议模型优化，能够有效缩小目录 Cache 协议的状态空间，加快验证速度，提高验证大规模 Cache协议的能力。 为支持可扩展 Cache 一致性协议的验证，本文提出了一个通用的参数化协议二维抽象框架 TDA，从构成系统状态空间的二维方向分别进行抽象，最大限度地剔除了原始系统中的冗余信息。 TDA 模型关于单索引 ACTL*公式弱保持，足以验证原始系统。 建立的具有真并发语义的参数化系统的形式化模型，适合描述一般意义上的并发系统，更具通用性和适用性。 理论推导和 Cache 一致性协议抽象实例都验证了 TDA 的正确性和合理 性。 针对面向协议实现级的低层次验证脱节问题，本文开展了 RTL 级 Cache 一致性协议模型检验研究。 在决策图模型的基础上，提出了利用约束逻辑编程对协议的 Verilog 描述进行谓词抽象的方法。 与基于 SAT 的方法相比，不需要将字级约束展开为位级约束，求解效率显著提高，并且提供了一个统一的框架用于描述各种约束。 结合工程需要，本文研究了高性能计算机的 Cache 一致性协议模型，以及协议的主要特点与主要性质，构建了面向高性能计算机的 Cache 协议模型检验平台 HVPCP，从高层协议级与 RTL 实现级两个层次实现 Cache 一致性协议的显式和隐式模型检验。 Cache 一致性协议是实现多处理机系统的关键，不仅直接决定多处理机系统的正确性，而且对系统的规模和性能有着至关重要的影响。 日益增大的系统规模、存储一致。