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

research-article

Open access

Mechanized verification of a fine-grained concurrent queue from meta’s folly library

Authors:

Simon Friis Vindum,

Lars BirkedalAuthors Info & Claims

CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 100 - 115

https://doi.org/10.1145/3497775.3503689

Published: 11 January 2022 Publication History

Abstract

We present the first formal specification and verification of the fine-grained concurrent multi-producer-multi-consumer queue algorithm from Meta’s C++ library Folly of core infrastructure components. The queue is highly optimized, practical, and used by Meta in production where it scales to thousands of consumer and producer threads. We present an implementation of the algorithm in an ML-like language and formally prove that it is a contextual refinement of a simple coarse-grained queue (a property that implies that the MPMC queue is linearizable). We use the ReLoC relational logic and the Iris program logic to carry out the proof and to mechanize it in the Coq proof assistant. The MPMC queue is implemented using three modules, and our proof is similarly modular. By using ReLoC and Iris’s support for modular reasoning we verify each module in isolation and compose these together. A key challenge of the MPMC queue is that it has a so-called external linearization point, which ReLoC has no support for reasoning about. Thus we extend ReLoC, both on paper and in Coq, with novel support for reasoning about external linearization points.

References

[1]

Bodil Biering, Lars Birkedal, and Noah Torp-Smith. 2007. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst., 29, 5 (2007), 24. https://doi.org/10.1145/1275497.1275499

Digital Library

[2]

Lars Birkedal and Aleš Bizjak. 2021. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https://iris-project.org/tutorial-material.html

[3]

Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. 2021. Theorems for free from separation logic specifications. Proc. ACM Program. Lang., 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473586

Digital Library

[4]

Nathan Bronson. 2020. On the origins of the MPMC Queue. Personal Communication.

[5]

Nathan Bronson, Zach Amsden, George Cabrera, Prasad Chakka, Peter Dimov, Hui Ding, Jack Ferris, Anthony Giardullo, Sachin Kulkarni, Harry Li, Mark Marchukov, Dmitri Petrov, Lovro Puzar, Yee Jiun Song, and Venkat Venkataramani. 2013. TAO: Facebook’ s Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference (USENIX ATC 13). USENIX Association, San Jose, CA. 49–60. isbn:978-1-931971-01-0 https://www.usenix.org/conference/atc13/technical-sessions/presentation/bronson

[6]

Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2015. Aspect-oriented linearizability proofs. Log. Methods Comput. Sci., 11, 1 (2015), https://doi.org/10.2168/LMCS-11(1:20)2015

[7]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In ECOOP (LNCS, Vol. 8586). 207–231. https://doi.org/10.1007/978-3-662-44202-9_9

Digital Library

[8]

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. 2013. Views: Compositional Reasoning for Concurrent Programs. In POPL. 287–300. https://doi.org/10.1145/2429069.2429104

Digital Library

[9]

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings, Theo D’Hondt (Ed.) (Lecture Notes in Computer Science, Vol. 6183). Springer, 504–528. https://doi.org/10.1007/978-3-642-14107-2_24

[10]

Brijesh Dongol and John Derrick. 2013. Simplifying proofs of linearisability using layers of abstraction. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 66 (2013), https://doi.org/10.14279/tuj.eceasst.66.889

[11]

Brijesh Dongol and John Derrick. 2015. Verifying Linearisability: A Comparative Survey. ACM Comput. Surv., 48, 2 (2015), 19:1–19:43. https://doi.org/10.1145/2796550

Digital Library

[12]

Brijesh Dongol, John Derrick, and Ian J. Hayes. 2012. Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 53 (2012), https://doi.org/10.14279/tuj.eceasst.53.792

[13]

Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. 2010. Abstraction for concurrent objects. Theoretical Computer Science, 411, 51-52 (2010), 4379–4398. https://doi.org/10.1016/j.tcs.2010.09.021

Digital Library

[14]

