  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.
