论文部分内容阅读
近年来,计算机处理器开始向多核化发展,单个核芯的主频提升速度变慢,但很多传统的软件和算法都是串行的,无法从核的增多上获得性能提升,因此急需并行化编译技术。虽然研究人员提出了多种并行化算法,适用于不同的情况,但是对这些并行化算法的正确性并没有给出形式化的证明。本文着眼于并行化算法的正确性研究,在Coq中定义了一种简单的类汇编的语言,并在此基础上实现了一种类似于解耦软件流水线(DSWP)的并行化算法,形式化地定义了算法的正确性,以及算法实现过程各个中间过程的正确性,并完成了各个中间过程正确性到算法最终正确性的证明,为最终完全形式化地证明该并行化算法提供帮助。
In recent years, computer processors have started to move toward multicore development. As a result, the clock speed of a single core has been slowed down. However, many traditional software and algorithms are serial and can not achieve performance gains from the increase of cores. Therefore, parallelization is urgently needed Compile technology. Although researchers have proposed a variety of parallelization algorithms for different situations, no formal proof has been given on the correctness of these parallelization algorithms. This paper focuses on the correctness of parallel algorithms, defines a simple class assembly language in Coq, and implements a parallel algorithm similar to Decoupled Software Pipelining (DSWP) The correctness of the algorithm and the correctness of each intermediate process in the process of algorithm implementation are defined. The correctness of each intermediate process to the final correctness of the algorithm is proved, which helps to prove the parallelized algorithm in the final formalization.