「Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq」

［Journal of Information Processing Vol.24 No,1 , pp.132-140］
［情報処理学会論文誌 プログラミング Vol.8 No.4, Preprint掲載］

［Abstract］

　In this paper, a concurrent separation logic for GPGPU, namely GPUCSL, is proposed and its soundness is proved by using Coq. GPUCSL is based on a CSL proposed by Blom et al., which is for automatic verification of GPGPU kernels, but employs different inference rules because the rules in Blom’s CSL are not standard. For example, Blom’s CSL does not have a frame rule. The CSL proposed is a simple extension of the original CSL, and it is more suitable as a basis of advanced properties proposed for other studies on CSLs. The soundness proof is based on Vafeiadis’ method, which is for a CSL with a fork-join concurrency model. The proof reveals two problems in Blom’s approach in terms of soundness and extensibility. First, their assumption that thread ID independence of a kernel implies barrier divergence freedom does not hold. Second, it is not easy to extend their proof to other CSLs with a frame rule. Although the CSL proposed covers only a subset of CUDA, the preliminary experiment shows that it is useful and expressive enough to verify a simple kernel with barriers.

［Recommendation］

　This paper redesigns a concurrent separation logic for GPGPU (GPUCSL), and proves the soundness of the logic by means of Coq, an interactive theorem prover. In writing a program in a programming language for GPGPU, a proper insertion of instructions for barrier synchronization into the program is one of heavy burdens for programmers. The construction of a program theory to reduce the burden on barrier synchronization must be one of the important contribution of this paper. It can be expected that the method shown in this paper would be applicable to parallel execution and thus very useful. Furthermore, the method can be used to verify that a program with barrier synchronization in GPGPU satisfies its specification, and hence we can expect that the result is widely applicable and very practical. The use of Coq in proving soundness of GUPCSL is very interesting as an application of interactive theorem provers. For these reasons above, the paper deserves the Outstanding Paper Award, and we would recommend this paper to the award.