Recoverable Lock-Free Locks

TL;DR

This paper introduces a novel transformation that converts lock-based implementations into recoverable, lock-free versions, supporting nested locks and ensuring correctness and recoverability.

Contribution

It presents the first transformation that achieves both lock-freedom and recoverability from lock-based code, supporting nested locks.

Findings

Provides a recoverable, lock-free substitution for lock acquire and release.

Supports nested locks without compromising correctness.

Ensures recoverability in lock-free transformations.

Abstract

This paper presents the first transformation that introduces both lock-freedom and recoverability. Our transformation starts with a lock-based implementation, and provides a recoverable, lock-free substitution to lock acquire and lock release operations. The transformation supports nested locks for generality and ensures recoverability without jeopardising the correctness of the lock-based implementation it is applied on.