Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 17:15 - 17:30 at CPP - Program Logics Chair(s): William Mansky

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 logices, 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 elemetns 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.

Mon 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30
Program LogicsCPP at CPP
Chair(s): William Mansky University of Illinois at Chicago

Streamed session: https://youtu.be/poHYVOMQuro?t=3869

Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University
Pre-print Media Attached
Reasoning About Monotonicity in Separation Logic
Amin Timany Aarhus University, Lars Birkedal Aarhus University
Pre-print Media Attached