Authors
Xinyu Feng
Zhong Shao
Abstract
Proof-carrying code (PCC) is a general framework that can, in
principle, verify safety properties of arbitrary machine-language
programs. Existing PCC systems and typed assembly languages, however,
can only handle
sequential programs. This severely limits their
applicability since many real-world systems use some form of
concurrency in their core software. Recently Yu and Shao proposed a
logic-based ``type'' system for verifying concurrent assembly
programs. Their thread model, however, is rather restrictive in that
no threads can be created or terminated dynamically and no sharing
of code is allowed between threads. In this paper, we present
a new formal framework for verifying general
multi-threaded assembly code with unbounded dynamic thread creation
and termination as well as sharing of code between threads.
We adapt and generalize the rely-guarantee methodology to the assembly
level and show how to specify the semantics of thread ``fork'' with
argument passing. In particular, we allow threads to have different
assumptions and guarantees at different stages of their lifetime so they
can coexist with the dynamically changing thread environment.
Our work provides a foundation for certifying
realistic multi-threaded programs and makes an important advance toward
generating proof-carrying concurrent code.
Published
- In Proc. 2005 ACM SIGPLAN International Conference on
Functional Programming (ICFP'05), Tallinn, Estonia,
pages 254-267, September 2005. ©2005 ACM.