12 citations · 13 across the 6 of their papers we have counts for
4 papers · 1 filter
Abstraction for Crash-Resilient Objects (Extended Version)
Artem Khyzha, Ori Lahav
We study abstraction for crash-resilient concurrent objects using non-volatile memory (NVM). We develop a library correctness criterion that is sound for ensuring contextual refine…
Taming x86-TSO Persistency (Extended Version)
Artem Khyzha, Ori Lahav
We study the formal semantics of non-volatile memory in the x86-TSO architecture. We show that while the explicit persist operations in the recent model of Raad et al. from POPL'20…
Proving Linearizability Using Partial Orders (Extended Version)
Artem Khyzha, Mike Dodds, Alexey Gotsman +1
Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization…
A Generic Logic for Proving Linearizability (Extended Version)
Artem Khyzha, Alexey Gotsman, Matthew Parkinson
Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms, and recent years have seen a number of proposals of program logics for proving…