Permission accounting in separation logic.

Concurrent separation logic includes the notion of ‘ownership' of a heap data structure that can be transferred between processes. This paper refined that idea with permission – partial ownership – so that we could deal with shared read-only data. It applies that idea to two significant examples – readers-and-writers, in particular, had never before had a simple formal proof – and shows why at least two forms of permission are required. Separation logic has become a major influence on work in concurrency and in program analysis. Permissions are now routinely used in that work