Formal verification of concurrent programs with read-write locks

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 heap model with a writing permission set, denoted as logical heap, then define "strong separation" and "weak separation" over logical heap. Following CSL's local-reasoning idea, we develop a novel program logic to enforces weak separations of heap between different threads and support verification of concurrent programs with ...

• Type: Journal
• Year: 2010
• Where: FCSC
• Authors: Ming Fu, Yu Zhang, Yong Li
• Keywords: Computer Science, Concurrent Programs, Concurrent Separation Logic, FCSC 2010, Read-write Locks