\section{Minimal configuration}
We need to answer the following questions to design an \mbox{HMCS-T}{} lock configuration that is sufficient to exercise all possible thread interleaving in any arrangement: 

\begin{itemize
\item How many threads are sufficient?
\item How many lock levels are sufficient?
\item How many lock acquisitions per participant are sufficient?
\end{itemize}


To answer these questions, we build  non-deterministic finite acceptors (NFAs) that capture the state transition for each shared variable.
The shared variables are the \texttt{status} and \texttt{next} fields of a \texttt{QNode}{} and the \texttt{tail pointer} variable.
The transitions of the status flag of a  root-level \texttt{QNode}{} are different from the transitions of the status field of a non-root-level \texttt{QNode}{}.
Figure~\ref{fig:NFAStatusOneLevel} and Figure~\ref{fig:NFAStatusNonRootLevel}, respectively, show the  NFA for the \texttt{status} field of a root-level and a non-root-level \texttt{QNode}{}.
Figure~\ref{fig:NFANextOneLevel} shows the NFA for the \texttt{next} field of any \texttt{QNode}{}.
The \texttt{tail pointer}  variable can be either \texttt{null}{} or non-\texttt{null}{}, and it is less interesting in designing the \mbox{HMCS-T}{} verification configurations.
Appendix~\ref{appx:NFARoot},~\ref{appx:NFANonRoot}, and~\ref{appx:NFANext} describe the transition associated with every edge shown in Figure~\ref{fig:NFAStatusOneLevel},~\ref{fig:NFAStatusNonRootLevel}, and~\ref{fig:NFANextOneLevel}, respectively. 



Node labels in Figure~\ref{fig:NFAStatusOneLevel}-\ref{fig:NFAStatusNonRootLevel} represent the field values in those states, and the subscripts distinguish the same values that bear different meanings in different contexts.
Solid black edges represent the actions taken by a thread $t${} owning the \texttt{QNode}{} under scrutiny.
Dotted blue edges represent the actions taken by a predecessor $p${} of $t${}.
Dotted red edges represent the actions taken by a successor $s${} of $t${}.
Thick black edges represent beginning of a new acquisition effort by a thread $t${} that owns the \texttt{QNode}{}.
Any subsequent path formed only of solid black edges represents a sequence of actions taken by a same thread of execution. 
Since the first operation in any acquisition is \texttt{SWAP}{}ing the status field, every new acquisition edge has a \wait[i] node as its sink.
Green color filled node(s) represent the state(s) where the lock contending thread $t${} has become the  owner of the lock at that level.

The NFA provides the following key insights:
\begin{enumerate
\item \textbf{Three participants:} 
Any edge can be traversed via a path starting at the start state that involves no more than a predecessor (dotted blue edge), self (black edge), and a successor (dotted red edge) in Figures~\ref{fig:NFAStatusOneLevel}, ~\ref{fig:NFAStatusNonRootLevel}, and~\ref{fig:NFANextOneLevel}.
Hence, three participants (a predecessor, self, and a successor) are sufficient to exercise all possible transitions that the status field of a \texttt{QNode}{} may go through. 

\item \textbf{Two rounds:}  
Any edge can be traversed via a path starting at the start state that involves no more than two ``begin acquisition'' (thick black line) edges.
Hence, two rounds of acquisitions on the same \texttt{QNode}{} are sufficient to exercise all possible transitions. This means, at least, one thread should try two acquisitions.
The other two threads can perform one acquisition each to exercise all interleaving of the third thread that performs two acquisitions.

\item \textbf{Three levels:}  
The \edge{C_1}{W_4}  in Figure~\ref{fig:NFAStatusNonRootLevel} demands that a thread $t_1$ to have acquired the lock at the current node \texttt{q} at level $l$ and abandoned at an ancestor level and a different thread  $t_2$, a peer of $t_1$ at a level $<l$, to have inherited the level $l$ lock from $t_1$.
Hence, there should,  at least, be two threads at level $l-1$, which can cause one of them (say $t_1$) to acquire locks at level $l-1$ and $l$ but timeout at level $l+1$ and eventually grant the locks at level $l-1$ and $l$ to another thread (say $t_2$). 
Three levels, parent, current, and children are sufficient to exercise all possible transitions in a non-root-level \texttt{QNode}{} .
\end{enumerate}


To elaborate on Property 1 and 2, we describe a few interesting transitions in  Figure~\ref{fig:NFAStatusOneLevel}.
The \edge{U_2}{U_3} needs $t${} to have a predecessor to reach \unlocked[2] and then a successor to cause impatience  during the release protocol to transition to \unlocked[3].
The \edge{W_3}{R_2} needs $t${} to have a predecessor to reach \unlocked[2] and then the second round of acquisition attempt by $t${} to reach \wait[3] and then a successor to make $t${} impatient in its release protocol to eventually make the successor update $t${}'s status to \recycled[2].  
The \edge{R_2}{U_1} and \edge{R_2}{A_1}  need at least two rounds of acquisitions by $t${} and a successor $s${} to reach \recycled[2]. The same successor $s${} can act as a predecessor for \edge{R_2}{U_1} transition. Similarly, $s${} can act as a predecessor leading to a timeout to cause \edge{R_2}{A_1} transition.


\begin{comment}
Figure~\ref{fig:NFANextOneLevel} shows the state transition diagram for the \texttt{next} field of a \texttt{QNode}{}.
We defer the description of each transition to Appendix~\ref{appx:NFANext}.
Similar to Figure~\ref{fig:NFAStatusOneLevel}, there are no cycles (live lock) without user intervention; every node has at least a path to an accept state without going through a ``new acquisition'' edge implying bounded steps to end the protocol (acquire and release or abandon); every state that is sink of a new acquisition edge has a non-timeout path to an acceptance state implying starvation freedom; three participants (a predecessor, self, and a successor) are sufficient to exercise all possible transitions (e.g., \edge{S_1}{P_1}); two acquisitions by at least one thread is sufficient to transition through all possible edges and the other two threads (predecessor and successor) can perform one acquisition.
\end{comment}





\begin{figure}[t]
\centering
\begin{minipage}{.38\linewidth}
\includegraphics[width=\linewidth]{images/SpinRoot.pdf}
\caption{{Model checking configuration to exercise all possible interleaving for a thread at root level.}}
\label{fig:SpinRoot}
\end{minipage}
\hspace{1ex}
\centering
\begin{minipage}{.58\linewidth}
\includegraphics[width=\linewidth]{images/SpinNonRoot.pdf}
\caption{{Model checking configuration to exercise all possible interleaving for a thread at a non-root level.}}
\label{fig:SpinNonRoot}
\end{minipage}
\end{figure}

\begin{comment}
The NFA for the status flag of non-root \texttt{QNode}{} is more complicated, as shown in Figure~\ref{fig:NFAStatusNonRootLevel}.
The details of each transition are deferred to Apendex~\ref{appx:NFANonRoot}.
It is apparent, however, from Figure~\ref{fig:NFAStatusNonRootLevel} that similar to the root-level \texttt{status} field, the observations about live-lock freedom, deadlock  freedom, starvation freedom, abounded steps to release and timeout hold good for the non-root level NFA as well. The states \cohort[1] and \texttt{V}$_1$ are analogous to the lock ownership state \unlocked[1] in Figure~\ref{fig:NFAStatusOneLevel}.
Also, the need for three participants at a non-root level $l$ and two rounds of acquisitions for the \texttt{QNode}{} under observation still hold good.
However, a non-root level demands more than one level in the tree to exercise all possible transitions. 
For example, the \edge{C_1}{W_4} demands that a thread $t_1$ to have acquired the lock at the current node \texttt{q} at level $l$ and abandoned at an ancestor level and a different thread  $t_2$ a peer of $t_1$ at a level $<l$ to have inherited the level $l$ from $t_1$.
This demands at least three levels: a level $l$ under observation, its parent level $l+1$ and its child level $l-1$.
\end{comment}

NFAs, unfortunately, do not capture an important safety property---mutual exclusion.
An NFA is ill-defined if the ownership of a \texttt{QNode}{} is not exclusive, which can happen if another thread belonging to the same domain starts modifying a shared \texttt{QNode}{}. 
To check the mutual exclusion property, we exercise all possible thread interleaving in a model checking phase.

To exercise all states of the root-level lock we use a thread configuration shown in Figure~\ref{fig:SpinRoot}. 
The thread under scrutiny will be subjected to two rounds of acquisitions and the other two threads perform one round of acquisition each.
Since model checking will exercise all interleaving, the timeout value is immaterial.

To exercise all states of the non-root-level lock, we use a thread configuration shown in Figure~\ref{fig:SpinNonRoot}. 
There are two threads at level $1$, which can causes one of them (say $t_1$) to acquire the locks at level $1$ and $2$ but timeout at level $3$ and eventually grant the ownership of locks at level $1$ and $2$ to another thread (say $t_2$).
The presence of two threads at level $1$, also causes the common ancestor $X$, the \texttt{QNode}{} under scrutiny at level $l$, to go through the necessary two rounds of acquisitions. 
The other two participants---a successor $s${}, and a predecessor $p${} at level $l$--- perform only one round of acquisition each.
The model checking does not require $s${} and  $p${}  to begin the protocol at the leaf level, which avoids exercising some non-interesting interleavings.
Hence, we set up $s${} and $p${} without children.
Note that such arrangement is for model checking only; the \mbox{HMCS-T}{} lock admits new acquisitions starting at the leaf level only.
In total, we need 4 threads, 2 at level $1$ sharing the parent  $X$, and 3 (of which one would have ascended from $1$) at level $2$.
The behavior at level $3$ will be non-deterministic---either a successful acquisition or  abandonment to simulate all possible transitions in $X$.
Non-deterministic behavior is easy to exhibit in Spin~\cite{Holzmann:1997:MCS:260897.260902}. 

The verification checks for the assertion that two threads are never simultaneously in the critical section for the configuration in Figure~\ref{fig:SpinRoot}.
This assertion ensures that the root-level lock ensures mutual exclusion to the critical section if each \texttt{QNode}{} is accessed by  descendent threads in a mutually exclusive manner.
For the configuration in Figure~\ref{fig:SpinNonRoot}, we check that $t_1$ and $t_2$ never simultaneously acquire the level $l-1$ lock and no two threads ever simultaneously acquire the level $l$ lock.
This assertion ensures that a non-root-level lock ensures mutual exclusion to its next level if each \texttt{QNode}{} is accessed by descendent threads in a mutually exclusive manner.



Additionally, the NFAs in Figure~\ref{fig:NFAStatusOneLevel},~\ref{fig:NFAStatusNonRootLevel}, and~\ref{fig:NFANextOneLevel} provide insights into the following key properties:
\begin{enumerate
\item \textbf{Livelock Freedom:} There does not exist any cycle without at least one ``begin new acquisition'' edge. Hence, there cannot be perpetual state transitions (live lock) without user opting to start another round of lock acquisition.
\item \textbf{Starvation Freedom:} Every \wait[i] node (beginning of a new acquisition) has a path to the lock owning state (\unlocked[1] in Figure~\ref{fig:NFAStatusOneLevel} and \texttt{V}$_1$ and \cohort[1] in Figure~\ref{fig:NFAStatusNonRootLevel}), if it is not allowed to traverse any \emph{timeout} edge. This implies, every thread that starts its acquisition process and does not timeout, eventually acquires the lock.
The \texttt{next} field does not decide the lock ownership and hence ignored.
\item \textbf{Bounded Steps to Release:} There exists a finite-length solid-black edge path from lock owner state to another node $\eta$ such that a new acquisition (thick black edge) effort can begin at $\eta$.
 This implies, 1) an acquired lock can be released in a bounded number of steps by the lock owner and 2) once the lock is released, the \texttt{QNode}{} can be subjected to another acquisition attempt immediately. 
\item \textbf{Bounded Steps on Timeout:} Every node that is \emph{not}  source node of a new acquisition edge (thick black edge) has a solid-black edge path to the source of a timeout edge.
This implies that in any state after starting an acquisition process if a timeout occurs, $t${} can abandon the protocol in a bounded number of steps.
Source nodes of new acquisition edges are precluded because one cannot start an abandonment without having started an acquisition.
\item \textbf{Deadlock Freedom:} Every node has a path (there is an $\epsilon$ path to itself) formed out of solid-black edges to a node from where a new acquisition can begin.
\end{enumerate}


\section{Correctness of \hmcst{n}}

To establish the mutual exclusion guarantee of \hmcst{n}, we take the following steps:

\begin{lemma}\emph{\textbf{(Root level lock ensures mutual exclusion:)}}  A root-level lock ensures mutual exclusion if every root-level \texttt{QNode}{} is owned by a descendent in a mutually exclusive manner.
\label{lem:root}
\end{lemma}

\begin{proof}
Verified by model checking a root-level lock with the configuration shown in Figure~\ref{fig:SpinRoot}.
\end{proof}

\begin{lemma} \emph{\textbf{(Non-root level lock ensures mutual exclusion:)}} A non-root-level lock admits mutually exclusive access to the next level lock if every \texttt{QNode}{} at that level is owned by a single descendent at a time.
\label{lem:nonroot}
\end{lemma}
\begin{proof}
Verified by model checking a non-root-level in an \mbox{HMCS-T}{} lock with the configuration shown in Figure~\ref{fig:SpinNonRoot}.
\end{proof}

\begin{fact}[Exclusive ownership of leaf-level node:] Every \texttt{QNode}{} at leaf level is owned by a unique thread, and the ownership is never shared with any other thread.
\label{axiom:exclusiveleaf}
\end{fact}


\begin{theorem} [\mbox{HMCS-T}{} ensures mutual exclusion:] \hmcst{n} ensures mutual exclusion to the critical section it protects.
\label{thm:hmcsnExl}
\end{theorem}
\begin{proof}
  \hmcst{n} is composed of a root-level lock and $n-1$ non-root-level locks.  
Each level ensures mutual exclusion to the level above as long the threads from descendent levels (if any) accesses the shared \texttt{QNode}{} at the current level in a mutually exclusive manner. 
Assume \hmcst{n} does not ensure mutual exclusion to the critical section. This means two threads $t_1$ and $t_2$ can  simultaneously be in the critical section.
Both $t_1$ and $t_2$ are either 1) peers at level $n$ and hence compete for the root-level lock at level $n$, or 2)  belong to the same domain and hence compete for a non-root-level lock at  a level $l < n$.

