Brief Announcement: Detectable Sequential Specifications for Recoverable Shared Objects

The recent commercial release of persistent main memory by Intel has sparked intense interest in recoverable concurrent objects. Specifying and implementing such objects is technically challenging on current generation hardware precisely because the top layers of the memory hierarchy (CPU registers and cache) remain volatile, which causes application threads to lose critical execution state during a failure. Friedman, Herlihy, Marathe, and Petrank (DISC'17) recently proposed that this difficulty can be alleviated by making the recoverable objects detectable, meaning that during recovery, they can resolve the status of an operation that was interrupted by a failure. In this paper, we formalize this important concept using a detectable sequential specification (DSS), which augments an object's interface with auxiliary methods that threads use to first declare their need for detectability, and then perform detection if needed after a failure. Compared to prior work on this topic, our DSS-based approach is less reliant on assumptions regarding the system, and more flexible in the sense that it allows applications to request detectability on demand. As a proof of concept, we present a detectable recoverable lock-free queue algorithm and evaluate its performance on a multiprocessor equipped with Intel Optane persistent memory. Our queue outperforms the detectable log queue of Friedman, Herlihy, Marthe, and Petrank (PPoPP'18) by up to 1.7x.