Modular verification of concurrent assembly code with dynamic thread creation and termination

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

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Xinyu Feng, Zhong Shao
• Keywords: Dynamic Thread Creation, ICFP 2005, Multi-threaded Assembly Code, Programming Languages, Unbounded Dynamic Thread