Formal verification of concurrent programs with read-write locks |
| |
Authors: | Ming Fu Yu Zhang and Yong Li |
| |
Affiliation: | (1) School of Information and Engineering Sciences, Middlesex University, Middlesex, UK |
| |
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
reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.
This paper focuses on extending CSL and presenting 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 enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write
locks. |
| |
Keywords: | |
本文献已被 万方数据 SpringerLink 等数据库收录! |
|