Sciweavers

ICFP
2005
ACM

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

14 years 3 months ago
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...
Xinyu Feng, Zhong Shao
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2005
Where ICFP
Authors Xinyu Feng, Zhong Shao
Comments (0)