Automated Verification of CountDownLatch

The CountDownLatch (CDL) is a versatile concurrency mechanism that was first introduced in Java 5, and is also being adopted into C++ and C#. Its usage allows one or more threads to exchange resources and synchronize by waiting for some tasks to be completed before others can proceed. In this paper, we propose a new framework for verifying the correctness of concurrent applications that use CDLs. Our framework is built on top of two existing mechanisms, concurrent abstract predicate and fictional separation logic, with some enhancements such as borrowed heap and thread local abstraction. In addition, we propose a new inconsistency detection mechanism based on waits-for relation to guarantee deadlock freedom. Prior concurrency verification works have mostly focused on data-race freedom. As a practical proof of concept, we have implemented this new specification and verification mechanism for CDL in a new tool, called HIPCAP, on top of an existing HIP verifier. We have used this new tool to successfully verify various use cases for CDL.