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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Linearizability is a standard correctness criterion for concurrentalgorithms, typically proved by establishing the algorithms' linearizationpoints (LP). However, LPs often hinder abstraction, and for some algorithmssuch as the timestamped stack, it is unclear how to even identify their LPs. Inthis paper, we show how to develop declarative proofs of linearizability byforegoing LPs and instead employing axiomatization of so-called visibilityrelations. While visibility relations have been considered before for thetimestamped stack, our study is the first to show how to derive theaxiomatization systematically and intuitively from the sequential specificationof the stack. In addition to the visibility relation, a novel separabilityrelation emerges to generalize real-time precedence of procedure invocation.The visibility and separability relations have natural definitions for thetimestamped stack, and enable a novel proof that reduces the algorithm to asimplified form where the timestamps are generated atomically.

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack: Extended Version