papers/hanzo-formal-verification/sections/06-compute-scheduler-verification.tex

\section{Compute Scheduler Verification}

\label{sec:compute}
% ============================================================================

The Hanzo compute scheduler~\cite{hanzoaci} allocates GPU resources to
inference and training jobs.

\subsection{Resource Allocation Fairness}

\begin{definition}[Weighted Fair Queuing]
For $n$ organizations with weights $w_1, \ldots, w_n$ and a pool of $G$ GPUs,
weighted fair allocation assigns:
\begin{equation}
g_i = \left\lfloor G \cdot \frac{w_i}{\sum_j w_j} \right\rfloor
\end{equation}
GPUs to organization $i$, with remaining GPUs assigned by weight-priority.
\end{definition}

\begin{theorem}[Allocation Fairness]
The scheduler's allocation satisfies:
\begin{equation}
\left| \frac{g_i}{G} - \frac{w_i}{\sum_j w_j} \right| < \frac{1}{G}
\quad \forall i.
\end{equation}
No organization receives more than $1/G$ deviation from its fair share.
\end{theorem}

\subsection{Deadlock Freedom}

\begin{theorem}[Deadlock Freedom]
The compute scheduler with priority-based preemption is deadlock-free: for
any finite set of jobs, every job either completes or is explicitly rejected
within bounded time. No circular wait condition can occur because:
\begin{enumerate}[leftmargin=1.4em]
    \item Resources (GPUs) are preemptible by higher-priority jobs.
    \item Jobs do not hold resources while waiting for other resources.
    \item A total order on job priorities breaks symmetry.
\end{enumerate}
\end{theorem}

\subsection{Bug Found: Priority Inversion}

A high-priority realtime inference job could be blocked by a low-priority
batch training job occupying the last available GPU, with medium-priority jobs
preventing the batch job from completing. The fix implements priority
inheritance: the batch job temporarily inherits the high-priority job's
priority, ensuring it completes and releases the GPU.

% ============================================================================