Abstract
We 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.