This file contains the source code for ADVOCAT (Automated Deadlock Verification for On-chip Cache coherence and InTerconnects), as described in the DATE’16 publication: “Deadlock Verification of Cache Coherence Protocols and Communication Fabrics” from Verbeek et al.


REQUIREMENTS:
- Haskell 7.10.2

INSTALLATION:
Simply run:
	make

If there are missing dependencies, cabal will ask you to install these. For example, if you see the following: 

cabal: At least the following dependencies are missing:
aeson ==0.8.*

Then run:
	cabal install aeson
	
LICENSE:
See file LICENSE

EXPLANATION:
When run, deadlock detection is started on the network defined in file “Cross_deadlock.hs”.
This example is explained in the DATE’16 paper (Section 5).
The example is run on a 4x4 2D mesh with the directory connected to node (3,3) (all other nodes are connected to caches).
The queue sizes are set to 22, meaning that a deadlock is possible.
When the queue size is set to 23, (line 59 of Cross_Deadlock.hs, then recompile with make), the network becomes deadlock-free.


QUESTIONS:
Please contact fvb —at— ou.nl for any questions.
