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

Linearisability has become the standard correctness criterion for concurrentdata structures, ensuring that every history of invocations and responses ofconcurrent operations has a matching sequential history. Existing proofs oflinearisability require one to identify so-called linearisation points withinthe operations under consideration, which are atomic statements whose executioncauses the effect of an operation to be felt. However, identification oflinearisation points is a non-trivial task, requiring a high degree ofexpertise. For sophisticated algorithms such as Heller et al's lazy set, iteven is possible for an operation to be linearised by the concurrent executionof a statement outside the operation being verified. This paper proposes analternative method for verifying linearisability that does not requireidentification of linearisation points. Instead, using an interval-based logic,we show that every behaviour of each concrete operation over any interval is apossible behaviour of a corresponding abstraction that executes withcoarse-grained atomicity. This approach is applied to Heller et al's lazy setto show that verification of linearisability is possible without having toconsider linearisation points within the program code.

Simplifying proofs of linearisability using layers of abstraction