Aarhus University Seal / Aarhus Universitets segl

Reasoning about monotonicity in separation logic

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Standard

Reasoning about monotonicity in separation logic. / Timany, Amin; Birkedal, Lars.

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). New York : Association for Computing Machinery, 2021. p. 91-104.

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Harvard

Timany, A & Birkedal, L 2021, Reasoning about monotonicity in separation logic. in Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). Association for Computing Machinery, New York, pp. 91-104, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021, Virtual, Online, Denmark, 17/01/2021. https://doi.org/10.1145/3437992.3439931

APA

Timany, A., & Birkedal, L. (2021). Reasoning about monotonicity in separation logic. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21) (pp. 91-104). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439931

CBE

Timany A, Birkedal L. 2021. Reasoning about monotonicity in separation logic. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). New York: Association for Computing Machinery. pp. 91-104. https://doi.org/10.1145/3437992.3439931

MLA

Timany, Amin and Lars Birkedal "Reasoning about monotonicity in separation logic". Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). New York: Association for Computing Machinery. 2021, 91-104. https://doi.org/10.1145/3437992.3439931

Vancouver

Timany A, Birkedal L. Reasoning about monotonicity in separation logic. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). New York: Association for Computing Machinery. 2021. p. 91-104 https://doi.org/10.1145/3437992.3439931

Author

Timany, Amin ; Birkedal, Lars. / Reasoning about monotonicity in separation logic. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). New York : Association for Computing Machinery, 2021. pp. 91-104

Bibtex

@inproceedings{8e4d288b153445c5a58440f9fc215748,
title = "Reasoning about monotonicity in separation logic",
abstract = "Reasoning about monotonicity is of key importance in concurrent separation logics. For instance, one needs to reason about monotonicity to show that the value of a concurrent counter with an increment operation only grows over time. Modern concurrent separation logics, such as VST, FCSL, and Iris, are based on resource models defined using partial commutative monoids. For any partial commutative monoid, there is a canonical ordering relation, the so-called extension order, and in a sense the logics are designed to reason about monotonicity wrt. the extension ordering. Thus a natural question is: Given an arbitrary preorder, can we construct a partial commutative monoid, where the extension order captures the given preorder. In this paper, we answer this question in the affirmative and show that there is a canonical construction, which given any preorder produces a partial commutative monoid for which the extension order, restricted to the elements of the preorder, is exactly the given preorder. We prove that our construction is a free construction in the category-theoretic sense. We demonstrate, using examples, that the general construction is useful. We have formalized the construction and its properties in Coq. Moreover, we have integrated it in the Iris program logic framework and used that to formalize our examples. ",
keywords = "monotonicity, partial commutative monoids, program verification, separation logic",
author = "Amin Timany and Lars Birkedal",
note = "Publisher Copyright: {\textcopyright} 2021 ACM. Copyright: Copyright 2021 Elsevier B.V., All rights reserved. .; 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 ; Conference date: 17-01-2021 Through 19-01-2021",
year = "2021",
month = jan,
doi = "10.1145/3437992.3439931",
language = "English",
isbn = "978-1-4503-8299-1",
pages = "91--104",
booktitle = "Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP {\textquoteright}21)",
publisher = "Association for Computing Machinery",
address = "United States",

}

RIS

TY - GEN

T1 - Reasoning about monotonicity in separation logic

AU - Timany, Amin

AU - Birkedal, Lars

N1 - Publisher Copyright: © 2021 ACM. Copyright: Copyright 2021 Elsevier B.V., All rights reserved. .

PY - 2021/1

Y1 - 2021/1

N2 - Reasoning about monotonicity is of key importance in concurrent separation logics. For instance, one needs to reason about monotonicity to show that the value of a concurrent counter with an increment operation only grows over time. Modern concurrent separation logics, such as VST, FCSL, and Iris, are based on resource models defined using partial commutative monoids. For any partial commutative monoid, there is a canonical ordering relation, the so-called extension order, and in a sense the logics are designed to reason about monotonicity wrt. the extension ordering. Thus a natural question is: Given an arbitrary preorder, can we construct a partial commutative monoid, where the extension order captures the given preorder. In this paper, we answer this question in the affirmative and show that there is a canonical construction, which given any preorder produces a partial commutative monoid for which the extension order, restricted to the elements of the preorder, is exactly the given preorder. We prove that our construction is a free construction in the category-theoretic sense. We demonstrate, using examples, that the general construction is useful. We have formalized the construction and its properties in Coq. Moreover, we have integrated it in the Iris program logic framework and used that to formalize our examples.

AB - Reasoning about monotonicity is of key importance in concurrent separation logics. For instance, one needs to reason about monotonicity to show that the value of a concurrent counter with an increment operation only grows over time. Modern concurrent separation logics, such as VST, FCSL, and Iris, are based on resource models defined using partial commutative monoids. For any partial commutative monoid, there is a canonical ordering relation, the so-called extension order, and in a sense the logics are designed to reason about monotonicity wrt. the extension ordering. Thus a natural question is: Given an arbitrary preorder, can we construct a partial commutative monoid, where the extension order captures the given preorder. In this paper, we answer this question in the affirmative and show that there is a canonical construction, which given any preorder produces a partial commutative monoid for which the extension order, restricted to the elements of the preorder, is exactly the given preorder. We prove that our construction is a free construction in the category-theoretic sense. We demonstrate, using examples, that the general construction is useful. We have formalized the construction and its properties in Coq. Moreover, we have integrated it in the Iris program logic framework and used that to formalize our examples.

KW - monotonicity

KW - partial commutative monoids

KW - program verification

KW - separation logic

UR - http://www.scopus.com/inward/record.url?scp=85100538690&partnerID=8YFLogxK

U2 - 10.1145/3437992.3439931

DO - 10.1145/3437992.3439931

M3 - Article in proceedings

AN - SCOPUS:85100538690

SN - 978-1-4503-8299-1

SP - 91

EP - 104

BT - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21)

PB - Association for Computing Machinery

CY - New York

T2 - 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021

Y2 - 17 January 2021 through 19 January 2021

ER -