Sciweavers

FCSC
2010

Formal verification of concurrent programs with read-write locks

13 years 1 months ago
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 ...
Ming Fu, Yu Zhang, Yong Li
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where FCSC
Authors Ming Fu, Yu Zhang, Yong Li
Comments (0)