26 citations · 27 across the 3 of their papers we have counts for
6 papers · 1 filter
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…
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…
Reconciling Event Structures with Modern Multiprocessors
Evgenii Moiseenko, Anton Podkopaev, Ori Lahav +2
Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem. Although it has been shown to have important…
Bridging the Gap between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consi…