Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ

Verification of concurrent programs is very tough because the proof needs to account for a huge number of interleavings of execution steps of all threads. As concurrent programs are often implemented in C/C++, which do not support garbage collection, program verification needs to consider memory reclamation as well. In this paper, we report the safe memory verification of two concurrent programs integrated with hazard pointers, a mechanism for safe memory reclamation. We use CafeOBJ to formally specify the two programs and the properties of interest. The formal proofs are produced with the assistance of a tool called IPSG.