Certified concurrent abstraction layers

ABSTRACT

Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) and reduce the complex dependencies among components at different levels of abstraction. Despite their obvious importance, concurrent abstraction layers have not been treated formally. This severely limits the applicability of layer-based techniques and makes it difficult to scale verification across multiple concurrent layers.

In this paper, we present CCAL---a fully mechanized programming toolkit developed under the CertiKOS project---for specifying, composing, compiling, and linking certified concurrent abstraction layers. CCAL consists of three technical novelties: a new game-theoretical, strategy-based compositional semantic model for concurrency (and its associated program verifiers), a set of formal linking theorems for composing multithreaded and multicore concurrent layers, and a new CompCertX compiler that supports certified thread-safe compilation and linking. The CCAL toolkit is implemented in Coq and supports layered concurrent programming in both C and assembly. It has been successfully applied to build a fully certified concurrent OS kernel with fine-grained locking.

References

1. Samson Abramsky and Paul-Andre Mellies. 1999. Concurrent Games and Full Completeness. In Proc. 14th IEEE Symposium on Logic in Computer Science (LICS'99). 431s442.
2. Thomas Anderson and Michael Dahlin. 2011. Operating Systems Principles and Practice. Recursive Books.
3. Carliss Y. Baldwin and Kim B. Clark. 2000. Design Rules: Volume 1, The Power of Modularity. MIT Press.
4. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Proc. 4th Symposium on Formal Methods for Components and Objects (FMCO'05). 364-387.
5. Stephen Brookes. 2004. A Semantics for Concurrent Separation Logic. In Proc. 15th International Conference on Concurrency Theory (CONCUR' 04). 16-34.
6. Stephen Chong, Joshua Guttman, Anupam Datta, Andrew Myers, Benjamin Pierce, Patrick Schaumont, Tim Sherwood, and Nickolai Zeldovich. 2016. Report on the NSF Workshop on Formal Methods for Security. people.csail.mit.edu/nickolai/papers/chong-nsf-sfm.pdf. (2016).
7. Xinyu Feng. 2009. Local Rely-Guarantee Reasoning. In Proc. 36th ACM Symposium on Principles of Programming Languages (POPL'09). 315-327.
8. Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In Proc. 16th European Symposium on Programming (ESOP'07). 173-188.
9. Xinyu Feng, Zhong Shao, Yuan Dong, and Yu Guo. 2008. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In Proc. 2008 ACM Conference on Programming Language Design and Implementation (PLDI'08). 170-182.
10. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, and Hongseok Yang. 2010. Abstraction for Concurrent Objects. Theor. Comput. Sci. 411, 51-52 (2010), 4379-4398.
11. Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010. Reasoning about Optimistic Concurrency Using a Program Logic for History. In Proc. 21st International Conference on Concurrency Theory (CONCUR'10). 388-402.
12. Dan R. Ghica and Andrzej S. Murawski. 2008. Angelic Semantics of Fine-Grained Concurrency. Annals of Pure and Applied Logic 151, 2-3 (2008), 89-114.
13. Alexey Gotsman, Noam Rinetzky, and Hongseok Yang. 2013. Verifying Concurrent Memory Reclamation Algorithms with Grace. In Proc. 22nd European Symposium on Programming (ESOP'13). 249s269.
14. Alexey Gotsman and Hongseok Yang. 2012. Linearizability with Ownership Transfer. In Proc. 23rd International Conference on Concurrency Theory (CONCUR'12). 256-271.
15. Ronghui Gu, Jeremie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan(Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15). 595-608.
16. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjoberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16). 653-669.
17. Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In Proc. 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14). 165-181.
18. Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serar Tasiran. 2015. Automated and Modular Refinement Reasoning for Concurrent Programs. In Proc. 27th International Conference on Computer Aided Verification (CAV'15). 449-465.
19. Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.
20. Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463-492.
21. C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (Oct. 1969), 576-580.
22. Bart Jacobs and Frank Piessens. 2011. Expressive Modular Fine-grained Concurrency Specification. In Proc. 38th ACM Symposium on Principles of Programming Languages (POPL'11). 133-146.
23. Ralf Jung, David Swasey, Filip Sieczkowski, Ksper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15). 637-650.
24. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive Formal Verification of an OS Microkernel. ACM Transactions on Computer Systems 32, 1 (Feb. 2014), 2:1-2:70.
25. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, et al. 2009. seL4: Formal Verification of an OS Kernel. In Proc. 22nd ACM Symposium on Operating System Principles (SOSP'09). 207-220.
26. Xavier Leroy. 2005-2018. The CompCert verified compiler. http://compcert.inria.fr/. (2005-2018).
27. Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107-115.
28. Xavier Leroy and Sandrine Blazy. 2008. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning 41, 1 (2008), 1-31.
29. Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective Auxiliary State for Coarse-Grained Concurrency. In Proc. 40th ACM Symposium on Principles of Programming Languages (POPL'13). 561-574.
30. Hongjin Liang and Xinyu Feng. 2016. A Program Logic for Concurrent Objects under Fair Scheduling. In Proc. 43rd ACM Symposium on Principles of Programming Languages (POPL'16). 385-399.
31. Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations. In Proc. 39th ACM Symposium on Principles of Programming Languages (POPL'12). 455-468.
32. Hongjin Liang, Xinyu Feng, and Zhong Shao. 2014. Compositional Verification of Termination-Preserving Refinement of Concurrent Programs. In Proc. Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and 29th IEEE Symposium on Logic in Computer Science (CSL-LICS'14). 65:1-65:10.
33. Hongjin Liang, Jan Hoffmann, Xinyu Feng, and Zhong Shao. 2013. Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. In Proc. 24th International Conference on Concurrency Theory (CONCUR'13). 227-241.
34. Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers, Inc.
35. Nancy A. Lynch and Frits W. Vaandrager. 1995. Forward and Backward Simulations: I. Untimed Systems. Inf. Comput. 121, 2 (1995), 214-233.
36. John M. Mellor-Crummey and Michael L. Scott. 1991. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Transactions on Computer Systems 9, 1 (Feb. 1991), 21-65.
37. Robin Milner. 1971. An Algebraic Definition of Simulation Between Programs. In Proc. 2nd International Joint Conference on Artificial Intelligence (IJCAI'71). 481-489.
38. Andrzej S. Murawski and Nikos Tzevelekos. 2016. An invitation to game semantics. ACM SIGLOG News 3, 2 (2016), 56-67.
39. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and German Andres Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In Proc. 23rd European Symposium on Programming (ESOP'14). 290-310.
40. Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2006. Polymorphism and Separation in Hoare Type Theory. In Proc. 2006 ACM SIGPLAN International Conference on Functional Programming (ICFP'06). 62-73.
41. Susumu Nishimura. 2013. A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables. In CSL 2013. 578-596.
42. Peter W. O'Hearn. 2004. Resources, Concurrency and Local Reasoning. In Proc. 15th International Conference on Concurrency Theory (CONCUR' 04). 49-67.
43. David Michael Ritchie Park. 1981. Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings. 167-183.
44. Pedro Da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In Proc. 28th European Conference on Object-Oriented Programming (ECOOP'14). 207-231.
45. Pedro Da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular Termination Verification for Non-blocking Concurrency. In Proc. 25th European Symposium on Programming (ESOP'16). 176-201.
46. John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. 17th IEEE Symposium on Logic in Computer Science (LICS'02). 55-74.
47. Silvin Rideau and Glynn Winskel. 2011. Concurrent Strategies. In Proc. 26th IEEE Symposium on Logic in Computer Science (LICS'11). 409-418.
48. Jerome H. Saltzer and M. Frans Kaashoek. 2009. Principles of Computer System Design. Morgan Kaufmann.
49. Davide Sangiorgi and David Walker. 2003. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge, England.
50. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized Verification of Fine-grained Concurrent Programs. In Proc. 2015 ACM Conference on Programming Language Design and Implementation (PLDI'15). 77-87.
51. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. In Proc. 24th European Symposium on Programming (ESOP'15). 333-358.
52. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Commun. ACM 53, 7 (2010), 89-97.
53. Vilhelm Sjoberg, Jieung Kim, Ronghui Gu, and Zhong Shao. 2017. Safety and Liveness of MCS LockDLayer by Layer. In Proc. 15th Asian Symposium on Programming Languages and Systems (APLAS'17). 273-297.
54. Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15). 275-287.
55. The Coq development team. 1999-2018. The Coq proof assistant. http://coq.inria.fr. (1999-2018).
56. Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying Refinement and Hoare-style Reasoning in a Logic for Higher-Order Concurrency. In Proc. 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP'13). 377-390.
57. Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical Relations for Fine-Grained Concurrency. In Proc. 40th ACM Symposium on Principles of Programming Languages (POPL'13). 343-356.
58. Viktor Vafeiadis and Matthew Parkinson. 2007. A Marriage of Rely/ Guarantee and Separation Logic. In Proc. 18th International Conference on Concurrency Theory (CONCUR'07). 256-271.
59. Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. 2016. A Practical Verification Framework for Preemptive OS Kernels. In Proc. 28th International Conference on Computer Aided Verification (CAV'16), Part II. 59-79.
60. Jean Yang and Chris Hawblitzel. 2010. Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System. In Proc. 2010 ACM Conference on Programming Language Design and Implementation (PLDI'10). 99-110.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Concurrent programming languages

  • Software organization and properties

    • Software functional properties

      • Correctness

        • Functionality

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

    • Abstraction

    • Logic and verification