Iron: Managing obligations in higher-order concurrent separation logic

Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal

Research output: Contribution to journalArticleScientificpeer-review

63 Downloads (Pure)


Precise management of resources and the obligations they impose, such as the need to dispose of memory, close locks, and release file handles, is hardÐespecially in the presence of concurrency, when some resources are shared, and different threads operate on them concurrently. We present Iron, a novel higher-order concurrent
separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. In particular, Iron can be used to show the correctness of challenging examples, where the reclamation of memory is delegated to a forked-off thread. We show soundness of Iron by means of a model of
Iron, defined on top of the Iris base logic, and we use this model to prove that memory resources are accounted for precisely and not leaked. We have formalized all of the developments in the Coq proof assistant.
Original languageEnglish
Article number65
Pages (from-to)65:1-65:30
Number of pages30
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
Publication statusPublished - 2019


  • Separation logic
  • concurrency
  • resource management

Fingerprint Dive into the research topics of 'Iron: Managing obligations in higher-order concurrent separation logic'. Together they form a unique fingerprint.

Cite this