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

Deductive verification of concurrent programs under weak memory has thus farbeen limited to simple programs over a monolithic state space. For scalability,we also require modular techniques with verifiable library abstractions. Thispaper addresses this challenge in the context of RC11 RAR, a subset of the C11memory model that admits relaxed and release-acquire accesses, but disallows,so-called, load-buffering cycles. We develop a simple framework for specifyingabstract objects that precisely characterises the observability guarantees ofabstract method calls. We show how this framework can be integrated with anoperational semantics that enables verification of client programs that executeabstract method calls from a library they use. Finally, we show howimplementations of such abstractions in RC11 RAR can be verified by developinga (contextual) refinement framework for abstract objects. Our framework,including the operational semantics, verification technique for client-libraryprograms, and simulation between abstract libraries and their implementations,has been mechanised in Isabelle/HOL.

Verifying C11-Style Weak Memory Libraries via Refinement