Formal verification of concurrent programs with
read-write locks |
| |
Authors: | Ming FU Yu ZHANG Yong LI |
| |
Affiliation: | School of Computer Science
and Technology, University of Science and Technology of China, Hefei
230027, China;Suzhou Institute for
Advanced Study, University of Science and Technology of China, Suzhou
215123, China; |
| |
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: | verification concurrent separation logic mutual exclusive locks read-write locks |
|
| 点击此处可从《Frontiers of Computer Science》浏览原始摘要信息 |
|
点击此处可从《Frontiers of Computer Science》下载全文 |
|