Hubertus Franke, Rusty Russell, and Matthew Kirkwood. 2002. Fuss, Futexes and Furwocks: Fast Userlevel Locking in Linux. In Proceedings of Ottawa Linux Symposium. 85, 479–495.

[15]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 442–451. https://doi.org/10.1145/3209108.3209174

Digital Library

[16]

Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2020. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR, abs/2006.13635 (2020), arxiv:2006.13635. arxiv:2006.13635

[17]

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. 2007. Local Reasoning for Storable Locks and Threads. In Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings. 19–37. https://doi.org/10.1007/978-3-540-76637-7_3

[18]

Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A Scalable Lock-Free Stack Algorithm. In SPAA. 206–215. https://doi.org/10.1145/1007912.1007944

Digital Library

[19]

Maurice Herlihy and Jeannette Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. TOPLAS, 12, 3 (1990), 463–492. https://doi.org/10.1145/78969.78972

Digital Library

[20]

John Hughes. 1989. Why Functional Programming Matters. Comput. J., 32, 2 (1989), 98–107. https://doi.org/10.1093/comjnl/32.2.98

Digital Library

[21]

Bart Jacobs and Frank Piessens. 2011. Expressive modular fine-grained concurrency specification. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 271–282. https://doi.org/10.1145/1926385.1926417

Digital Library

[22]

Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 256–269. https://doi.org/10.1145/2951913.2951943

Digital Library

[23]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 (2018), e20. https://doi.org/10.1017/S0956796818000151

[24]

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang., 4, POPL (2020), 45:1–45:32. https://doi.org/10.1145/3371113

Digital Library

[25]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 637–650. https://doi.org/10.1145/2676726.2676980

Digital Library

