12 citations · 13 across the 6 of their papers we have counts for
7 papers
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 Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea +4
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any sy…
Privatization-Safe Transactional Memories (Extended Version)
Artem Khyzha, Hagit Attiya, Alexey Gotsman
Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often wou…
Safe Privatization in Transactional Memory
Artem Khyzha, Hagit Attiya, Alexey Gotsman +1
Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often wou…
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…