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

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.

Izumi Asakura

 He received his B.S. and M.S. degrees from Department of Mathematical and Computing Science, Tokyo Institute of Technology in 2014 and 2016, respectively.

Hidehiko Masuhara

 He is a Professor of Mathematical and Computing Science, Tokyo Institute of Technology. He is working on programming languages and software development environment. He received his B.S., M.S., and Ph.D. in Computer Science from Department of Information Science, University of Tokyo in 1992, 1994, and 1999, respectively. Before joining Tokyo Institute of Technology, he served as an assistant professor, lecturer, and associate professor at Department of Graphics and Computer Science, Graduate School of Arts and Sciences, University of Tokyo.

Tomoyuki Aotani

 He is an assistant professor at Department of Mathematical and Computing Science, Tokyo Institute of Technology. He received his BSc from Hosei University in 2004 and MA and PhD from the University of Tokyo in 2006 and 2009, respectively. His research interests include design of programming languages, program analysis, verification and optimization.