Cut-off theorems for the PV-model

Lisbeth Fajstrup*

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review


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.
Original languageEnglish
JournalFormal Methods in System Design
Issue number1-3
Pages (from-to)21-43
Number of pages23
Publication statusPublished - 15 Jun 2022

Bibliographical note

Publisher Copyright:
© 2022, The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature.


Dive into the research topics of 'Cut-off theorems for the PV-model'. Together they form a unique fingerprint.

Cite this