一种并行化算法在Coq中的实现及其正确性描述

• 作者: 孟建超
• 来源期刊: 电子技术
• 关键词: 并行化算法 正确性 形式化证明 解耦软件流水线 软件安全
• 年，卷（期）: 2015,（9）
• 所属期刊栏目: 电子技术教育
• 页码范围: 86-91
• 页数: 6页
• 字数: 5823字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-0755.2015.09.023

摘要

近年来，计算机处理器开始向多核化发展，单个核芯的主频提升速度变慢，但很多传统的软件和算法都是串行的，无法从核的增多上获得性能提升，因此急需并行化编译技术。虽然研究人员提出了多种并行化算法，适用于不同的情况，但是对这些并行化算法的正确性并没有给出形式化的证明。本文着眼于并行化算法的正确性研究，在Coq中定义了一种简单的类汇编的语言，并在此基础上实现了一种类似于解耦软件流水线（DSWP）的并行化算法，形式化地定义了算法的正确性，以及算法实现过程各个中间过程的正确性，并完成了各个中间过程正确性到算法最终正确性的证明，为最终完全形式化地证明该并行化算法提供帮助。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孟建超	中国科学技术大学计算机科学与技术学院	1	0	0.0	0.0