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

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

It has been observed that linearizability, the prevalent consistencycondition for implementing concurrent objects, does not preserve someprobability distributions. A stronger condition, called strong linearizabilityhas been proposed, but its study has been somewhat ad-hoc. This paperinvestigates strong linearizability by casting it in the context ofobservational refinement of objects. We present a strengthening ofobservational refinement, which generalizes strong linearizability, obtainingseveral important implications.  When a concrete concurrent object refining another, more abstract object -often sequential - the correctness of a program employing the concrete objectcan be verified by considering its behaviors when using the more abstractobject. This means that trace properties of a program using the concrete objectcan be proved by considering the program with the abstract object. This,however, does not hold for hyperproperties, including many security propertiesand probability distributions of events.  We define strong observational refinement, a strengthening of refinement thatpreserves hyperproperties, and prove that it is equivalent to the existence offorward simulations. We show that strong observational refinement generalizesstrong linearizability. This implies that strong linearizability is alsoequivalent to forward simulation, and shows that strongly linearizableimplementations can be composed both horizontally (i.e., locality) andvertically (i.e., with instantiation).  For situations where strongly linearizable implementations do not exist (orare less efficient), we argue that reasoning about hyperproperties of programscan be simplified by strong observational refinement of abstract objects thatare not necessarily sequential.

Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs that Use Concurrent Objects