Cut-off theorems for the PV-model

For a PV thread T which accesses a set R of resources, each with a maximal capacity κ: R→ N, the PV-program Tn, where n copies of T are run in parallel, is deadlock free for all n if and only if TM is deadlock free where M is the sum of the capacities of the shared resources M= Σ r∈Rκ(r). This is a sharp bound: For all κ: R→ N and finite R there is a thread T using these resources such that TM has a deadlock, but Tn does not for n< M. Moreover, we prove a more general theorem for a set of different threads sharing resources R: There are no deadlocks in p= T1 | T2 | ⋯ | Tn if and only if there are no deadlocks in Ti1|Ti2|⋯|TiM for any M-element subset { i1, … , iM} ⊂ [1 : n]. For κ(r) ≡ 1 , Tn is serializable, i.e., all executions are equivalent to serial executions, for all n if and only if T2 is serializable. For general capacities, we define local obstructions to serializability—if no such obstruction exists, the program is serializable. There is no local obstruction to serializability in Tn for all n if and only if there is no local obstruction to serializability in TM for M= Σ r∈Rκ(r) + 1. The obstructions may be found using a deadlock algorithm in TM+1. There is a generalization to p= T1 | T2 | ⋯ | Tn: If there are no local obstructions to serializability in any of the sub programs, Ti1|Ti2|⋯|TiM, then p is serializable.