Verifying Deadlock-Freedom of Communication Fabrics

Verifying Deadlock-Freedom of Communication Fabrics,10.1007/978-3-642-18275-4_16,Alexander Gotmanov,Satrajit Chatterjee,Michael Kishinevsky

Verifying Deadlock-Freedom of Communication Fabrics   (Citations: 1)
BibTex | RIS | RefWorks Download
Avoiding message dependent deadlocks in communication fabrics is critical for modern microarchitectures. If discovered late in the design cycle, deadlocks lead to missed project deadlines and suboptimal design decisions. One approach to avoid this problem is to get high level of confidence on an early microarchitectural model. However, formal proofs of liveness even on abstract models are hard due to large number of queues and distributed control. In this work we address liveness verification of communication fabrics described in the form of high-level microarchitectural models which use a small set of well-defined primitives. We prove that under certain realistic restrictions, deadlock freedom can be reduced to unsatisfiability of a system of Boolean equations. Using this approach, we have automatically verified liveness of several non-trivial models (derived from industrial microarchitectures), where state-of-the-art model checkers failed and pen and paper proofs were either tedious or unknown.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Recently, there has been significant progress in formal deadlock verification based on modeling systems using a well-defined set of functional primitives [6] and generating inductive invariants [5] and deadlock conditions statically capturing all possible system deadlocks [7]...
    • ...Unreachable structural deadlocks are ruled out using safety invariants which are also obtained through automatic analysis of the model [7]...

    Michael Kishinevskyet al. Challenges in Verifying Communication Fabrics

Sort by: