Verification of Safety Properties for Concurrent Assembly Code
Abstract
Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concurrent programs using high-level languages and calculi, the verification of concurrent assembly code remains an open problem, largely due to the lack of abstraction at a low-level. Nevertheless, it is sometimes necessary to reason about assembly code or machine executables so as to achieve higher assurance. In this paper, we propose a logic-based "type" system for the static verification of concurrent assembly programs, applying the "invariance proof" technique for verifying general safety properties and the "assume-guarantee" paradigm for decomposition. In particular, we introduce a notion of "local guarantee" for the thread-modular verification in a non-preemptive setting. Our system is fully mechanized. Its soundness has been verified using the Coq proof assistant. A safety proof of a program is semiautomatically constructed with help of Coq, allowing the verification of even undecidable safety properties. We demonstrate the usage of our system using three examples, addressing mutual exclusion, deadlock freedom, and partial correctness respectively.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2004
- Accession Number
- ADA436482
Entities
People
- Dachuan Yu
- Zhong Shao
Organizations
- Yale University