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.
- M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. on Programming Languages and Systems, 17(3):507--535, 1995.]] Google Scholar
Digital Library
- A.W. Appel. Foundational proof-carrying code. In Proc. 16th Annual IEEE Symposium on Logic in Computer Science, pages 247--258. IEEE Computer Society, June 2001.]] Google ScholarDigital Library
- R. Bornat, C. Calcagno, P. W. O'Hearn, and M. J. Parkinson. Permission accounting in separation logic. In Proc. 32th ACM Symp. on Principles of Prog. Lang., pages 259--270, 2005.]] Google ScholarDigital Library
- S. D. Brookes. A semantics for concurrent separation logic. In Proc. 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 16--34, 2004.]]Google ScholarCross Ref
- S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In ICSE'03: International Conference on Software Engineering, pages 385--395, 2003.]] Google ScholarDigital Library
- C. Colby, P. Lee, G. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for Java. In Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pages 95--107, New York, 2000. ACM Press.]] Google ScholarDigital Library
- T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95--120, 1988.]] Google ScholarDigital Library
- K. Crary. Toward a foundational typed assembly language. In Proc. 30th ACM Symp. on Principles of Prog. Lang., pages 198--212, 2003.]] Google ScholarDigital Library
- C. Demartini, R. Iosif, and R. Sisto. dSPIN: A dynamic extension of SPIN. In Proc. 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pages 261--276, London, UK, 1999. Springer-Verlag.]] Google ScholarDigital Library
- R. Ferreira and X. Feng. Coq (v8.0) implementation for CMAP language and the soundness proof. http://flint.cs.yale.edu/publications/cmap.html, Mar. 2005.]]Google Scholar
- C. Flanagan and M. Abadi. Object types against races. In CONCUR'99 - Concurrency Theory, volume 1664 of LNCS, pages 288--303. Springer-Verlag, 1999.]] Google Scholar
- C. Flanagan and M. Abadi. Types for safe locking. In Proceedings of the 8th European Symposium on Programming Languages and Systems, pages 91--108. Springer-Verlag, 1999.]] Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In Proc. 2002 European Symposium on Programming, pages 262--277. Springer-Verlag, 2002.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Thread-modular model checking. In Proc. 10th SPIN workshop, pages 213--224, May 2003.]]Google ScholarCross Ref
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proceedings of the ACM SIGPLAN 2003 conference on Programming Language Design and Implementation, pages 338--349, 2003.]] Google ScholarDigital Library
- D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In ASE'02: Automated Software Engineering, pages 3--12, 2002.]] Google ScholarDigital Library
- D. Grossman. Type-safe multithreading in cyclone. In Proceedings of the 2003 ACM SIGPLAN International workshop on Types in Languages Design and Implementation, pages 13--25, 2003.]] Google ScholarDigital Library
- N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Proc. Seventeenth Annual IEEE Symposium on Logic In Computer Science (LICS'02), pages 89--100. IEEE Computer Society, July 2002.]] Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model checking Java programs using Java pathfinder. Software Tools for Technology Transfer (STTT), 2(4):72--84, 2000.]]Google Scholar
- T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In PLDI'04: Programming Language Design and Implementation, pages 1--13, 2004.]] Google ScholarDigital Library
- C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666--677, 1978.]] Google ScholarDigital Library
- G. J. Holzmann. Proving properties of concurrent systems with SPIN. In Proc. 6th International Conference on Concurrency Theory (CONCUR'95), volume 962 of LNCS, pages 453--455. Springer, 1995.]] Google ScholarDigital Library
- C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 5(4):596--619, 1983.]] Google ScholarDigital Library
- L. Lamport. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 16(3):872--923, May 1994.]] Google ScholarDigital Library
- R. Milner. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., 1982.]] Google ScholarDigital Library
- G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: a realistic typed assembly language. In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, Atlanta, GA, May 1999.]]Google Scholar
- G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Prog. Lang., pages 85--97. ACM Press, Jan. 1998.]] Google ScholarDigital Library
- G. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang., pages 106--119. ACM Press, Jan. 1997.]] Google ScholarDigital Library
- G. Necula and P. Lee. The design and implementation of a certifying compiler. In Proc. 1998 ACM Conf. on Prog. Lang. Design and Impl., pages 333--344, New York, 1998.]] Google ScholarDigital Library
- Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. Technical report, Dec. 2004. http://flint.cs.yale.edu/publications/ecap.html.]]Google Scholar
- P. W. O'Hearn. Resources, concurrency and local reasoning. In Proc. 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 49--67, 2004.]]Google Scholar
- C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In Proc. TLCA, volume 664 of LNCS, 1993.]] Google ScholarDigital Library
- S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS'05: Tools and Algorithms for the Construction and Analysis of Systems, pages 93--107, 2005.]] Google ScholarDigital Library
- J. H. Reppy. CML: A higher concurrent language. In Proc. 1991 Conference on Programming Language Design and Implementation, pages 293--305, Toronto, Ontario, Canada, 1991. ACM Press.]] Google ScholarDigital Library
- E. W. Stark. A proof technique for rely/guarantee properties. In Proc. 5th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 206 of LNCS, pages 369--391, 1985.]] Google ScholarDigital Library
- K. Stølen. A method for the development of totally correct sharedstate parallel programs. In Proc. 2nd International Conference on Concurrency Theory (CONCUR'91), pages 510--525, 1991.]] Google ScholarDigital Library
- The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1, Oct. 2001.]]Google Scholar
- B. Werner. Une Théorie des Constructions Inductives. PhD thesis, A L'Université Paris 7, Paris, France, 1994.]]Google Scholar
- A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.]] Google ScholarDigital Library
- E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proc. 28th ACM Symp. on Principles of Prog. Lang., pages 27--40, New York, NY, USA, 2001. ACM Press.]] Google ScholarDigital Library
- D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. In Proc. 2003 European Symposium on Programming, LNCS Vol. 2618, pages 363--379, 2003.]]Google ScholarDigital Library
- D. Yu and Z. Shao. Verification of safety properties for concurrent assembly code. In Proc. 2004 ACM SIGPLAN Int'l Conf. on Functional Prog., September 2004.]] Google ScholarDigital Library
Index Terms
- Modular verification of concurrent assembly code with dynamic thread creation and termination
Recommendations
Modular verification of concurrent assembly code with dynamic thread creation and termination
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingProof-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 ...
Certifying concurrent programs using transactional memory
Transactional memory (TM) is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so that programmers do not have to reason ...
On the Verification of Strong Atomicity in Programs Using STM
SSIRI '09: Proceedings of the 2009 Third IEEE International Conference on Secure Software Integration and Reliability ImprovementTransactional memory(TM) provides an easy-using and high-performance parallel programming model for multicore systems. It simplifies parallel programming by supporting that transactions appear to execute atomically and in isolation. Despite the large ...
Comments