Verification of correctness of parallel algorithms in practice

Abstract

Verification of the correctness of parallel algorithms is often omitted in the works from the parallel computation field. In this paper, we discuss in detail how to show that a parallel algorithm is correct. This process involves proving its safety and liveness. In our case study, we prove the correctness of our two parallel algorithms for the NP-hard pickup and delivery problem with time windows. Both algorithms (for minimizing the number of routes and the travel distance) were already shown to be extremely efficient in practice—the implementations were thoroughly examined using the famous Li and Lim’s benchmark dataset.