More Web Proxy on the site http://driver.im/

research-article

Mechanized verification of fine-grained concurrent programs

Authors:

Aleksandar Nanevski,

Anindya BanerjeeAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 6

Pages 77 - 87

https://doi.org/10.1145/2813885.2737964

Published: 03 June 2015 Publication History

Abstract

Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated interference scenarios between threads, reasoning about such programs is challenging and error-prone, and can benefit from mechanization. In this paper, we present the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. Our tool is based on the recently proposed program logic FCSL. It is implemented as an embedded DSL in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning. We illustrate the proof layout in FCSL by example, outline its infrastructure, and report on our experience of using FCSL to verify a number of concurrent algorithms and data structures.

References

[1]

A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds, G. Stewart, S. Blazy, and X. Leroy. Program Logics for Certified Compilers. Cambridge University Press, 2014.

[2]

Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004.

Digital Library

[3]

R. Bornat, C. Calcagno, P. W. O’Hearn, and M. J. Parkinson. Permission accounting in separation logic. In POPL, pages 259–270. ACM, 2005.

Digital Library

[4]

S. Brookes. A semantics for concurrent separation logic. Th. Comp. Sci., 375(1-3), 2007.

Digital Library

[5]

C. Calcagno, M. J. Parkinson, and V. Vafeiadis. Modular safety checking for fine-grained concurrency. In SAS, volume 4634 of LNCS, pages 233–248. Springer, 2007.

Digital Library

[6]

A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234–245. ACM, 2011.

Digital Library

[7]

A. Chlipala. Certified Programming with Dependent Types. The MIT Press, 2013. Available from http://adam.chlipala.net/cpdt.

Digital Library

[8]

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs, volume 5674 of LNCS, pages 23–42. Springer, 2009.

Digital Library

[9]

E. Cohen, W. J. Paul, and S. Schmaltz. Theory of multi core hypervisor verification. In SOFSEM, volume 7741 of LNCS, pages 1–27. Springer, 2013.

[10]

Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.4, 2014. http://coq.inria.fr/.

[11]

P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. TaDA: A Logic for Time and Data Abstraction. In ECOOP, volume 8586 of LNCS, pages 207–231. Springer, 2014.

[12]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453–457, Aug. 1975.

Digital Library

[13]

T. Dinsdale-Young, L. Birkedal, P. Gardner, M. J. Parkinson, and H. Yang. Views: compositional reasoning for concurrent programs. In POPL, pages 287–300. ACM, 2013.

Digital Library

[14]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent Abstract Predicates. In ECOOP, volume 6183 of LNCS, pages 504–528. Springer, 2010.

Digital Library

[15]

X. Feng. Local rely-guarantee reasoning. In POPL, pages 315–327. ACM, 2009.

Digital Library

[16]

X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP, volume 4421 of LNCS, pages 173–188. Springer, 2007.

Digital Library

[17]

G. Gonthier, A. Mahboubi, and E. Tassi. A Small Scale Reflection Extension for the Coq system. Technical Report 6455, Microsoft Research – Inria Joint Centre, 2009.

[18]

G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer. How to make ad hoc proof automation less ad hoc. In ICFP, pages 163–175. ACM, 2011.

Digital Library

[19]

C. S. Gordon. Verifying Concurrent Programs by Controlling Alias Interference. PhD thesis, University of Washington, 2014.

[20]

D. Hendler, I. Incze, N. Shavit, and M. Tzafrir. Flat combining and the synchronization-parallelism tradeoff. In SPAA, pages 355–364, 2010.

Digital Library

[21]

M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst., 12(3):463–492, 1990.

Digital Library

[22]

A. Hobor and J. Villard. The ramifications of sharing in data structures. In POPL, pages 523–536. ACM, 2013.

Digital Library

[23]

B. Jacobs and F. Piessens. Expressive modular fine-grained concurrency specification. In POPL, pages 271–282. ACM, 2011.

Digital Library

[24]

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, volume 6617 of LNCS, pages 41–55. Springer, 2011.

Digital Library

[25]

J. B. Jensen, N. Benton, and A. Kennedy. High-level separation logic for low-level code. In POPL, pages 301–314. ACM, 2013.

Digital Library

[26]

C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Prog. Lang. Syst., 5(4):596–619, 1983.

