44 - Semantic model of CSL

Summary

Dijkstra presented semaphore-based mutual exclusion as an extension to a sequential language [37]. Posix threads present Dijkstra-Hoare concurrency as an extension to a sequential language [55]. O'Hearn presented concurrent separation logic (CSL) as an extension to separation logic, in which all the rules of sequential separation logic still hold [71].

Can we really model concurrency as an extension to sequentiality? Boehm explains why it is very tricky to explain shared-memory concurrency as an extension to a sequential language [24]. But we have taken great care to specify our language's external-interaction model (Chapter 33), in order to do this soundly.

Therefore we do something ambitious: we present the semantic model of CSL, for the C language, in the presence of an optimizing compiler and weak cache coherency, as a modular extension to our semantic model for sequential separation logic. This chapter is based on Aquinas Hobor's PhD thesis [49, 51] and on current work by Gordon Stewart.

Concurrent separation logic with first-class locks. O'Hearn's presentation of CSL had several limitations, most importantly a lack of first-class locks (locks that can be created/destroyed dynamically, and in particular can be used to control access to other locks). Hobor et al. [51] and Gotsman et al. [44] independently extended CSL to handle first-class locks as well as a number of other features.

Chapter 30 explains our CSL with first-class locks.