A formal semantics for a DataFlow Machine — Using VDM

  • Kevin D. Jones
A Case Study
Part of the Lecture Notes in Computer Science book series (LNCS, volume 252)


This paper presents a formal description of a non-conventional machine architecture (The Manchester DataFlow Machine) in the denotational style, using an extension of the traditional VDM methods.

The semantics is defined in terms of two fixed-point expressions over a relational domain. Some general and specific properties of such a semantics are presented.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AW77]
    E.A. Ashcroft and W. Wadge. LUCID — a non-procedural language with iteration. CACM, 20(7), 1977.Google Scholar
  2. [BA81]
    Brock and Ackerman. Scenarios — a model for non-determinate computation. In LNCS 107, pages 252–259, Springer-Verlag, 1981.Google Scholar
  3. [Bac78]
    J. Backus. Can programming be liberated form the von neumann style? CACM, 21(8), 1978.Google Scholar
  4. [Bli83]
    A. Blikle. Concurrent distributed processes. 1983.Google Scholar
  5. [Bow81]
    D.L. Bowen. The Implementation of Data Structures in a Dataflow Computer. PhD thesis, University of Manchester, 1981.Google Scholar
  6. [Bro82]
    M. Broy. Fixed point theory for communication and concurrency. In Proc of TC2 Working Conference on Formal Description of Programming Concepts II, IFIP, 1982.Google Scholar
  7. [Bus83]
    V.J. Bush. A survey of the use of matching functions. 1983.Google Scholar
  8. [Cat81]
    A.J. Catto. Non-Deterministic Programming in a Dataflow Environment. PhD thesis, University of Manchester, 1981.Google Scholar
  9. [Dav78]
    A.L. Davies. The architecture and system method of DDM1. In Proc. 5 th Annual Symposium on Computer Architecture, pages 210–215, 1978.Google Scholar
  10. [DFL74]
    J.B. Dennis, J.B. Fossen, and J.P. Linderman. Dataflow schemas. In LNCS 5, Springer-Verlag, 1974.Google Scholar
  11. [Fau82]
    A. Faustini. The Equivalence of an Operational and a Denotational Semantics for Pure Dataflow Programs. PhD thesis, University of Warwick, 1982.Google Scholar
  12. [Gur82]
    J.R. Gurd. Manchester prototype dataflow system description. 1982.Google Scholar
  13. [GW80]
    J.R. Gurd and I. Watson. A data driven system for high speed parallel computing. Computer Design, 19(6–7), 1980.Google Scholar
  14. [GW83]
    J.R. Gurd and I. Watson. Priliminary evaluation of a prototype dataflow computer. In Proc. IFIP 83, North Holland, 1983.Google Scholar
  15. [Hit74]
    P. Hitchcock. An Approach to Formal Reasoning about Programs. PhD thesis, University of Warwick, 1974.Google Scholar
  16. [HP72]
    P. Hitchcock and D. Park. Induction rules and termination proofs. In IRIA Proc., 1972.Google Scholar
  17. [Jon73]
    C.B. Jones. Formal Development of Programs. Technical Report TR12.117, IBM Hursley, 1973.Google Scholar
  18. [Jon81]
    C.B. Jones. Development Methods for Computer Programs — including a Notion of Interference. PhD thesis, University of Oxford, 1981.Google Scholar
  19. [Jon86]
    Cliff B. Jones. Systematic Software Development using VDM. Prentice Hall International, 1986.Google Scholar
  20. [Jon87]
    C.B. Jones. VDM proof obligations and their justification. In this volume, 1987.Google Scholar
  21. [KDJ85]
    K.D.Jones. The Application of a Formal Development Method to a Parallel Machine Environment. PhD thesis, The University of Manchester, 1985.Google Scholar
  22. [Kir81]
    C.C. Kirkham. The basic programmers manual. 1981.Google Scholar
  23. [KM66]
    R.M. Karp and R.E. Miller. Properties of a model for parallel computing. SIAM. Journal of Applied Maths, 14:1390–1417, 1966.Google Scholar
  24. [Kos78]
    P.R. Kosinski. A straightforward non-deterministic semantics for dataflow programs. In Proc. 5 th Annual Symposium on Principles of Programming Languages, 1978.Google Scholar
  25. [Oli84]
    J. Oliveira. A Semantics for Deterministic Dataflow Programs. PhD thesis, University of Manchester, 1984.Google Scholar
  26. [Par80]
    D. Park. On the semantics of fair parallelism. In LNCS 86, Springer-Verlag, 1980.Google Scholar
  27. [Plo76]
    G.D. Plotkin. A powerdomain construction. SIAM Journal of Computing, 5(3), 1976.Google Scholar
  28. [Sar85]
    J. Sargeant. Efficient Stored Data Structures for Dataflow Computing. PhD thesis, University of Manchester, 1985.Google Scholar
  29. [Smy78]
    M.B. Smyth. Powerdomains. Journal of Computer System Sciences, 16:23–26, 1978.Google Scholar
  30. [Sto77]
    J.E. Stoy. Denotational Semantics. MIT Press, 1977.Google Scholar
  31. [VBO83]
    J.R. Gurd V.J. Bush and J. Oliviera. FP as a basis for dataflow program transformation. 1983.Google Scholar
  32. [Vee81]
    A.H. Veen. A Formal Model for Dataflow Programs with Token Colouring. Technical Report IW 179/81, Mathematisch Centrum, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1987

Authors and Affiliations

  • Kevin D. Jones
    • 1
  1. 1.Department of Computer ScienceThe UniversityManchesterEngland

Personalised recommendations