A development snapshot (3.00) of CSP-Prover 3.0 with a DFP package

(to CSP-Porver's homepage)

Introduction

We are developing the next version of CSP-Prover. The differences from the previous version (CSP-Prover2005-2) are summarized as follows:
  1. the replicated alphabetized parallel was added,
  2. expressions of recursive processes were refined,
  3. a DFP (Deadlock Freedom Proofs) package was encoded,
  4. an example of systolic arrays was given.
where DFP contains definitions, lemmas, and theorems given in [1] for proving deadlock freedom of networks. And then, it was proven that a systolic array for matrix multiplication is deadlock free by CSP-Prover with DFP according to [1], where 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.

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

Download

You can download a development snapshot of the next version of CSP-Prover:              download [CSP-Prover-3.00.tar.gz] (139KB) (06/07/2005--)

note: We do not use "year" in version numbering hereafter.
      New version numbers will be given as follow:
        1.*,  2.*,  3.*,  4.*,  ... : major revision  (ver.1 = CSP-Prover2004, ver.2 = CSP-Prover2005, ver.3 = next version)
        3.0,  3.1,  3.2,  3.3,  ... : minor revision of ver.3
        3.00, 3.01, 3.02, 3.03, ... : development snapshots of ver.3.0

Test CSP-Prover with DFP

This version is being developed, and will be modified soon, but you can test to prove that a systolic array for matrix multiplication is deadlock free by CSP-Prover with DFP.

It is assumed that "CSP-Prover-3.00" has been downloaded and has been unpacked (e.g. tar zxvf CSP-Prover-3.00.tar.gz) to the directory (or
your appropriate directory:

   ~/tool/CSP-Prover-3.00

The directory CSP-Prover-3.00 has the tree shown in the following Figure:

     CSP-Prover-3.00 ---+--- CSP   (README, theory map)
                        |
                        +--- DFP   (README, theory map)
                        |
                        +--- Systolic-array   (README, theory map)

To prove the deadlock freedom of a systolic array, heap files of CSP and DFP should be built as follows
(it requires Isabelle(2004)/HOL-Complex):
  1. make a heap file of CSP by

       isatool usedir -b HOL-Complex CSP

    at ~/tool/CSP-Prover-3.00/CSP

  2. make a heap file of DFP by

       isatool usedir -b CSP DFP

    at ~/tool/CSP-Prover-3.00/DFP

  3. Execute ProofGeneral (2004) with DFP as follows:

      Isabelle -l DFP

    at ~/tool/CSP-Prover-3.00/Systolic-array

  4. Load the theory file "SA_main.thy" by C-x C-f.

  5. Prove the theorem by C-c C-n until the bottom.
    (or Finish the proof by C-c C-b at one step)
If you cannot use ProofGeneral, then you can also start isabelle with
DFP as follows:

       isabelle -I DFP

at ~/tool/CSP-Prover-3.00/Systolic-array in a shell window. Then, cut
and past commands from SA_main.thy to the shell window step by step.

Last modified: 11 July 2005
(since 06/07/2005)