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/

Zendy Plus

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

Zendy Tools

Zendy Open

Multiprocess systems, including grid systems, multiprocessors and multicorecomputers, incorporate a variety of specialized hardware and softwaremechanisms, which speed computation, but result in complex memory behavior. Asa consequence, the possible outcomes of a concurrent program can be unexpected.A memory consistency model is a description of the behaviour of such a system.Abstract memory consistency models aim to capture the concrete implementationsand architectures. Therefore, formal specification of the implementation orarchitecture is necessary, and proofs of correspondence between the abstractand the concrete models are required.  This paper provides a case study of this process. We specify a new model,partition consistency, that generalizes many existing consistency models. Aconcrete message-passing network model is also specified. Implementations ofpartition consistency on this network model are then presented and provedcorrect. A middle level of abstraction is utilized to facilitate the proofs.All three levels of abstraction are specified using the same framework. Thepaper aims to illustrate a general methodology and techniques for specifyingmemory consistency models and proving the correctness of their implementations.

Partition Consistency: A Case Study in Modeling Systems with Weak Memory Consistency and Proving Correctness of their Implementations