[26]

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain, Peter Müller (Ed.) (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 17:1–17:29. isbn:978-3-95977-035-4 https://doi.org/10.4230/LIPIcs.ECOOP.2017.17

[27]

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang., 2, ICFP (2018), 77:1–77:30. https://doi.org/10.1145/3236772

Digital Library

[28]

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Hongseok Yang (Ed.) (Lecture Notes in Computer Science, Vol. 10201). Springer, 696–723. https://doi.org/10.1007/978-3-662-54434-1_26

Digital Library

[29]

Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 205–217. http://dl.acm.org/citation.cfm?id=3009855

Digital Library

[30]

Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 459–470. https://doi.org/10.1145/2491956.2462189

Digital Library

[31]

John M. Mellor-Crummey and Michael L. Scott. 1991. Algorithms for scalable synchronization on shared-memory multiprocessors. TOCS, 9, 1 (1991), 21–65. https://doi.org/10.1145/103727.103729

Digital Library

[32]

Meta. 2021. Folly: Facebook Open-source Library. https://github.com/facebook/folly

[33]

Glen Mével and Jacques-Henri Jourdan. 2021. Formal verification of a concurrent bounded queue in a weak memory model. Proc. ACM Program. Lang., 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473571

Digital Library

[34]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2020. Cosmo: a concurrent separation logic for multicore OCaml. Proc. ACM Program. Lang., 4, ICFP (2020), 96:1–96:29. https://doi.org/10.1145/3408978

Digital Library

[35]

Maged Michael and Michael Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC. 267–275. https://doi.org/10.1145/248052.248106

Digital Library

[36]

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Zhong Shao (Ed.) (Lecture Notes in Computer Science, Vol. 8410). Springer, 290–310. https://doi.org/10.1007/978-3-642-54833-8_16

Digital Library

[37]

Matthew Parkinson and Gavin Bierman. 2005. Separation logic and abstraction. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, Jens Palsberg and Martín Abadi (Eds.). ACM, 247–258. https://doi.org/10.1145/1040305.1040326

Digital Library

[38]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 77–87. https://doi.org/10.1145/2737924.2737964

Digital Library

[39]

Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Zhong Shao (Ed.) (Lecture Notes in Computer Science, Vol. 8410). Springer, 149–168. https://doi.org/10.1007/978-3-642-54833-8_9

Digital Library

[40]

Kasper Svendsen, Lars Birkedal, and Matthew Parkinson. 2013. Modular Reasoning about Separation of Concurrent Data Structures. In ESOP (LNCS, Vol. 7792). 169–188. isbn:978-3-642-37036-6 https://doi.org/10.1007/978-3-642-37036-6_11

Digital Library

[41]

Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 377–390. https://doi.org/10.1145/2500365.2500600

Digital Library

[42]

Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 343–356. https://doi.org/10.1145/2429069.2429111

Digital Library

[43]

Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: navigating weak memory with ghosts, protocols, and separation. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014. 691–707. https://doi.org/10.1145/2660193.2660243

Digital Library

[44]

Aaron Turon and Mitchell Wand. 2011. A separation logic for refining concurrent objects. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 247–258. https://doi.org/10.1145/1926385.1926415

Digital Library

[45]

Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. Ph. D. Dissertation. University of Cambridge.

[46]

Viktor Vafeiadis and Matthew Parkinson. 2007. A Marriage of Rely/Guarantee and Separation Logic. In CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, Luís Caires and Vasco Thudichum Vasconcelos (Eds.) (Lecture Notes in Computer Science, Vol. 4703). Springer, 256–271. https://doi.org/10.1007/978-3-540-74407-8_18

[47]

Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue (proof pearl). 76–90 pages. https://doi.org/10.1145/3437992.3439930

Digital Library

[48]

Simon Friis Vindum, Dan Frumin, and Lars Birkedal. 2021. Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library - Coq Artefact. https://doi.org/10.5281/zenodo.5770802

[49]

Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, and Haibo Chen. 2019. Using concurrent relational logic with helpers for verifying the AtomFS file system. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, Tim Brecht and Carey Williamson (Eds.). ACM, 259–274. https://doi.org/10.1145/3341301.3359644

Digital Library

Cited By

Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689732
Nguyen DBeringer LMansky WWang STimany ATraytel DPientka BBlazy S(2024)Compositional Verification of Concurrent C Programs with Search Structure TemplatesProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636940(60-74)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636940
Koval NKhalanskiy DAlistarh D(2023)CQS: A Formally-Verified Framework for Fair and Abortable SynchronizationProceedings of the ACM on Programming Languages10.1145/35912307:PLDI(244-266)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591230
Show More Cited By

Index Terms

Mechanized verification of a fine-grained concurrent queue from meta’s folly library
1. Theory of computation
  1. Design and analysis of algorithms
    1. Concurrent algorithms
  2. Logic
    1. Separation logic

Recommendations

Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Mechanized verification of fine-grained concurrent programs
PLDI '15

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2022

351 pages

ISBN:9781450391825

DOI:10.1145/3497775

Program Chairs:
Andrei Popescu
University of Sheffield, UK
,
Steve Zdancewic
University of Pennsylvania, USA

Copyright © 2022 Owner/Author.

Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2022

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NWO
Villum Fonden

Conference

CPP '22

Sponsor:

SIGPLAN

CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 17 - 18, 2022

PA, Philadelphia, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
326
Total Downloads

Downloads (Last 12 months)146
Downloads (Last 6 weeks)17

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689732
Nguyen DBeringer LMansky WWang STimany ATraytel DPientka BBlazy S(2024)Compositional Verification of Concurrent C Programs with Search Structure TemplatesProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636940(60-74)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636940
Koval NKhalanskiy DAlistarh D(2023)CQS: A Formally-Verified Framework for Fair and Abortable SynchronizationProceedings of the ACM on Programming Languages10.1145/35912307:PLDI(244-266)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591230
Mulder IKrebbers R(2023)Proof Automation for Linearizability in Separation LogicProceedings of the ACM on Programming Languages10.1145/35860437:OOPSLA1(462-491)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586043
Mével GJourdan J(2021)Formal verification of a concurrent bounded queue in a weak memory modelProceedings of the ACM on Programming Languages10.1145/34735715:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473571

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents