English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Rely-guarantee (RG) is a highly influential compositional proof technique forconcurrent programs, which was originally developed assuming a sequentiallyconsistent shared memory. In this paper, we first generalize RG to make itparametric with respect to the underlying memory model by introducing an RGframework that is applicable to any model axiomatically characterized by Hoaretriples. Second, we instantiate this framework for reasoning about concurrentprograms under causally consistent memory, which is formulated using a recentlyproposed potential-based operational semantics, thereby providing the firstreasoning technique for such semantics. The proposed program logic, which wecall Piccolo, employs a novel assertion language allowing one to specifyordered sequences of states that each thread may reach. We employ Piccolo formultiple litmus tests, as well as for an adaptation of Peterson's algorithm formutual exclusion to causally consistent memory.

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)