Incremental Proof of the Producer/Consumer Property for the PCI Protocol

Colloque avec actes et comité de lecture. internationale.International audienceWe present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem~\cite{jones:fmcad00,mokkedem:fmsd00}, the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts