Reasoning about concurrent programs is challenging, especially if data is shared among threads.
Program correctness can be violated by the presence of data races—whose prevention has been a topic of concern
both in research and in practice.
The Rust programming language is a prime example, putting the slogan fearless concurrency in practice
by not only employing an ownership-based type system for memory management,
but also using its type system to enforce mutual exclusion on shared data.
Locking, unfortunately, not only comes at the price of \emph{deadlocks} but shared access to data may also cause memory \emph{leaks}.

This paper develops a theory of deadlock and leak freedom for \emph{higher-order locks} in a shared memory concurrent setting.
Higher-order locks allow sharing not only of basic values but also of other locks and channels, and are themselves first-class citizens.
The theory is based on the notion of a \emph{sharing topology}, administrating who is permitted to access shared data at what point in the program.
The paper first develops higher-order locks for \emph{acyclic} sharing topologies,
instantiated in a $\lambda$-calculus with higher-order locks and message-passing concurrency.
The paper then extends the calculus to support \emph{circular} dependencies with \emph{dynamic} lock orders,
which we illustrate with a dynamic version of Dijkstra's dining philosophers problem.
Well-typed programs in the resulting calculi are shown to be free of deadlocks and memory leaks,
with proofs mechanized in the Coq proof assistant.