Modular reasoning for modular concurrency

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 their clients. This talk will present CaReSL, the first logic to apply granularity abstraction for modular verification of higher-order concurrent programs. The talk is organized around a few simple but subtle examples that motivate CaReSL’s key ideas, and that ultimately come together in a significant case study: the first formal proof of correctness for Hendler et al.’s “flat combining” algorithm.