55 citations · 90 across the 9 of their papers we have counts for
10 papers
Extending the C/C++ Memory Model with Inline Assembly
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis +1
Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive…
Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour
Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis +2
Memory persistency models provide a foundation for persistent programming by specifying which (and when) writes to non-volatile memory (NVM) become persistent. Memory persistency m…
Specifying and Verifying Persistent Libraries
Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of t…
The Path to Durable Linearizability
Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a po…
Making Weak Memory Models Fair
Ori Lahav, Egor Namakonov, Jonas Oberhauser +2
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the…
The Decidability of Verification under Promising 2.0
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole +2
In PLDI'20, Lee et al. introduced the \emph{promising } semantics PS 2.0 of the C++ concurrency that captures most of the common program transformations while satisfying the DRF gu…