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

Proving the correctness of programs written for multiple processors is achallenging problem, due in no small part to the weaker memory guaranteesafforded by most modern architectures. In particular, the existence of storebuffers means that the programmer can no longer assume that writes to differentlocations become visible to all processors in the same order. However, allpractical architectures do provide a collection of weaker guarantees aboutmemory consistency across processors, which enable the programmer to writeprovably correct programs in spite of a lack of full sequential consistency. Inthis work, we present a mechanization in the ACL2 theorem prover of anaxiomatic weak memory model (introduced by Alglave et al.). In the process, weprovide a new proof of an established theorem involving these axioms.

An ACL2 Mechanization of an Axiomatic Framework for Weak Memory