Languages

Formal Verification of Concurrent Programs with Read-Write Locks

Authors
Ming Fu
Yu Zhang
Yong Li
 
Abstract
Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent Separation Logic(CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reason about concurrent programs with read-write locks due to the different concurrent control mechanisms.
This paper focuses on extending CSL and present a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the memory with a writing permission set, denoted as logical memory , then define "strong separation" and "weak separation" over logical memory. Following CSL's local-reasoning idea, we develop a novel program logic to enforces weak separations of memory between different threads and support verification of concurrent programs with read-write locks.
Published