Proving systolic arrays

  • E. Pascal Gribomont
Parallelism And Concurrency
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)


A method for proving the correctness of systolic arrays is presented. A small language, derived from Hoare's CSP, is used to describe the processing units. The semantics of this language allows the reduction of the network of processes to an equivalent sequential program, the correctness of which can be proved by the classical invariant method. The compatibility of the language with CSP is investigated. As a result, the language can also be used to describe wavefront arrays.


Matching Pair Communication Statement Systolic Array Parallel Composition Consistency Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Apt83]
    APT, K.R. “Formal Justification of a Proof System for Communicating Sequential Processes”, JACM, vol. 30, pp. 197–216, (1983)Google Scholar
  2. [Cha86]
    CHANDY, K.M., J. MISRA “Systolic algorithms as programs”, Distributed Computing, vol. 1, pp. 177–183, (1986)Google Scholar
  3. [Che78]
    CHEN, T.C. et al. “The rebound sorter: an efficient sort engine for large files”, Proc. 4th. Int. Conf. on VLDB, pp. 312–318, IEEE, New-York, (1978)Google Scholar
  4. [Dij76]
    DIJKSTRA E.W. “A discipline of programmingrd, Prentice-Hall, New-Jersey, (1976)Google Scholar
  5. [Dij77]
    DIJKSTRA E.W. “A correctness proof for networks of communicating processes: a small exercise”, EWD 607, Burroughs, The Netherlands, (1977)Google Scholar
  6. [Elr83]
    ELRAD, T.E., N. FRANCEZ “Decomposition of distributed programs into communication-closed layers”, SCP, vol. 2, pp. 155–174, (1983)Google Scholar
  7. [Flo67]
    FLOYD, R.W. “Assigning meanings to programs”, Proc. AMS Symp. in Applied Mathematics, vol. 19, pp. 19–31, (1967)Google Scholar
  8. [For85]
    FORTES, J.A.B. et al. “Systematic approaches to the design of algorithmically specified systolic arrays”, IEEE Conf. ICASSP 85, vol.1, pp. 300–302, (1985)Google Scholar
  9. [Hen86]
    HENNESSY, M. “Proving Systolic Systems Correct”, ACM Toplas, vol. 8, pp. 344–387, (1986)Google Scholar
  10. [Hoa69]
    HOARE, C.A.R. “An axiomatic approach to computer programming”, CACM, vol. 12, pp. 576–583, (1969)Google Scholar
  11. [Hoa78]
    HOARE, C.A.R. “Communicating Sequential Processes”, CACM, vol. 21, pp. 666–677, (1978)Google Scholar
  12. [Hoa85]
    HOARE, C.A.R. “Communicating Sequential Processes”, Prentice-Hall, (1985)Google Scholar
  13. [Hua87]
    HUANG, C.H., C. LENGAUER “An implemented method for incremental systolic design” LNCS, vol. 258, pp. 160–177, (1987)Google Scholar
  14. [Kun80]
    KUNG, H.T., C.E. LEISERSON “Algorithms for VLSI processor arrays”, in “Introduction to VLSI systems”, Mead and Conway (Eds), Addison-Wesley, Reading, Mass, pp. 271–292, (1980)Google Scholar
  15. [Kun87]
    KUNG, S.Y. et al. “Wavefront Arrays Processors — Concept to implementation”, Computer, vol. 20, pp. 18–33, (1987)Google Scholar
  16. [May83]
    MAY, D. “OCCAM”, ACM Sigplan Notices, vol. 18, nr. 4, pp. 69–79, (1983)Google Scholar
  17. [Mar87]
    MARTIN, A.R., J.V. TUCKER “The concurrent assignment representation of synchronous systems”, LNCS, vol. 259, pp. 369–386, (1987)Google Scholar
  18. [Mil80]
    MILNER, R. “A Calculus of Communicating Systems” LNCS, vol. 92 (1980)Google Scholar
  19. [Mis81]
    MISRA, J., K.M. CHANDY “Proofs of Networks of Processes”, IEEE Trans. on Software Engineering, vol. SE-7, pp. 417–426, (1981)Google Scholar
  20. [Moi85]
    MOITRA, A. “Automatic construction of CSP programs from sequential non-deterministic programs”, SCP, vol. 5, pp. 277–307, (1985)Google Scholar
  21. [Mon87]
    MONGENET, C, G.-R. PERRIN “Synthesis of systolic arrays for inductive problems”, LNCS, vol. 258, pp. 260–277, (1987)Google Scholar
  22. [Oss83]
    OSSEFORT, M. “Correctness Proofs of Communicating Processes: Three Illustrative Examples from the Literature”, ACM Toplas, vol. 5, pp. 620–640, (1983)Google Scholar
  23. [Qui84]
    QUINTON, P. “Automatic Synthesis of Systolic Arrays from Uniform Recurrent Equations”, Proc. 11th Int. Symp. on Computer Architecture, pp. 208–214, (1984)Google Scholar
  24. [Raj87]
    RAJOPADHYE, S.V., R.M. FUJIMOTO “Systolic array synthesis by static analysis of program dependencies”, LNCS, vol. 258, pp. 295–310, (1987)Google Scholar
  25. [Rem87]
    REM, M. “Trace theory and systolic computations”, LNCS, vol. 258, pp. 14–33, (1987)Google Scholar
  26. [Sou84]
    SOUNDARARAJAN, N. “Axiomatic Semantics of Communicating Sequential Processes”, ACM Toplas, vol. 6, pp. 647–662, (1984)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • E. Pascal Gribomont
    • 1
  1. 1.Philips Research LaboratoryBrussels

Personalised recommendations