Authors

Dachuan Yu
Zhong Shao

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 semi-automatically 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.

Published

• In Proc. 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP'04), Snowbird, Utah, pages 175-188, September 2004. ©2004 ACM.
• Gzipped Postscript [82k]
• PDF [135k]
• BibTex entry
• Implementation in Coq (v7.3.1) (tar.gz) [17k]