Faustini, Antony Azio (1982) The equivalence of an operational and a denotational semantics for pure dataflow. PhD thesis, University of Warwick.

Preview

PDF WRAP_THESIS_Faustini_1982.pdf - Requires a PDF viewer. Download (5Mb) | Preview

Request Changes to record.

Abstract

In this thesis we prove the equivalence of an operational and a denotational semantics for pure dataflow.

The term pure dataflow refers to dataflow nets in which the nodes are functional (i.e., the output history is a function of the input history only) and the arcs are unbounded fifo queues.

Gilles Kahn gave a method for the representation of a pure dataflow net as a set of equations; one equation for each arc in the net. Kahn stated, and we prove, that the operational behaviour of a pure dataflow net is exactly described by the least fixed point solution to the net’s associated set of equations.

In our model we do not require that nodes be sequential nor deterministic, not even the functional nodes. As a consequence our model has a claim of being completely general. In particular our nets have what we call the elcapsulation property in that any subnet can be replaced in any pure dataflow context by a node having exactly the same input/output behaviour. Our model is also complete in the sense that our nodes have what we call the universality property, that is, for any continuous history function there exists a node that will compute it.

The proof of the Kahn principle given in this thesis makes use of infinite games of perfect information. Infinite games turn out to be an extremely useful tool for defining and proving results about operational semantics. We use infinite games to give for the first time a completely general definition of subnet functionality. In addition their use in certain proofs is effective in reducing notational complexity.

Finally we look at possible ways of extending Kahn’s denotational model by the introduction of pause objects called hiatons. Finally we describe interesting ways of refining our operational model.

Item Type:	Thesis (PhD)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions:	Faculty of Science, Engineering and Medicine > Science > Computer Science
Library of Congress Subject Headings (LCSH):	Data flow computing
Series Name:	Department of Computer Science Research Report
Publisher:	University of Warwick. Department of Computer Science
Official Date:	April 1982
Dates:	Date Event April 1982 Submitted
Number:	Number 41
Number of Pages:	199
DOI:	CS-RR-041
Institution:	University of Warwick
Theses Department:	Department of Computer Science
Thesis Type:	PhD
Status:	Not Peer Reviewed
Publication Status:	Unpublished
Supervisor(s)/Advisor:	Wadge, Bill
Extent:	191 p.
Language:	eng

Request changes or add full text files to a record

Repository staff actions (login required)

View Item

Downloads