Modular programming and modular verification go hand in hand, but most existing logics for concurrency ignore two crucial forms of modularity: *higher-order functions*, which are essential for building reusable components, and *granularity abstraction*, a key technique for hiding the intricacies of fine-grained concurrent data structures from the clients of those data structures. In this paper, we present CaReSL, the first logic to support the use of granularity abstraction for modular verification of higher-order concurrent programs. After motivating the features of CaReSL through a variety of illustrative examples, we demonstrate its effectiveness by using it to tackle a significant case study: the first formal proof of (partial) correctness for Hendler et al.'s "flat combining" algorithm.
Proceedings of the 18th Acm Sigplan International Conference on Functional Programming, Icfp '13, 2013, p. 377-390
Main Research Area:
ACM SIGPLAN International Conference on FunctionalPprogrammingInternational Conference on Functional Programming, 2013