Aarhus University Seal / Aarhus Universitets segl

Reasoning about monotonicity in separation logic

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


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.

Original languageEnglish
Title of host publicationProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21)
Number of pages14
Place of publicationNew York
PublisherAssociation for Computing Machinery
Publication yearJan 2021
ISBN (print)978-1-4503-8299-1
Publication statusPublished - Jan 2021
Event10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 - Virtual, Online, Denmark
Duration: 17 Jan 202119 Jan 2021


Conference10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021
ByVirtual, Online

Bibliographical note

Publisher Copyright:
© 2021 ACM.

Copyright 2021 Elsevier B.V., All rights reserved. .

    Research areas

  • monotonicity, partial commutative monoids, program verification, separation logic

See relations at Aarhus University Citationformats

ID: 217507606