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

Linearizability, the traditional correctness condition for concurrent datastructures is considered insufficient for the non-volatile shared memory modelwhere processes recover following a crash. For this crash-recovery sharedmemory model, strict-linearizability is considered appropriate since, unlikelinearizability, it ensures operations that crash take effect prior to thecrash or not at all.  This work formalizes and answers the question of whether an implementation ofa data type derived for the crash-stop shared memory model is alsostrict-linearizable in the crash-recovery model. This work presents a rigorousstudy to prove how helping mechanisms, typically employed by non-blockingimplementations, is the algorithmic abstraction that delineates linearizabilityfrom strict-linearizability. Our first contribution formalizes thecrash-recovery model and how explicit process crashes and recovery introducesfurther dimensionalities over the standard crash-stop shared memory model. Wemake the following technical contributions: (i) we prove thatstrict-linearizability is independent of any known help definition; (ii) wethen present a natural definition of help-freedom to prove that anyobstruction-free, linearizable and help-free implementation of a total objecttype is also strict-linearizable; (iii) finally, we prove that for a largeclass of object types, a non-blocking strict-linearizable implementation cannothave helping. Viewed holistically, this work provides the first precisecharacterization of the intricacies in applying a concurrent implementationdesigned for the crash-stop model to the crash-recovery model, and vice-versa.

Separation and Equivalence results for the Crash-stop and Crash-recovery Shared Memory Models