In this lecture, we will introduce several fine-grained concurrent algorithms that often rely on parsimonious usage of mutual exclusion, and often allow races. We will explain the verification challenges they pose in terms of functional soundness (sequential consistency, linearizability), progress properties (wait-freedom, lock-freedom, obstruction-freedom), and the approaches for solving these problems that are based on Separation Logic. We will in particular extend the previous proof system with a support for rely-guarantee, and show how it can be embedded in a permission-based approach called deny-guarantee.