TI Distributed Deadlock Detection: Algorithms and Proofs 

AU Steve Hilditch 

AU Tom Thomson 

LT UMCS-89-6-1 

OR UMCS 

AV http
http:www.cs.man.ac.ukcsonlycstechrepAbstractsUMCS-89-6-1.html 

AV email techreports@cs.man.ac.uk 

MN June 

YR 1989 

AB We consider loosely-coupled multiprocessors on which memory is 
distributed.   We discuss transaction schedulers which both
serialise transactions and  minimize network messages. _
    Two distributed deadlock detection algorithms are given which
are `truly  distributed' in the sense that they require no
synchronisation procedures or  central control.  These algorithms
can be used in the more general  distributed case.  Formal proofs
of their correctness are given, together with  a discussion of
their efficiency and a comparison with published algorithms. _
    We believe that the formal proof notation and method should
be useful for  verifying other distributed algorithms where
communication is by message  passing.