NESTid Seminar: Preserving Hyperproperties when Using Concurrent Objects

Thursday 26 Jan 2023, 16:00 → 17:00 UTC

Abstract: 

Linearizability, a consistency condition for concurrent objects, is known to preserve trace properties. This suffices for modular usage of concurrent objects in applications, deriving their safety properties from the abstract object they implement. However, other desirable properties, like average complexity and information leakage, are not trace properties. These *hyperproperties* are not preserved by linearizable concurrent objects, especially when randomization is used. This talk will discuss formal ways to specify concurrent objects that preserve hyperproperties and their relation with verification methods like forward / backward simulation. We will show that certain concurrent objects cannot satisfy such specifications, and describe ways to mitigate these limitations.

This is a joint work with Constantin Enea and Jennifer Welch.

Speaker: Hagit Attiya (Technion, Israel)

ZOOM link:
 https://durhamuniversity.zoom.us/j/95517607611?pwd=dFVwSVRBRmVUQXIrWTBXZ3FYV2xKZz09

More info: https://nestid.webspace.durham.ac.uk/nestid-seminars/