Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
This paper focuses on the problem of reason ing about concurrent assembly code with reentrant locks. Our verification technique is based on concurrent separation logic (CSL). In CSL, locks are treated as nonreentrant locks and each lock is associated with a resource invariant, the lock-protected resources are obtained and released through acquiring and releasing the lock respectively. In order to accommodate for reentrancy, we introduce some additional notions into our specification language to describe reentrant level for each acquiring and releasing lock operation. Keeping track of the reentrant level for each lock in the pre-and post conditions enables the program logic to ensure that resources are not re-acquired upon reentrancy, thus resources owned by a thread are prevented from reintroducing in the postcondition. Our framework is fully mechanized. Its soundness has been verified using the Coq proof assistant. We demonstrate the usage of our framework through giving a safety proof of a simple program.
reentrant locks concurrent separation logic safety program logic
Ming Fu Yu Zhang Yong Li
Department of Computer Science & Technology University of Science & Technology of China Hefei, 230027, China Software Security Laboratory Suzhou Institute for Advanced Study, USTC SuZhou, 215123, China
国际会议
天津
英文
233-240
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）