If $t_1$ and $t_2$  are peers at level $n$, they will enqueue, two different \texttt{QNode}s{} and compete for the root-level lock and by Lemma~\ref{lem:root} only one of them can be in the critical section at a time.
Hence, $t_1$ and $t_2$ cannot be peers at the root-level.

Now, $t_1$ and $t_2$ are either peers at level $n-1$ or belong to the same domain at level $l' < n-1$.
If $t_1$ and $t_2$  are peers at level $n-1$, they will enqueue two different \texttt{QNode}s{} and compete for the non-root-level lock at level $n-1$ and by Lemma~\ref{lem:nonroot} only one of them can own the level $n-1$ lock ensuring the mutual exclusion between them.
Hence, $t_1$ and $t_2$ cannot be peers at level $n-1$.

Since \hmcst{n} has only a finite number of levels, by extrapolation, $t_1$ and $t_2$ are either peers at the leaf level or  share the same \texttt{QNode}{} at the leaf level.
If $t_1$ and $t_2$  are peers at the leaf level, they will enqueue two different \texttt{QNode}s{} and compete for the non-root-level lock at the leaf level and by Fact~\ref{lem:nonroot} only one of them can own the leaf level lock ensuring the mutual exclusion between them.
Hence, $t_1$ and $t_2$ must be sharing the same \texttt{QNode}{} at the leaf level. 
By Lemma~\ref{axiom:exclusiveleaf}, no two threads can share the same \texttt{QNode}{} at the leaf level, hence $t_1 = t_2$, which contradicts the assumption.

