Skip to main content
SpringerLink
Log in

Proving systolic arrays

  • Parallelism And Concurrency
  • Conference paper
  • First Online:
CAAP '88 (CAAP 1988)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 299))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. APT, K.R. “Formal Justification of a Proof System for Communicating Sequential Processes”, JACM, vol. 30, pp. 197–216, (1983)

    Google Scholar 

  2. CHANDY, K.M., J. MISRA “Systolic algorithms as programs”, Distributed Computing, vol. 1, pp. 177–183, (1986)

    Google Scholar 

  3. 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. DIJKSTRA E.W. “A discipline of programmingrd, Prentice-Hall, New-Jersey, (1976)

    Google Scholar 

  5. DIJKSTRA E.W. “A correctness proof for networks of communicating processes: a small exercise”, EWD 607, Burroughs, The Netherlands, (1977)

    Google Scholar 

  6. ELRAD, T.E., N. FRANCEZ “Decomposition of distributed programs into communication-closed layers”, SCP, vol. 2, pp. 155–174, (1983)

    Google Scholar 

  7. FLOYD, R.W. “Assigning meanings to programs”, Proc. AMS Symp. in Applied Mathematics, vol. 19, pp. 19–31, (1967)

    Google Scholar 

  8. 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. HENNESSY, M. “Proving Systolic Systems Correct”, ACM Toplas, vol. 8, pp. 344–387, (1986)

    Google Scholar 

  10. HOARE, C.A.R. “An axiomatic approach to computer programming”, CACM, vol. 12, pp. 576–583, (1969)

    Google Scholar 

  11. HOARE, C.A.R. “Communicating Sequential Processes”, CACM, vol. 21, pp. 666–677, (1978)

    Google Scholar 

  12. HOARE, C.A.R. “Communicating Sequential Processes”, Prentice-Hall, (1985)

    Google Scholar 

  13. HUANG, C.H., C. LENGAUER “An implemented method for incremental systolic design” LNCS, vol. 258, pp. 160–177, (1987)

    Google Scholar 

  14. 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. KUNG, S.Y. et al. “Wavefront Arrays Processors — Concept to implementation”, Computer, vol. 20, pp. 18–33, (1987)

    Google Scholar 

  16. MAY, D. “OCCAM”, ACM Sigplan Notices, vol. 18, nr. 4, pp. 69–79, (1983)

    Google Scholar 

  17. MARTIN, A.R., J.V. TUCKER “The concurrent assignment representation of synchronous systems”, LNCS, vol. 259, pp. 369–386, (1987)

    Google Scholar 

  18. MILNER, R. “A Calculus of Communicating Systems” LNCS, vol. 92 (1980)

    Google Scholar 

  19. 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. MOITRA, A. “Automatic construction of CSP programs from sequential non-deterministic programs”, SCP, vol. 5, pp. 277–307, (1985)

    Google Scholar 

  21. MONGENET, C, G.-R. PERRIN “Synthesis of systolic arrays for inductive problems”, LNCS, vol. 258, pp. 260–277, (1987)

    Google Scholar 

  22. OSSEFORT, M. “Correctness Proofs of Communicating Processes: Three Illustrative Examples from the Literature”, ACM Toplas, vol. 5, pp. 620–640, (1983)

    Google Scholar 

  23. 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. 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. REM, M. “Trace theory and systolic computations”, LNCS, vol. 258, pp. 14–33, (1987)

    Google Scholar 

  26. SOUNDARARAJAN, N. “Axiomatic Semantics of Communicating Sequential Processes”, ACM Toplas, vol. 6, pp. 647–662, (1984)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Philips Research Laboratory, Brussels

    E. Pascal Gribomont

Authors
  1. E. Pascal Gribomont
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. Dauchet M. Nivat

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pascal Gribomont, E. (1988). Proving systolic arrays. In: Dauchet, M., Nivat, M. (eds) CAAP '88. CAAP 1988. Lecture Notes in Computer Science, vol 299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026104

Download citation

  • DOI: https://doi.org/10.1007/BFb0026104

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19021-9

  • Online ISBN: 978-3-540-38930-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation