CAJ | 학술논문

近年来，计算机处理器开始向多核化发展，单个核芯的主频提升速度变慢，但很多传统的软件和算法都是串行的，无法从核的增多上获得性能提升，因此急需并行化编译技术。虽然研究人员提出了多种并行化算法，适用于不同的情况，但是对这些并行化算法的正确性并没有给出形式化的证明。本文着眼于并行化算法的正确性研究，在Coq中定义了一种简单的类汇编的语言，并在此基础上实现了一种类似于解耦软件流水线（DSWP）的并行化算法，形式化地定义了算法的正确性，以及算法实现过程各个中间过程的正确性，并完成了各个中间过程正确性到算法最终正确性的证明，为最终完全形式化地证明该并行化算法提供帮助。
근년래，계산궤처리기개시향다핵화발전，단개핵심적주빈제승속도변만，단흔다전통적연건화산법도시천행적，무법종핵적증다상획득성능제승，인차급수병행화편역기술。수연연구인원제출료다충병행화산법，괄용우불동적정황，단시대저사병행화산법적정학성병몰유급출형식화적증명。본문착안우병행화산법적정학성연구，재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.