We introduce the notion of a \emph{connectivity graph}—an abstract representation of the topology of concurrently interacting entities, which allows us to encapsulate generic principles of reasoning about deadlock freedom. Connectivity graphs are \emph{parametric} in their vertices (which represent entities like threads and channels) and their edges (which represent references between entities) with labels (which represent interaction protocols). To prove deadlock and memory leak freedom in the style of progress and preservation, we distill generic \emph{separation logic rules} for local graph transformations that preserve acyclicity of the connectivity graph, and a \emph{waiting induction} principle for acyclic connectivity graphs, to reason about global progress locally. We mechanize our results in Coq, and instantiate our method with a higher-order binary session-typed language to obtain the first mechanized proof of deadlock and leak freedom.