Concurrency errors due to poorly handled exceptions are common. Developers often make mistakes in writing proper code logic to relinquish the resources in the exception-handlers and cleanup blocks such as finally in Java. Our observations suggest that these mistakes often go unnoticed because the exception-handling code is generally not tested in the development phase. These errors materialize when the exception handlers execute within the production environment. Therefore, verifying multi-threaded programs augmented with their exception handlers is necessary to guarantee their correctness. This paper proposes a dynamic technique to verify exception-handling code in concurrent libraries. The technique detects the presence of deadlocks originating from exception-handling code. We also present a prototype called Lumina,that implements our technique to demonstrate that it can detect the deadlocks effectively, unlike the state-of-the-art dynamic verifier JavaPathfinder (JPF).

Multi-threaded libraries, including the ones advertised as thread-safe, may contain concurrency bugs, and worse, may not include relevant test cases that can drive the program execution towards bug-prone interleavings. Also, the effectiveness of dynamic verification, a prominent concurrency bug detection technique, depends critically on the availability of relevant test cases. Generating such test cases automatically to assist dynamic verification is, therefore, a significant problem.Among hard-to-detect concurrency bugs in multi-threaded Java libraries are communication deadlocks, which occur due to the incorrect usage of wait() and notify() communication primitives. In this work, we present a novel technique to systematically synthesize multi-threaded test cases to expose communication deadlocks. We model these deadlocks as global constraints over the events of two sequential program traces of the library APIs. The task of predicting the relevance of combining two sequential program traces is delegated to an SMT solver. We implement our technique in a prototype tool named REVELIO, and evaluate it on fifteen classes of popular multi-threaded Java libraries. We find that REVELIO is able to synthesize precise tests exposing communication deadlocks, which the state-of-the-art tools cannot.

The success of dynamic verification techniques for confirming the absence of bugs in concurrent programs rests on their ability to systematically address the interleaving space arising because of the nondeterminism. However, existing dynamic verification engines suffer from the problem of scalability due to the size of the reachable state space that grows exponentially as the number of parallel entities increases. The second front on which the dynamic verification technique struggles is the dependence on the test cases to drive the program, thus being as efficient as the quality of the test cases. Lastly, any verification technique suffers from the lack of a significant benchmark of bugs to prove its worth. This work tries to improve the area of dynamic verification concerning the limitations as mentioned above. We utilize the worthiness and popularity of constraint solvers and establish our work in the realm of concurrent programs.

Software evolution in third-party libraries across version upgrades can result in addition of new functionalities or change in existing APIs. As a result, there is a real danger of impairment of backward compatibility. Application developers, therefore, must keep constant vigil over library enhancements to ensure application consistency, i.e., application retains its semantic behavior across library upgrades. In this paper, we present the design and implementation of POLLUX, a framework to detect application-affecting changes across two versions of the same dependent non-adversarial library binary, and provide feedback on whether the application developer should link to the newer version or not. POLLUX leverages relevant application test cases to drive execution through both versions of the concerned library binary, records all concrete effects on the environment, and compares them to determine semantic similarity across the same API invocation for the two library versions. Our evaluation with 16 popular, open-source library binaries shows that POLLUX is accurate with no false positives and works across compiler optimizations.