Efficient Abortable-locking Protocol for Multi-level NUMA Systems: Design and Correctness

The popularity of Non-Uniform Memory Access (NUMA) architectures has led to numerous locality-preserving hierarchical lock designs, such as HCLH, HMCS, and cohort locks. Locality-preserving locks trade fairness for higher throughput. Hence, some instances of acquisitions can incur long latencies, which can be intolerable for certain applications. Few locks allow a waiting thread to abort on a timeout. State-of-the-art abortable locks are not fully locality aware, introduce high overheads, and are unsuitable for frequent aborts. Enhancing locality-aware locks with lightweight timeout capability is critical for their adoption. In this article, we describe the design and implementation of the HMCS-T lock, a Hierarchical MCS (HMCS) lock variant that admits timeout. HMCS-T maintains the locality benefits of HMCS while ensuring aborts are lightweight. HMCS-T offers the progress guarantee missing in most abortable queuing locks. The resulting locking algorithm is complex and stateful. Proving the correctness of a complex, stateful synchronization algorithm is challenging. We prove the correctness of HMCS-T by first decomposing the problem via a novel technique that uses non-deterministic finite acceptors (NFAs). The decomposed problems become small enough to be mechanically model checked without a state-space explosion. Then, we generalize the correctness proof of any arbitrary lock configuration using a construction argument.