Deadlock detection tools

This page provides an overview of the deadlock detection tools  I have created during my PHD. If your interested in applying or extending these tools, please contact me.

We have tools detecting deadlocks in networks with thousands of processing nodes and resources. If you want to detect routing deadlocks in some interconnection network, please click here for a short tutorial on running our deadlock detection tools for Packet-Switched and Wormhole-Switched networks. In five simple steps, we define a topology, a routing function and compile two algorithms and run them. The work is based on the first two publications below. These tools:
  • Detect deadlocks;
  • Detect livelocks;
  • Check whether the routing function is correct wrt to the topology;
  • Check whether the routing function is connected;
  • Check whether the routing function always supplies valid next hops;
  • Can deal with fault-tolerant routing functions.
We have also used the algorithm to check some custom properties, such as checking for 180 turns in a 2D mesh, or checking whether the routing function changes between subnetworks.

Deadlock detection in packet switched networks

Associated paper: A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free. Proceedings of The 19th Euromicro International Conference on Parallel, Distributed and Network-Based Computing (PDP'11), february 2011 (link)
Sources: (link)


Deadlock detection in wormhole switched networks

Associated paper: Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching. Proceedings of Networks-on-Chips Symposium (NOCS'11), may 2011.
Sources (ACL2 proof): (link)


Deadlock detection in xMAS networks (communication fabrics)

Associated paper: Hunting deadlocks efficiently in microarchitectural models of communication fabrics. Currently under review.
Sources: (link)

<-Home->