## Reasoning about monotonicity in separation logic

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

### Standard

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",
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",

}

### RIS

TY - GEN

T1 - Reasoning about monotonicity in separation logic

AU - Timany, Amin

AU - Birkedal, Lars

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 -