Cut-off Theorems for the PV-model

TL;DR

This paper establishes precise bounds for deadlock and serializability in parallel PV-model threads, showing that analyzing a finite subset of resources suffices to determine these properties for any number of parallel threads.

Contribution

It introduces sharp cut-off theorems for deadlock and serializability in PV-model parallel programs, providing practical criteria for their analysis.

Findings

Deadlock freedom in T^n for all n iff T^M is deadlock free, with M as sum of resource capacities.

Serializability in T^n for all n iff T^2 is serializable, for capacity 1.

Existence of local obstructions to serializability characterized by a finite subset of subprograms.

Abstract

We prove cut-off results for deadlocks and serializability of a $PV$-thread $T$ run in parallel with itself: For a $PV$ thread $T$ which accesses a set $\mathcal{R}$ of resources, each with a maximal capacity $\kappa:\mathcal{R}\to\mathbb{N}$, the PV-program $T^n$, where $n$ copies of $T$ are run in parallel, is deadlock free for all $n$ if and only if $T^M$ is deadlock free where $M=\Sigma_{r\in\mathcal{R}}\kappa(r)$. This is a sharp bound: For all $\kappa:\mathcal{R}\to\mathbb{N}$ and finite $\mathcal{R}$ there is a thread $T$ using these resources such that $T^M$ has a deadlock, but $T^n$ does not for $n<M$. Moreover, we prove a more general theorem: There are no deadlocks in $p=T1|T2|\cdots |Tn$ if and only if there are no deadlocks in $T_{i_1}|T_{i_2}|\cdots |T_{i_M}$ for any subset $\{i_1,\ldots,i_M\}\subset [1:n]$. For $\kappa(r)\equiv 1$, $T^n$ is serializable for all $n$ if and only if $T^2$ is serializable. For general capacities, we define a local obstruction to serializability. There is no local obstruction to serializability in $T^n$ for all $n$ if and only if there is no local obstruction to serializability in $T^M$ for $M=\Sigma_{r\in\mathcal{R}}\kappa(r)+1$. The obstructions may be found using a deadlock algorithm in $T^{M+1}$. These serializability results also have a generalization: If there are no local obstructions to serializability in any of the $M$-dimensional sub programs, $T_{i_1}|T_{i_2}|\cdots |T_{i_M}$, then $p$ is serializable.