AbstractInnite wait anomalies associated with a barrier rendezvous model (e.g., Ada) can be divided into two classes: stal ls and dead locks. Although precise static deadlock detection is NP-hard, we present two polynomial time algorithms which operate on a statically derivable program representation, the sync graph, to certify a useful class of programs free of deadlocks. We identify three conditions local to any deadlocked tasks, and a fourth global condition on all tasks, which must occur in the sync graph of any program which can deadlock. Again, exact checking of the local conditions is NP-hard; the algorithms check them using conservative approximations. Certifying stall freedom is intractable for programs with conditional branching, including loops. We give program transforms which may help alleviate this diculty.
RightsThis Item is protected by copyright and/or related rights.You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use.For other uses you need to obtain permission from the rights-holder(s).