Automated Verification of CountDownLatch

TL;DR

This paper introduces HIPCAP, a new verification framework and tool for ensuring correctness and deadlock freedom in concurrent applications using CountDownLatch, enhancing existing methods with novel mechanisms.

Contribution

It presents a new verification framework based on concurrent abstract predicate and fictional separation logic, with deadlock detection, implemented in the HIPCAP tool for CDL correctness.

Findings

Successfully verified various CDL use cases

Enhanced deadlock detection mechanism

Implemented in the HIPCAP verification tool

Abstract

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.