Hence, only one thread can be in the critical section in \hmcst{n}.
\end{proof}

The desirable attributes---starvation freedom, live-lock and deadlock freedom, bounded steps to release or time out---for a given level of lock do not translate to the same for an entire \hmcst{n} lock.
To establish these properties for \hmcs{n}, we make the following claims:
\begin{fact}[Ordered acquisition:] Any thread in \mbox{HMCS-T}{} lock of $n$ levels obeys a monotonically increasing order in acquisition effort starting from level $1$ and ending at level $l \le n$.
\label{axiom:acquisition}
\end{fact}
\sloppy
\begin{fact}[Ordered release and abandonment:] \mbox{HMCS-T}{} lock of $n$ levels obeys a bitonically ordered release and abandonment---monotonically increasing in level followed by monotonically decreasing in level. 
A thread owning  locks  $1<=$ \texttt{prefix:suffix} $ \le n$ either releases the \texttt{suffix} locks before releasing the ownership of remaining \texttt{prefix} locks or delegates the same responsibility to  another thread that becomes the owner of entire \texttt{prefix:suffix} locks. 
\label{axiom:release}
\end{fact}



\begin{theorem} \hmcst{n} guarantees live-lock freedom, deadlock freedom, starvation freedom, bounded steps to release, and bounded steps on timeout.
\end{theorem}

\begin{proof}
\hmcst{n} is composed of a root-level lock and $n-1$ non-root-level locks.  
By Fact~\ref{axiom:acquisition} and~\ref{axiom:release}, every thread follows an ordered acquisition and release  or abandonment protocol.
Hence, each thread goes through a finite number of levels in any process.
At each level, root or non-root, the NFA that a thread is subjected to for its \texttt{QNode}{}, ensures live-lock freedom, deadlock freedom, starvation freedom, bounded steps to release, and bounded steps on timeout if the \texttt{QNode}{} is accessed mutually exclusively by descendants that share the same ancestor \texttt{QNode}{}.
By Theorem~\ref{thm:hmcsnExl}, each \texttt{QNode}{} is owned by a descendent thread in a mutually exclusive manner. 
Hence, by construction \hmcst{n} ensures live-lock freedom, deadlock freedom, starvation freedom, bounded steps to release, and bounded steps on timeout. 
\end{proof}


