(*-------------------------------------------*
            |    Example 1 [Roscoe_Dathi_1987 P.10]     |
            |             WITH computation              |
            |  Self-timed version of a systolic array   |
            |                 June 2005                 |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

1 Introduction 

Systolic arrays are parallel algorithms that typically consist of a
large number of similar processing elements which are interconnected
to exchange data where it is characteristic that (1) interconnections
are local only, (2) data moves at a constant velocity, and (3) each of
the elements performs just a certain part of the computation required
to solve the problem. In this example, we prove that a systolic array
for matrix multiplication is deadlock free, according to [1].

2 Theory files

SA_definition.thy : defines a network for matrix multiplication,
SA_expanding.thy  : proves a semantic network satisfying the network,
SA_local.thy      : proves the inequality for Rule1 in [1],
SA_condition.thy  : proves the other condition for Rule1 in [1],
SA_main.thy       : proves deadlock freedom of the network.

3 How to use these theory files

(note: The DFP heap file is required for this example)

(1) Execute Proof General (2004) as follows:

       Isabelle -l DFP

(2) Load the theory file "SA_main.thy" by C-x C-f.

(3) Prove the lemmas by C-c C-n until the bottom.
   (or Finish the proof by C-c C-b at one step)

References

[1] A.W.Roscoe and N.Dathi, "The pursuit of deadlock freedom",
    Information and Computation, Vol.75, No.3, pp.289-327, 1987.