Formal Reasoning about Concurrent Assembly Code with Reentrant Locks

This paper focuses on the problem of reasoning about concurrent assembly code with reentrant locks. Our verification technique is based on concurrent separation logic (CSL). In CSL, locks are treated as non-reentrant locks and each lock is associated with a resource invariant, the lock-protected resources are obtained and released through acquiring and releasing the lock respectively. In order to accommodate for reentrancy, we introduce some additional notions into our specification language to describe reentrant level for each acquiring and releasing lock operation. Keeping track of the reentrant level for each lock in the pre- and post- conditions enables the program logic to ensure that resources are not reacquired upon reentrancy, thus resources owned by a thread are prevented from reintroducing in the postcondition. Our framework is fully mechanized. Its soundness has been verified using the Coq proof assistant. We demonstrate the usage of our framework through giving a safety proof of a simple program.