Digital Library

[27]

C. B. Jones. The role of auxiliary variables in the formal development of concurrent programs. In Reflections on the Work of C.A.R. Hoare, pages 167–187. Springer London, 2010.

[28]

R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL, pages 637–650. ACM, 2015.

Digital Library

[29]

K. R. M. Leino and P. Müller. A basis for verifying multi-threaded programs. In ESOP, volume 5502 of LNCS, pages 378–393. Springer, 2009.

Digital Library

[30]

K. R. M. Leino, P. Müller, and J. Smans. Verification of Concurrent Programs with Chalice. In FOSAD, volume 5705 of LNCS, pages 195–222. Springer, 2009.

Digital Library

[31]

X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL, pages 42–54, 2006.

Digital Library

[32]

P. Letouzey. Extraction in Coq: An Overview. In Computability in Europe, volume 5028 of LNCS, pages 359–369. Springer, 2008.

Digital Library

[33]

R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarsegrained concurrency. In POPL, pages 561–574. ACM, 2013.

Digital Library

[34]

H. Liang and X. Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, pages 459–470. ACM, 2013.

Digital Library

[35]

P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory Vienna, 1968.

[36]

A. Mahboubi and E. Tassi. Canonical structures for the working Coq user. In ITP, volume 7998 of LNCS, pages 19–34. Springer, 2013.

Digital Library

[37]

A. Nanevski, R. Ley-Wild, I. Sergey, and G. A. Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In ESOP, volume 8410 of LNCS, pages 290–310. Springer, 2014. Extended version is available at http://software.imdea. org/fcsl/papers/concurroids-extended.pdf.

[38]

A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare Type Theory. In ICFP, pages 62–73. ACM, 2006.

Digital Library

[39]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In ICFP, pages 229– 240. ACM Press, 2008.

Digital Library

[40]

A. Nanevski, V. Vafeiadis, and J. Berdine. Structuring the verification of heap-manipulating programs. In POPL, pages 261–274. ACM, 2010.

Digital Library

[41]

P. W. O’Hearn. Resources, concurrency, and local reasoning. Th. Comp. Sci., 375(1-3):271–307, 2007.

Digital Library

[42]

S. S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM, 19(5):279–285, 1976.

Digital Library

[43]

S. Qadeer, A. Sezgin, and S. Tasiran. Back and forth: Prophecy variables for static verification of concurrent programs. Technical Report MSR-TR-2009-142, Microsoft Research, 2009.

[44]

A. Raad, J. Villard, and P. Gardner. CoLoSL: Concurrent Local Subjective Logic. In ESOP, volume 9032 of LNCS, pages 710–735. Springer, 2015.

[45]

J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, pages 55–74. IEEE Computer Society, 2002.

Digital Library

[46]

I. Sergey, A. Nanevski, and A. Banerjee. Mechanized verification of fine-grained concurrent programs. Accompanying code and tutorial. Available from http://software.imdea.org/fcsl.

Digital Library

[47]

I. Sergey, A. Nanevski, and A. Banerjee. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP, volume 9032 of LNCS, pages 333–358. Springer, 2015.

Digital Library

[48]

Z. Shao. Certified software. Commun. ACM, 53(12):56–66, 2010.

Digital Library

[49]

J. Smans, D. Vanoverberghe, D. Devriese, B. Jacobs, and F. Piessens. Shared boxes: Rely-Guarantee reasoning in VeriFast. CW Reports CW662, KU Leuven, May 2014.

[50]

M. Sozeau and N. Tabareau. Universe polymorphism in Coq. In ITP, volume 8558 of LNCS, pages 499–514. Springer, 2014.

[51]

K. Svendsen and L. Birkedal. Impredicative Concurrent Abstract Predicates. In ESOP, volume 8410 of LNCS, pages 149–168. Springer, 2014.

[52]

R. K. Treiber. Systems programming: coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center, 1986.

[53]

A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoarestyle reasoning in a logic for higher-order concurrency. In ICFP, pages 377–390. ACM, 2013.

Digital Library

[54]

V. Vafeiadis. RGSep Action Inference. In VMCAI, volume 5944 of LNCS, pages 345–361. Springer-Verlag, 2010.

Digital Library

[55]

V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, volume 4703 of LNCS, pages 256– 271. Springer, 2007.

