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

Implementation of a Parallelizing Algorithm in Coq and its Correctness Description

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

In recent years, the multi-core computer became more and more popular, and the increasing of clock speed slow down, processor performance increased by the numbers of cores, but many traditional software and algorithms are single threaded and thus do not benefit, so we need parallelizing compiling technology. Although there are many parallelizing algorithms, but the correctness of these algorithms are not formally proved. This paper focuses on the correctness of parallelizing algorithm, we implemented a parallelizing algorithm similar to Decoupled Software Pipelining in Coq, and formally defined the correctness of the algorithm, we also define the correctness of each step of the parallelizing algorithm, it is helpful to the formal proof of the correctness of this algorithm.