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.