  Separation logic is often praised for its ability to closely mimic the
locality of state updates when reasoning about them at the level of assertions.
The prover only needs to concern themselves with the footprint of the
computation at hand, i.e., the part of the state that is actually being
accessed and manipulated. Modern concurrent separation logics lift this local
reasoning principle from the physical state to abstract ghost state. For
instance, these logics allow one to abstract the state of a fine-grained
concurrent data structure by a predicate that provides a client the illusion of
atomic access to the underlying state. However, these abstractions
inadvertently increase the footprint of a computation: when reasoning about a
local low-level state update, one needs to account for its effect on the
abstraction, which encompasses a possibly unbounded portion of the low-level
state. Often this gives the reasoning a global character.
  We present context-aware (concurrent) separation logic (Co(Co)SL) to provide
new opportunities for local reasoning in the presence of rich ghost state
abstractions. Co(Co)SL introduces the notion of a context of a computation, the
part of the concrete state that is only affected on the abstract level.
Contexts give rise to a new proof rule that allows one to reduce the footprint
by the context, provided the computation preserves the context as an invariant.
The context rule complements the frame rule of separation logic by enabling
more local reasoning in cases where the predicate to be framed is known in
advance. We instantiate our developed theory for the flow framework, enabling
contextual reasoning about programs manipulating general heap graphs, and
describe two other applications of the logic. We have implemented the flow
instantiation of the logic in a proof outline checker and used it to verify two
highly-concurrent binary search trees.