Digital Library

[56]

F. Vogels. Formalisation and Soundness of Static Verification Algorithms for Imperative Programs. PhD thesis, KU Leuven, 2012.

Cited By

Kim JGu RShao Z(2024) : A simplified and abstract multicore hardware model for large scale system software formal verification Journal of Systems Architecture10.1016/j.sysarc.2023.103049147(103049)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103049
Kim JKoenig JChen HGu RShao Z(2024) : A template to build verified thread-local interfaces with software scheduler abstractions Journal of Systems Architecture10.1016/j.sysarc.2023.103046147(103046)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103046
Costea ATiwari AChianasta SR KRoychoudhury ASergey I(2023)Hippodrome: Data Race Repair Using Static Analysis SummariesACM Transactions on Software Engineering and Methodology10.1145/354694232:2(1-33)Online publication date: 31-Mar-2023
https://dl.acm.org/doi/10.1145/3546942
Show More Cited By

Index Terms

Mechanized verification of fine-grained concurrent programs
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

Mechanized verification of fine-grained concurrent programs
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated ...
Variables as Resource for Shared-Memory Programs: Semantics and Soundness

Parkinson, Bornat, and Calcagno recently introduced a logic for partial correctness in which program variables are treated as resource, generalizing earlier work based on separation logic and permissions. An advantage of their approach is that it yields ...
Execution privatization for scheduler-oblivious concurrent programs
OOPSLA '12

Making multithreaded execution less non-deterministic is a promising solution to address the difficulty of concurrent programming plagued by the non-deterministic thread scheduling. In fact, a vast category of concurrent programs are scheduler-oblivious:...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 6

PLDI '15

June 2015

630 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2813885

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2015
630 pages
ISBN:9781450334686
DOI:10.1145/2737924
General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

Copyright © 2015 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: 03 June 2015

Published in SIGPLAN Volume 50, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

85
Total Citations
View Citations
478
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)3

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kim JGu RShao Z(2024) : A simplified and abstract multicore hardware model for large scale system software formal verification Journal of Systems Architecture10.1016/j.sysarc.2023.103049147(103049)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103049
Kim JKoenig JChen HGu RShao Z(2024) : A template to build verified thread-local interfaces with software scheduler abstractions Journal of Systems Architecture10.1016/j.sysarc.2023.103046147(103046)Online publication date: Feb-2024
https://doi.org/10.1016/j.sysarc.2023.103046
Costea ATiwari AChianasta SR KRoychoudhury ASergey I(2023)Hippodrome: Data Race Repair Using Static Analysis SummariesACM Transactions on Software Engineering and Methodology10.1145/354694232:2(1-33)Online publication date: 31-Mar-2023
https://dl.acm.org/doi/10.1145/3546942
Wolf FSchwerhoff MMüller P(2023)Concise outlines for a complex logic: a proof outline checker for TaDAFormal Methods in System Design10.1007/s10703-023-00427-w61:1(110-136)Online publication date: 31-Jul-2023
https://doi.org/10.1007/s10703-023-00427-w
Meyer RWies TWolff S(2023)Make Flows Small Again: Revisiting the Flow FrameworkTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_32(628-646)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_32
Huisman MSeceleanu C(2022)Verification and Validation of Concurrent and Distributed Heterogeneous Systems (Track Summary)Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_24(417-421)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19849-6_24
Patel NKrishna SShasha DWies T(2021)Verifying concurrent multicopy search structuresProceedings of the ACM on Programming Languages10.1145/34854905:OOPSLA(1-32)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485490
Silver LZdancewic S(2021)Dijkstra monads forever: termination-sensitive specifications for interaction treesProceedings of the ACM on Programming Languages10.1145/34343075:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434307
Wolf FSchwerhoff MMüller P(2021)Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDAFormal Methods10.1007/978-3-030-90870-6_22(407-426)Online publication date: 10-Nov-2021
https://doi.org/10.1007/978-3-030-90870-6_22
Safari MOortwijn WHuisman M(2021)Automated Verification of the Parallel Bellman–Ford AlgorithmStatic Analysis10.1007/978-3-030-88806-0_17(346-358)Online publication date: 13-Oct-2021
https://doi.org/10.1007/978-3-030-88806-0_17
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