Ilya Sergey
Aleksandar Nanevski
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.
- 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. Google Scholar
Cross Ref
- 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. Google ScholarDigital Library
- R. Bornat, C. Calcagno, P. W. O’Hearn, and M. J. Parkinson. Permission accounting in separation logic. In POPL, pages 259–270. ACM, 2005. Google ScholarDigital Library
- S. Brookes. A semantics for concurrent separation logic. Th. Comp. Sci., 375(1-3), 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234–245. ACM, 2011. Google ScholarDigital Library
- A. Chlipala. Certified Programming with Dependent Types. The MIT Press, 2013. Available from http://adam.chlipala.net/cpdt. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.4, 2014. http://coq.inria.fr/.Google Scholar
- 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.Google Scholar
- E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453–457, Aug. 1975. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- X. Feng. Local rely-guarantee reasoning. In POPL, pages 315–327. ACM, 2009. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- C. S. Gordon. Verifying Concurrent Programs by Controlling Alias Interference. PhD thesis, University of Washington, 2014.Google Scholar
- D. Hendler, I. Incze, N. Shavit, and M. Tzafrir. Flat combining and the synchronization-parallelism tradeoff. In SPAA, pages 355–364, 2010. Google ScholarDigital Library
- M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst., 12(3):463–492, 1990. Google ScholarDigital Library
- A. Hobor and J. Villard. The ramifications of sharing in data structures. In POPL, pages 523–536. ACM, 2013. Google ScholarDigital Library
- B. Jacobs and F. Piessens. Expressive modular fine-grained concurrency specification. In POPL, pages 271–282. ACM, 2011. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. B. Jensen, N. Benton, and A. Kennedy. High-level separation logic for low-level code. In POPL, pages 301–314. ACM, 2013. Google ScholarDigital Library
- C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Prog. Lang. Syst., 5(4):596–619, 1983. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL, pages 42–54, 2006. Google ScholarDigital Library
- P. Letouzey. Extraction in Coq: An Overview. In Computability in Europe, volume 5028 of LNCS, pages 359–369. Springer, 2008. Google ScholarDigital Library
- R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarsegrained concurrency. In POPL, pages 561–574. ACM, 2013. Google ScholarDigital Library
- H. Liang and X. Feng. Modular verification of linearizability with non-fixed linearization points. In PLDI, pages 459–470. ACM, 2013. Google ScholarDigital Library
- P. Lucas. Two constructive realizations of the block concept and their equivalence. Technical Report 25.085, IBM Laboratory Vienna, 1968.Google Scholar
- A. Mahboubi and E. Tassi. Canonical structures for the working Coq user. In ITP, volume 7998 of LNCS, pages 19–34. Springer, 2013. Google ScholarDigital Library
- 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.Google Scholar
- A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in Hoare Type Theory. In ICFP, pages 62–73. ACM, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Nanevski, V. Vafeiadis, and J. Berdine. Structuring the verification of heap-manipulating programs. In POPL, pages 261–274. ACM, 2010. Google ScholarDigital Library
- P. W. O’Hearn. Resources, concurrency, and local reasoning. Th. Comp. Sci., 375(1-3):271–307, 2007. Google ScholarDigital Library
- S. S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM, 19(5):279–285, 1976. Google ScholarDigital Library
- 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.Google Scholar
- A. Raad, J. Villard, and P. Gardner. CoLoSL: Concurrent Local Subjective Logic. In ESOP, volume 9032 of LNCS, pages 710–735. Springer, 2015.Google Scholar
- J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, pages 55–74. IEEE Computer Society, 2002. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Z. Shao. Certified software. Commun. ACM, 53(12):56–66, 2010.Google ScholarDigital Library
- 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.Google Scholar
- M. Sozeau and N. Tabareau. Universe polymorphism in Coq. In ITP, volume 8558 of LNCS, pages 499–514. Springer, 2014.Google Scholar
- K. Svendsen and L. Birkedal. Impredicative Concurrent Abstract Predicates. In ESOP, volume 8410 of LNCS, pages 149–168. Springer, 2014.Google Scholar
- R. K. Treiber. Systems programming: coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center, 1986.Google Scholar
- 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. Google ScholarDigital Library
- V. Vafeiadis. RGSep Action Inference. In VMCAI, volume 5944 of LNCS, pages 345–361. Springer-Verlag, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- F. Vogels. Formalisation and Soundness of Static Verification Algorithms for Imperative Programs. PhD thesis, KU Leuven, 2012.Google Scholar
Index Terms
- Mechanized verification of fine-grained concurrent programs
Recommendations
Mechanized verification of fine-grained concurrent programs
PLDI '15Efficient 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 ...
Compositional verification of termination-preserving refinement of concurrent programs
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)Many verification problems can be reduced to refinement verification. However, existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination, allowing a diverging program to trivially refine any ...
Comments