Tags:Asynchronous concurrent algorithms, Distributed runtime verification, Fault-tolerance and Linearizability
Abstract:
It was recently proposed an asynchronous, fault-tolerant, sound and complete algorithm for runtime verification of linearizability of concurrent algorithms. This solution relies on the snapshot abstraction in distributed computing. The fastest known snapshot algorithms use complex constructions, hard to implement, and the simplest ones provide large step complexity bounds or only weak termination guarantees. Thus, the snapshot-based verification algorithm is not completely satisfactory. In this paper, we propose an alternative solution, based on the collect abstraction, which can be optimally implemented in a simple manner. As a final result, we offer a simple and generic methodology that takes any presumably linearizable algorithm and produces a lightweight runtime verified linearizable version of it.
Towards Efficient Runtime Verified Linearizable Implementations