AbstractWe describe the representation of Ada programs containing the select and accept-do constructs, for use in safe and accurate static detection of deadlock in polynomial time. We describe a sync hypergraph program representation, which encompasses remote procedures including synchronization, conditional entries and entry calls, and else clauses and timeouts. We present a corresponding execution model for the sync hypergraph abstraction of Ada programs, and give constraints on valid deadlock cycles based on this execution model. We give full details of a deadlock detection algorithm, including lattice frameworks for deadlock cycle detection and proof of worst-case polynomial time bounds for convergence. As an intermediate step, we compute an approximate "can't happen together" (CHT) relation between rendezvous statements. This CHT relation has applications in other areas, notably in detection of unexecutable statements and in intertask data flow analysis.
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).