Description

PathFinder uses dynamic programming to find a path on a 2-D grid from the bottom row to the top row with the smallest accumulated weights, where each step of the path moves straight ahead or diagonally ahead. It iterates row by row, each node picks a neighboring node in the previous row that has the smallest accumulated weight, and adds its own weight to the sum[Rod].

Goal of this project

Given the impelmentation of Pathfinder for GPUs [OpenCL] from Rodinia Benchmark [Rod]. We want to specifiy and verify data-race freedom and also functional properties of the kernel. We use the technique we previosly developed for reasoning about the correctness of GPU programs [SCP,ByteC0ode]. We use VerCors tool set to automatically verify the specified kernel [VerCors].  

References

[ByteCode] M. Huisman and M. Mihelcic. Specification and Verification of GPGPUPrograms using Permission-Based Separation Logic. 2013.[.pdf]

[OpenCL] Khronos OpenCLWorking Group. The OpenCL Specification, version 1.2, 2001, URLhttp://www.khronos.org/registry/cl/specs/opencl-1.2.pdf

[VerCors]A. Amighi, S. Blom, M. Huisman, M. Zaharieva-Stojanovski. The VerCors Project. Setting Up Basecamp. In proceedings of Programming Languages meets Program Verification (PLPV 2012). ACM Digital Library. To appear. [.pdf]

[SCP] Stefan, Bloom, M. Huisman and M. Mihelcic, Specification and Verification of GPGPU programs. http://www.sciencedirect.com/science/article/pii/S0167642314001531

[Rod]http://www.cs.virginia.edu/~skadron/wiki/rodinia/index.php/Rodinia:Accelerating_Compute-Intensive_Applications_with_Accelerators