article

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

Authors:

Zhong ShaoAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 9

Pages 254 - 267

https://doi.org/10.1145/1090189.1086399

Published: 12 September 2005 Publication History

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.

References

[1]

M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. on Programming Languages and Systems, 17(3):507--535, 1995.]]

Digital Library

[2]

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

Digital Library

[3]

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

Digital Library

[4]

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

[5]

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

Digital Library

[6]

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

Digital Library

[7]

T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95--120, 1988.]]

Digital Library

[8]

K. Crary. Toward a foundational typed assembly language. In Proc. 30th ACM Symp. on Principles of Prog. Lang., pages 198--212, 2003.]]

Digital Library

[9]

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

Digital Library

[10]

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

[11]

C. Flanagan and M. Abadi. Object types against races. In CONCUR'99 - Concurrency Theory, volume 1664 of LNCS, pages 288--303. Springer-Verlag, 1999.]]

[12]

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

Digital Library

[13]

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

Digital Library

[14]

C. Flanagan and S. Qadeer. Thread-modular model checking. In Proc. 10th SPIN workshop, pages 213--224, May 2003.]]

[15]

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

Digital Library

[16]

D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In ASE'02: Automated Software Engineering, pages 3--12, 2002.]]

Digital Library

[17]

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

Digital Library

[18]

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

Digital Library

[19]

K. Havelund and T. Pressburger. Model checking Java programs using Java pathfinder. Software Tools for Technology Transfer (STTT), 2(4):72--84, 2000.]]

[20]

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

Digital Library

[21]

C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666--677, 1978.]]

Digital Library

[22]

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

Digital Library

[23]

C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 5(4):596--619, 1983.]]

Digital Library

[24]

L. Lamport. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 16(3):872--923, May 1994.]]

Digital Library

[25]

R. Milner. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., 1982.]]

Digital Library

[26]

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

[27]

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

Digital Library

[28]

G. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang., pages 106--119. ACM Press, Jan. 1997.]]

Digital Library

[29]

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

Digital Library

[30]

Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. Technical report, Dec. 2004. http://flint.cs.yale.edu/publications/ecap.html.]]

[31]

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

[32]

C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In Proc. TLCA, volume 664 of LNCS, 1993.]]

Digital Library

[33]

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

Digital Library

[34]

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

Digital Library

[35]

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

Digital Library

[36]

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

Digital Library

[37]

The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1, Oct. 2001.]]

[38]

B. Werner. Une Théorie des Constructions Inductives. PhD thesis, A L'Université Paris 7, Paris, France, 1994.]]

[39]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.]]

Digital Library

[40]

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

Digital Library

[41]

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

Digital Library

[42]

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

Digital Library

Cited By

Wang JFu MQiao LFeng X(2019)Formalizing SPARCv8 Instruction Set Architecture in CoqScience of Computer Programming10.1016/j.scico.2019.102371(102371)Online publication date: Nov-2019
https://doi.org/10.1016/j.scico.2019.102371
Mirzamohammadi SAmiri Sani ABalan RMisra AAgarwal SMascolo C(2016)ViolaProceedings of the 14th Annual International Conference on Mobile Systems, Applications, and Services10.1145/2906388.2906391(263-276)Online publication date: 20-Jun-2016
https://dl.acm.org/doi/10.1145/2906388.2906391
Le DChin WTeo YAsai KSagonas K(2015)Threads as Resource for Concurrency VerificationProceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation10.1145/2678015.2682540(73-84)Online publication date: 13-Jan-2015
https://dl.acm.org/doi/10.1145/2678015.2682540
Show More Cited By

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
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

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

Transactional 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 9

Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

September 2005

330 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1090189

Issue’s Table of Contents

ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming
September 2005
342 pages
ISBN:1595930647
DOI:10.1145/1086365
General Chair:
Olivier Danvy
BRICS, University of Aarhus, Denmark
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 September 2005

Published in SIGPLAN Volume 40, Issue 9

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

72
Total Citations
View Citations
395
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)1

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang JFu MQiao LFeng X(2019)Formalizing SPARCv8 Instruction Set Architecture in CoqScience of Computer Programming10.1016/j.scico.2019.102371(102371)Online publication date: Nov-2019
https://doi.org/10.1016/j.scico.2019.102371
Mirzamohammadi SAmiri Sani ABalan RMisra AAgarwal SMascolo C(2016)ViolaProceedings of the 14th Annual International Conference on Mobile Systems, Applications, and Services10.1145/2906388.2906391(263-276)Online publication date: 20-Jun-2016
https://dl.acm.org/doi/10.1145/2906388.2906391
Le DChin WTeo YAsai KSagonas K(2015)Threads as Resource for Concurrency VerificationProceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation10.1145/2678015.2682540(73-84)Online publication date: 13-Jan-2015
https://dl.acm.org/doi/10.1145/2678015.2682540
Liu ZStepanenko SPichon-Pharabod JTimany AAskarov ABirkedal L(2023)VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-AProceedings of the ACM on Programming Languages10.1145/35912797:PLDI(1438-1462)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591279
Rao XGeorges ALegoupil MWatt CPichon-Pharabod JGardner PBirkedal L(2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591265
Smith G(2023)A Dafny-based approach to thread-local information flow analysis2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1109/FormaliSE58978.2023.00017(86-96)Online publication date: May-2023
https://doi.org/10.1109/FormaliSE58978.2023.00017
Mariescu-Istodor RFränti P(2017)Grid-Based Method for GPS Route Analysis for RetrievalACM Transactions on Spatial Algorithms and Systems10.1145/31256343:3(1-28)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3125634
Wang JFu MQiao LFeng X(2017)Formalizing SPARCv8 Instruction Set Architecture in CoqDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-319-69483-2_18(300-316)Online publication date: 17-Oct-2017
https://doi.org/10.1007/978-3-319-69483-2_18
Mirzamohammadi SAmiri Sani ABalan RMisra AAgarwal SMascolo C(2016)ViolaProceedings of the 14th Annual International Conference on Mobile Systems, Applications, and Services10.1145/2906388.2906391(263-276)Online publication date: 20-Jun-2016
https://dl.acm.org/doi/10.1145/2906388.2906391
Chlipala A(2015)From Network Interface to Multithreaded Web ApplicationsACM SIGPLAN Notices10.1145/2775051.267700350:1(609-622)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2775051.2677003
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents