Step-Indexed Kripke Model of Separation Logic for Storable Locks

Abstract

We present a version of separation logic for modular reasoning about concurrent programs with dynamically allocated storable locks and dynamic thread creation. The assertions of the program logic are modelled by a Kripke model over a recursively de. ned set of worlds and the program logic is proved sound through a Kripke relation to the standard operational semantics. This constitutes an elegant solution to the circularity issue arising from lock resource invariants depending on worlds containing lock resource invariants.