Theory Challenge3
chapter ‹Array-Based Queuing Lock›
section ‹Challenge›
text_raw ‹{\upshape
Array-Based Queuing Lock (ABQL)
is a variation of the Ticket Lock algorithm with a bounded number
of concurrent threads and improved scalability due to better cache
behaviour.
%(\url{https://en.wikipedia.org/wiki/Array_Based_Queuing_Locks})
We assume that there are \texttt{N} threads and we
allocate a shared Boolean array \texttt{pass[]} of length \texttt{N}.
We also allocate a shared integer value \texttt{next}.
In practice, \texttt{next} is an unsigned bounded
integer that wraps to 0 on overflow, and
we assume that the maximal value of \texttt{next} is
of the form $k\mathtt{N} - 1$.
Finally, we assume at our disposal
an atomic \texttt{fetch\_and\_add} instruction,
such that \texttt{fetch\_and\_add(next,1)} increments the value
of \texttt{next} by 1 and returns the original value of \texttt{next}.
The elements of \texttt{pass[]} are spinlocks, assigned
individually to each thread in the waiting queue.
Initially, each element of \texttt{pass[]} is set to
\texttt{false}, except \texttt{pass[0]} which is set to
\texttt{true}, allowing the first coming thread to acquire
the lock.
Variable \texttt{next} contains the number of the first available
place in the waiting queue and is initialized to 0.
Here is an implementation of the locking algorithm in pseudocode:
\begin{lstlisting}[language=C,morekeywords={procedure,function,end,to,in,var,then,not,mod}]
procedure abql_init()
for i = 1 to N - 1 do
pass[i] := false
end-for
pass[0] := true
next := 0
end-procedure
function abql_acquire()
var my_ticket := fetch_and_add(next,1) mod N
while not pass[my_ticket] do
end-while
return my_ticket
end-function
procedure abql_release(my_ticket)
pass[my_ticket] := false
pass[(my_ticket + 1) mod N] := true
end-procedure
\end{lstlisting}
Each thread that acquires the lock must eventually release it
by calling \texttt{abql\_release(my\_ticket)}, where \texttt{my\_ticket}
is the return value of the earlier call of \texttt{abql\_acquire()}.
We assume that no thread tries to re-acquire the lock while already
holding it, neither it attempts to release the lock which it does not possess.
Notice that the first
assignment in \texttt{abql\_release()} can be moved at the end
of \texttt{abql\_acquire()}.
\bigskip
\noindent\textbf{Verification task~1.}~Verify
the safety of ABQL
under the given assumptions. Specifically, you should prove that no two
threads can hold the lock at any given time.
\bigskip
\noindent\textbf{Verification task~2.}~Verify
the fairness, namely that the threads acquire the lock
in order of request.
\bigskip
\noindent\textbf{Verification task~3.}~Verify
the liveness under a fair scheduler, namely that
each thread requesting the lock will eventually acquire it.
\bigskip
You have liberty of adapting the implementation and specification
of the concurrent setting as best suited for your verification tool.
In particular, solutions with a fixed value of \texttt{N} are acceptable.
We expect, however, that the general idea of the algorithm and
the non-deterministic behaviour of the scheduler shall be preserved.
}
\clearpage
›
section ‹Solution›
theory Challenge3
imports "lib/VTcomp" "lib/DF_System"
begin
text ‹The Isabelle Refinement Framework does not support concurrency.
However, Isabelle is a general purpose theorem prover, thus we can model
the problem as a state machine, and prove properties over runs.
For this polished solution, we make use of a small library for
transition systems and simulations: @{theory VerifyThis2018.DF_System}.
Note, however, that our definitions are still quite ad-hoc,
and there are lots of opportunities to define libraries that make similar
proofs simpler and more canonical.
We approach the final ABQL with three refinement steps:
▸ We model a ticket lock with unbounded counters, and prove safety, fairness, and liveness.
▸ We bound the counters by ‹mod N› and ‹mod (k*N) respectively›
▸ We implement the current counter by an array,
yielding exactly the algorithm described in the challenge.
With a simulation argument, we transfer the properties of the abstract
system over the refinements.
The final theorems proving safety, fairness, and liveness can be found at
the end of this chapter, in Subsection~\ref{sec:main_theorems}.
›
subsection ‹General Definitions›
text ‹We fix a positive number ‹N› of threads›
consts N :: nat
specification (N) N_not0[simp, intro!]: "N≠0" by auto
lemma N_gt0[simp, intro!]: "0<N" by (cases N) auto
text ‹A thread's state, representing the sequence points in the given algorithm.
This will not change over the refinements.›