Standard

Iron : Managing obligations in higher-order concurrent separation logic. / Bizjak, Aleš; Gratzer, Daniel; Krebbers, Robbert; Birkedal, Lars.

In: Proceedings of the ACM on Programming Languages, Vol. 3, No. POPL, 65, 2019, p. 65:1-65:30.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

Bizjak, A, Gratzer, D, Krebbers, R & Birkedal, L 2019, 'Iron: Managing obligations in higher-order concurrent separation logic' Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 65, pp. 65:1-65:30. https://doi.org/10.1145/3290378

APA

Bizjak, A., Gratzer, D., Krebbers, R., & Birkedal, L. (2019). Iron: Managing obligations in higher-order concurrent separation logic. Proceedings of the ACM on Programming Languages, 3(POPL), 65:1-65:30. [65]. https://doi.org/10.1145/3290378

Vancouver

Bizjak A, Gratzer D, Krebbers R, Birkedal L. Iron: Managing obligations in higher-order concurrent separation logic. Proceedings of the ACM on Programming Languages. 2019;3(POPL):65:1-65:30. 65. https://doi.org/10.1145/3290378

Author

Bizjak, Aleš ; Gratzer, Daniel ; Krebbers, Robbert ; Birkedal, Lars. / Iron : Managing obligations in higher-order concurrent separation logic. In: Proceedings of the ACM on Programming Languages. 2019 ; Vol. 3, No. POPL. pp. 65:1-65:30.

BibTeX

@article{7192bb132b224f2fafaf3554ca3df5a6,
title = "Iron: Managing obligations in higher-order concurrent separation logic",
abstract = "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{\DH}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 concurrentseparation 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 ofIron, 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.",
keywords = "Separation logic, concurrency, resource management",
author = "Aleš Bizjak and Daniel Gratzer and Robbert Krebbers and Lars Birkedal",
year = "2019",
doi = "10.1145/3290378",
language = "English",
volume = "3",
pages = "65:1--65:30",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
number = "POPL",

}

RIS

TY - JOUR

T1 - Iron

T2 - Proceedings of the ACM on Programming Languages

AU - Bizjak, Aleš

AU - Gratzer, Daniel

AU - Krebbers, Robbert

AU - Birkedal, Lars

PY - 2019

Y1 - 2019

N2 - 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 concurrentseparation 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 ofIron, 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.

AB - 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 concurrentseparation 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 ofIron, 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.

KW - Separation logic

KW - concurrency

KW - resource management

U2 - 10.1145/3290378

DO - 10.1145/3290378

M3 - Article

VL - 3

SP - 65:1-65:30

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 65

ER -

ID: 51563794