Correctness of Hierarchical MCS Locks with Timeout

TL;DR

This paper provides a formal correctness proof for the complex Hierarchical MCS locks with Timeout (HMCS-T) used in multi-level NUMA systems, employing model checking and logical reasoning to ensure safety properties.

Contribution

It introduces a formal correctness proof for HMCS-T, a complex, stateful, hierarchical lock protocol with timeout features, using model checking and logical analysis.

Findings

Correctness of HMCS-T lock components verified via model checking.

Minimal configurations necessary for safety properties identified.

Logical proof of overall HMCS-T correctness established.

Abstract

This manuscript serves as a correctness proof of the Hierarchical MCS locks with Timeout (HMCS-T) described in our paper titled "An Efficient Abortable-locking Protocol for Multi-level NUMA Systems" appearing in the proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. HMCS-T is a very involved protocol. The system is stateful; the values of prior acquisition efforts affect the subsequent acquisition efforts. Also, the status of successors, predecessors, ancestors, and descendants affect steps followed by the protocol. The ability to make the protocol fully non-blocking leads to modifications to the \texttt{next} field, which causes deviation from the original MCS lock protocol both in acquisition and release. At several places, unconditional field updates are replaced with SWAP or CAS operations. We follow a multi-step approach to prove the correctness of HMCS-T. To demonstrate the correctness of the HMCS-T lock, we use the Spin model checking. Model checking causes a combinatorial explosion even to simulate a handful of threads. First, we understand the minimal, sufficient configurations necessary to prove safety properties of a single level of lock in the tree. We construct HMCS-T locks that represent these configurations. We model check these configurations, which proves the correctness of components of an HMCS-T lock. Finally, building upon these facts, we argue logically for the correctness of HMCS-T<n>.