Functional Real-Time Programming: The
Language Ruth And Its Semantics

byDave Harrison

A thesis submitted in partial fulfilment of the requirements for the degreeof Doctor of Philosophy in the University of Stirling
September 1988

AbstractReal-time systems are amongst the most safety critical systems involving computer
software and the incorrect functioning of this software can cause great damage, up to
and including the loss of life. If seems sensible therefore to write real-time software in a
way that gives us the best chance of correctly implementing specifications. Because of
the high level of functional programming languages, their semantic simplicity and theiramenability to formal reasoning and correctness preserving transformation it thus seems
natural to use a functional language for this task.
This thesis explores the problems of applying functional programming languages toreal-time by defining the real-time functional programming language Ruth.

The first part of the thesis concerns the identification of the particular problems
associated with programming real-time systems. These can broadly be stated as arequirement that a real-time language must be able to express facts about time, a feature
we have called time expressibility.
The next stage is to provide time expressibility within a purely functionalframework. This is accomplished by the use of timestamps on inputs and outputs and byproviding a real-time clock as an input to Ruth programs.
The final major part of the work is the construction of a formal definition of thesemantics of Ruth to serve as a basis for formal reasoning and transformation. The
framework within which the formal semantics of a real-time language are definedrequires time expressibility in the same way as the real-time language itself. This isaccomplished within the framework of domain theory by the use of specialised domains
for timestamped objects, called herring-bone domains. These domains could be used as
the basis for the definition of the semantics of any real-time language.

To my parents :Jim Harrison (1914 - 1975),
Teresa and Bill Carr" ...What I want to establish is how accurate Ruth's time sense is. Somedragons don't have any at all".
"Ruth always knows when he is", Jaxom replied with quick pride. "I'd say
he had the best time memory on Pern"

Anne McCaffrey, "The White Dragon"
Sidgewick & Jackson 1979

Acknowledgements
My grateful thanks to :My family for their unfailing support, despite my stubborn refusal to leave university
and get a proper job.
My colleagues in The University of Stirling Department of Computing Science forproviding such a friendly and stimulating environment in which to work.
Peter "The Man in Black" Henderson for giving me the chance to start a Ph.D., and"Uncle" Ken Turner for giving me the chance to fmish it.
Mustafa Marashi for getting me to work on time, despite an almost total lack ofcooperation on my part.
My fellow members of The Office Cricket Club, Andrew "Rumpelstiltskin" Reeves,Andrew "Yosser" Sinclair and Paul "The Babbler" Williamson for keeping me relatively
sane while I was writing up. This incredible feat was accomplished by allowing me to
top the batting averages for a considerable period, and by plying me with large quantitiesof the products of the Belhaven and Maclay breweries. Thanks also to The Babbler for
proof reading large parts of this thesis.
Sam "The Urban Terrorist" Nelson and the staff and customers of The Settle Inn forpost-thesis depression counselling.
Simon "The Caretaker" Finn for his valiant, and almost successful, efforts to instruct mein the rudiments of domain theory; for proof reading most of this thesis; and for giving
helpful comments on the construction of herring-bone domains. Phil Wadler and John
Launchbury of Glasgow University also provided valuable suggestions on herring-bone
domain construction.
Finally, and most importantly, my supervisor, Simon "The Boss" Jones, without who's
ideas, enthusiasm and the fairly frequent interactions between his boot and my backside
this thesis would never have been written.
Dave "Baldrick" Harrison

Contents
Chapter 1: Defining The Problem: Real-Time Systems And The
Requirements For A Real-Time Programming Language
1.1

Introduction

9

1.2

What Is A Real-Time System?

1.3

Requirements For A Real-Time Programming Language

12
15

1.4

Conclusion

18

Chapter 2: A Survey Of Different Approaches To Real-Time
Language Design
2.1
2.2
2.3
2.4
2.5

Introduction
The Imperative Approach
The Dataflow Approach
The Functional Approach
Conclusion

20
21
25
35
44

Chapter 3: The Language Ruth
3.1

Introduction: Configurations, Processes And Channels

3.2

The Standard Subset of Ruth

3.3
3.4
3.5

Channels, Timestamps And The Ready Test

47
52
54

Clocks And "Real" Real-Time

61

A Worked Example

65

3.6

Conclusion

69

Chapter 4: Semantic Domains For Real-Time Programming
4.1
4.2
4.3
4.4

Introduction

70

Hening-Bone Domain Construction

73

Deftnitions Of The Domains Required For The Semantics Of Ruth

79

Conclusion

86

Chapter 5: The Semantic Definition Of Ruth
5.1

Introduction

87

5.2

Useful Semantic Functions

90

5.3

The Standard Subset Of Ruth

92

5.4

The Real-Time Subset Of Ruth

99

5.5

Conclusion

110

Chapter 6: Using Ruth: A Real-Time Computer Game
6.1

Introduction

111

6.2

Minesweep

112

6.3

Overview Of The Implementation

114

6.4

The Validate Process

6.5

The Cell Processes

6.6

The Monitor Process

6.7

Conclusion

.

118
124

.

127
135

Chapter 7: Review, Assessment And Future Work
7.1

Review

138

7.2

Ruth As A Real-Time Programming Language

142

7.3

Outline Implementation

147

7.4

Theoretical Issues

154

7.5

A Language Based On Explicit Timeouts

162

7.6

Conclusion

169

Appendix 1 :Formal Presentation Of The Semantic Domains

A 1.1

The Foundations

170

A1.2

Herring-Bone Domains

174

A1.3

Non-Primitive Domain Definitions

181

Appendix 2:

Formal Presentation Of The Semantics Of Ruth

A2.1

Syntactic Domains

A2.2

Abstract Syntax .

A2.3

Semantic Domains

A2.4

Semantic Functions

A2.5

Semantic Equations

Appendix 3:

184
184
185
186
191

The Syntax Of Ruth

A3.1

Introduction

203

A3.2

Syntactic Equations

203

Appendix 4:

References

The Minesweep Program .

206

212

Chapter 1 : Defining The Problem: Real-Time
Systems And The Requirements For
A Real-Time Programming Language.

1.1 Introduction

Real-time systems are amongst the most safety critical systems involving computer
software. The incorrect functioning of real-time software can cause great damage, up to
and including the loss of life. It seems sensible therefore, to write real-time software in a
way that gives us the best chance of correctly implementing specifications. Because of
the high level of functional programming languages, their semantic simplicity and theiramenability to formal reasoning and transformation it thus seems natural to use afunctional language for this task. However the functional style seems to have made little
headway amongst real-time programmers and the question must be asked whether this isdue to a basic unsuitability of the functional style of programming for writing real-time
software.

The first functional programming language was LISP [McCarthy 60], yet despite
functional languages' relatively long history it is only in recent times that they have been
regarded as a practical approach to solving real programming problems. Two major
reasons have been advanced for this: first, a belief that such languages were, by theirvery nature, unsuited to solving many classes of programming problems; second, thedifficulty of producing efficient implementations of functional languages on traditional
von Neumann machines. Because of the nature of the computing industry the second ofthese has always been considered the most important: ease of writing, debugging andmaintaining software has always come a poor second to the speed at which software
executes on the hardware.
This ordering of priorities is beginning, albeit slowly, to change because of therapidly rising cost of software production and the equally rapid fall in the cost of
hardware. Even so, efficiency considerations will always be important, particularly inthe area which concerns this work : that of real-time systems. However, functional
languages need not be less efficient than traditional imperative ones. There is a growinginterest in forms of computing engine different from the traditional sequential computerbecause of an effect which has been called the von Neumann bottleneck [Backus 78].
This phrase refers to the fact that the speed of a processor is limited by the speed withwhich it can communicate (both data and instructions) with its memory.

If the speed with which one processor may execute a particular task is limited, thenthe obvious way to improve performance is to use more than one processor to executethe task co-operatively (so called parallel processing). To fully exploit the potential ofparallel processing systems all of the available processors must be kept busy all of thetime, or in other words the task must be partitioned into as many sub-tasks as there areprocessors. This can be difficult with traditional, imperative, languages, such as Pascal
and Fortran, which are based on the von Neumann model of executing operations
sequentially, each operation making some change to the state of the machine. The resultof the computation is the final state of the machine. Functional languages, on the other
hand exhibit the property of referential transparency. The following definition ofreferential transparency is given in [Stoy 77].

"The only thing that matters about an expression is its value, and any expression canbe replaced by any other equal in value. Moreover, the value of an expression is,within certain limits, the same whenever it occurs."

Functional languages do not have the notion of a state which can be changed. A
functional program is simply an expression defining the value of the output of the
program as a function of its inputs. Because of referential transparency the order inwhich different parts of a functional program are evaluated cannot change the value of its
result. In particular, different sub-expressions of the program may be evaluated at thesame time. Thus the potential for parallel evaluation is much easier to realise with afunctional language than with an imperative one.
It seems reasonable to hope that by using parallel computer architectures specifically10designed for evaluating functional languages (e.g. ALICE [Darlington & Reeve 81],
GRIP [Peyton Jones 85]) it will soon be possible for a functional program to exceed theperformance of an imperative program running on a von Neumann machine.
Assuming this to be the case it would seem that the only barrier to the use offunctional languages for real-time systems work is that of suitability. In other words,
how easy is it to express solutions to real-time problems in a functional language : do thedifficulties outweigh the advantages? This work attempts to answer this question bypresenting the functional real-time programming language Ruth, first introduced in[Harrison 87], giving a full denotational semantics for it, and demonstrating its utility.

The fust task is to determine what a real-time system is, and in particular what makes
real-time systems different from other systems. This issue is addressed in the next
section of this chapter which introduces a classification of real-time systems so as tospecify exactly what application area Ruth is directed towards. Following on from thisSection 1.3 derives some basic requirements for a real-time programming language. The
fmal section of this chapter summarises these requirements and presents and overview of
the remainder of the work.

11

1.2 What Is A Real-Time System?

A real-time system can be classified as one in which when events occur is as
important as what events occur. By an event we mean an interaction between the system
and its environment. Typical events could be : the input of a value from a keyboard; theoutput of a control signal to an actuator; or the ticks of a real-time clock. The correctnessof a real-time system depends not only upon the values of its inputs and outputs andtheir relative ordering but also upon their absolute position in time. The situation is very
well summarised in [Young 82] :"In its broadest sense, the term real-time can be used to describe any information
processing activity or system which has to respond to externally generated input
stimuli within a finite and specifiable delay."

A real-time system can only be considered to be behaving correctly if it interacts with
its environment within specified periods of time, or in other words within its time

windows (cf. [Faustini & Lewis 86]). The use of the phrase time windows emphasisesthat systems which interact with their environment too early are just as much in error as
those which interact too late. Usually the lower limit of a time window is defined by thearrival of some input from the environment and we are interested only in the upper limitof the window: the time taken by the system to react to the input event (the deadline).
However the lower limit of a time window is not always fixed in this way and it would
be unwise to forget this. For example a rocket engine may be required to cut out 30
seconds after take off. If the engine cuts out too soon the rocket may fail to reach escapevelocity.

Real-time systems vary from broad systems in which the time windows are large
compared to the speed of a software implementation (e.g. electronic timetabling systems)
to narrow systems in which the time windows are small (e.g. signal processing). The
width of a system's time windows is not the whole story however. A further criterion is
the likely consequence of a system's failure to respond to events within its time12

windows. A disk head controller may have only micro-seconds to position the heads onthe correct track to access a particular block. If the controller fails to meet this deadline,
so that the block has already passed under the heads before they are in position, then theconsequences are not serious: the controller need only wait for the disk to complete
another revolution before it can access the block. On the other hand it may take a nuclear
power station many minutes to become unstable; any control signals during that time
could restabilise the situation but if none are forthcoming the reactor will become critical,
with disastrous results. Clearly, the disk head controller is the narrower of the two
problems but it is much more important that we meet the time windows in the nuclear
power station controller. This is the traditional classification of real-time systems into

hard systems which must always meet their time windows to avoid disaster (such as thenuclear power station controller) and soft systems which can tolerate a certain amount of
failure (such as the disk head controller). (e.g. [Shin 87])
As Le Lann argues [Le Lann 83], the major difference between what are commonly
called real-time systems (the hard end of the range) and conventional data processing
systems (the soft end) is the degree to which they can tolerate failures to meet time
windows. Whereas we prefer a conventional, soft system to produce some result even if
it takes longer than expected, a hard real-time system must produce its outputs within aparticular window or not at all. Conversely if a conventional system produces a result
earlier than expected this is a benefit; in a real-time system it may well be a disaster as theexternal environment may not be ready to receive it.

narrow
process control

hard

soft

data processingbroad

1 . 1 : A classification of real-time systems

13

Thus we have the classification shown in Fig. 1. 1. At the top right are the hard,narrow problems, such as physical process control. At the bottom left are the soft, broad
problems such as conventional data processing. Of course this classification should not
be taken as totally definitive but with some reservations we can take Fig. 1.1 to be areasonable view of the situation.
In the main, problems towards the bottom and left of the diagram are assumed tohave no real-time aspects. The windows are so wide (i.e. from now to eventually)
and/or the consequences of failure so slight (i.e. try again later) that there is no need tocomplicate matters by considering when as well as what. Problems towards the top andright of the diagram are usually handled by custom built electronics. The windows are sonarrow (i.e. micro-seconds) that no software system can be expected to cope without
generating more window violations than the environment can tolerate. It is problems
between these two extremes in which we are mostly interested since these are thesystems which are amenable to software monitoring and/or control, provided that thesoftware is written with timing requirements in mind. In the rest of this work this is thetype of system we shall call a real-time system.

14

1.3 Requirements For A Real-Time Programming Language

For a software system to take account of timing requirements essentially requires
two things: that the system be able to specify when it wishes events to happen and that it
be able to detect when events have (or have not) happened. This obviously requires thata real-time programming language possesses features allowing it to express real-time
information. It must be able to express such things as "turn on the fuel injector 20
milliseconds after the engine is switched on" and "if an acknowledgement is not received
before a timeout signal abort the communication". Such time expressibility is one of
the most important requirements for a real-time programming language.

The time windows constraining a real-time system are usually fixed by its need tointeract with physical hardware. As pointed out in [Le Lann 83] interactions between
software and hardware in real-time systems (called events above) are usually nottransparently recoverable. Incorrect events cannot be simply "rolled-back" and forgotten
about as they will have produced (potentially disastrous) reactions from the physicalhardware (such as moving a control surface on an aircraft). In non real-time systems theuser's response to incorrect events is simply to try again but in a real-time system this is
usually impossible because of the changes to the environment caused by such events.

The requirement that real-time systems interact correctly with their environment is nodifferent from the requirement for conventional systems, although the failure of areal-time system to meet this requirement is usually much more dangerous.
Consequently, language features aiding the writing of correct non real-time software
should be equally effective in the real-time domain. [Young 82] gives a set of desirable
features for a real-time language, such as strong typing, data abstraction and modular
structure which are equally applicable to any programming language. He also makes thepoint that languages should be as simple as possible since simple languages are easier tolearn and programs written in them are easier to understand and reason about.
The major benefit of the use of language features like strong typing, data abstraction
and modular structure is that they support structured programming techniques which
15

tend to make programs easier to develop, debug and maintain. They also make it easierfor the compiler to detect syntactic and static semantic errors. However, there are limits
to the errors that can be detected automatically at compile time. Logical errors may only
become apparent at run-time when it may be too late to correct them.

One way in which this situation can be improved is by formal transformation andreasoning. By formal transformation we mean the ability to write simple and clear
algorithms which are inefficient to execute on a computer, and then automaticallytransform them into semantically equivalent, complex, obscure, but efficient, versions
for execution (e.g. [Darlington 82], [Burstall & Darlington 77]). Another great aid todetecting logical errors is the ability to formally reason and to prove facts aboutprograms. Formal transformation and proof must be based on a formally definedsemantics, which consequently is also one of our requirements for a real-time
programming language.

At present program proving is a lengthy and complex task, even for small programs,
and even the most rigorously proven program is still vulnerable to hardware failure. It is
usually impossible to completely prove a piece of software correct and equally
impossible to completely test it, but, as pointed out above, incorrect software behaviour
could be disastrous. Real-time programmers are thus forced to program in a very

defensive manner, particularly in respect of meeting time windows, since it is often
better to produce the wrong answer at the right time, or no answer at all, than to produce
the right answer at the wrong time. If there is the slightest doubt as to whether a program
will meet its deadlines then it is rewritten, and in most real-time systems the time-criticalpart of the software can be expected to complete its tasks in as little as half the time
available to it. Even so, a real-time system is usually written in such a way that an
imminent failure to meet a time deadline will be detected and recovery action taken. Thisrequires that the system be able to monitor its own progress in time towards thesedeadlines: the system must have knowledge of the passage of real time.

16

The essential requirements for a real-time language are thus:(i)

The ability to defme that a particular event should take place at a particular time.

(ii)

The ability to detect when an event occurs, and, by extension, the ability todetect whether or not a particular event occurs at a particular time.

(iii) The ability to detect and recover from errors, particularly timing errors.

(iv) A formal semantics allowing transformation and proof techniques to be applied
to programs.

The first two of these requirements are what we have called time expressibility andare specific to real-time languages. The third requirement essentially means that thelanguage must support what we have referred to as defensive programming. The major
use of defensive programming in real-time systems is to ensure that deadlines are met.
Consequently the detection and correction of timing errors is the ability we shall be mostinterested in. Once again, this ability is specific to real-time languages and is anotheraspect of time expressibility. Thus the fIrst three requirements may be coalesced into one: that a real-time language have good time expressibility.
The fInal requirement, for a formal semantics, is applicable to both real-time and nonreal-time languages. However, because of the safety critical nature of most real-timesystems, its importance in the real-time domain cannot be overstressed. Althoughcompletely proving programs correct from such a semantics is probably infeasible atpresent, the safety critical parts of programs could be proven, thus increasing confIdence
in the reliability of the program. Further, the use of transformation techniques cannot bejustified without such a semantics.

17

1.4 Conclusion

Real-time systems are usually safety critical systems in that the actions they take are
generally not recoverable : once something has been done it cannot be undone. Since
real-time software is often used to control aircraft, power stations and the like, thecorrectness of real-time software can be a matter of life and death. The use of functional
languages is an aid to the production of correct software because of their relative
simplicity and amenability to formal proof and transformation. However there seems to
be a belief that functional languages are not suitable for writing real-time software. This
work attempts to disprove this by defining, and demonstrating the utility of, Ruth, afunctional language for writing real-time software.

A real-time problem can be classified as one in which when events occur is as
important as what events occur. The importance of when events occur in a real-timesystem has two major implications : the system must specify when it wishes events tooccur and it must be able to detect when events have (or have not) occurred. Thus, thedesign of Ruth must incorporate features allowing it to handle real-time information:
Ruth must have what we have called time expressibility.

The advantages of formal reasoning and transformation in aiding the production ofcorrect software have been noted above. Without a semantic defmition of a programming
language formal reasoning and transformation are impossible. Consequently a complete
formal definition of Ruth will be a major part of this work.
Software engineering issues such as strong typing, modular structure andinformation hiding are also important in the design of a real-time language. However
they are equally important in the design of non real-time languages and consequently
have been addressed in the design of several functional languages already (e.g. HOPE
[Burstall et. al. 80], [Sannella 81], Miranda [Turner 85] and Haskell [Hudak et. al. 89]).
The problems of incorporating software engineering and structured programming intofunctional languages have been, and will continue to be, extensively researched. In
contrast, time expressibility and the semantics of real-time languages have been largely
ignored. Consequently it is these issues which will be the major concern of this work.
18

The next chapter of this thesis contains a survey of the way in which the problems oftime expressibility and formal semantics for real-time have been tackled in three different
programming paradigms: the imperative, dataflow and functional paradigms. From thisbasis the concepts underlying the constructs of the language Ruth will be distilled; Ruth
itself is described in Chapter 3. Chapters 4 and 5 introduce the semantic definition of
Ruth which is based on the denotational framework (e.g. [Stoy 77], [Schmidt 86]).

Chapter 6 demonstrates the utility of Ruth for writing real-time systems by theconstruction of a reasonably substantial example: an interactive computer game. Finally,in Chapter 7, we look at what has been achieved and attempt to answer the initialquestion: is the functional style of programming suitable for solving real-time problems
or not?

19

Chapter 2 : A Survey Of Different Approaches To
Real-Time Language Design

2.1 Introduction

The purpose of this chapter is to compare how three different language paradigms,
imperative, functional and dataflow, solve the special problems associated with theprogramming of real-time systems which were discussed in the opening chapter of thisthesis. The comparison will concentrate on the time expressibility offered by languages
within the three paradigms and on the existence of formal semantic models, since, as
commented at the end of Chapter 1, these are areas which have received little attention in
the past.
The next section of this chapter concerns imperative languages, in particular Ada,
thus allowing the evaluation of current industrial practice with respect to time
expressibility and formal semantics. Section 2.3 concerns an area of current research :real-time languages based on the dataflow model. Section 2.4 assesses real-time andrelated work in functional programming to determine what basis exists from which toconstruct Ruth. The concluding section of this chapter brings together these different
strands to determine what problems remain with the application of the functional style toreal-time programming.

2.2 The Imperative Approach

Most computer programming languages are imperative. A program written in such alanguage is a sequence of commands telling the computer how to change its state so as toarrive at the final solution. Imperative languages directly model the workings of the von
Neumann computer, indeed their basic, sequential style of execution was derived fromit.
Because of its adoption as the required implementation language for real-timesystems by the US Department of Defense and the UK Ministry of Defence probably themost important imperative real-time language is the language Ada [USDOD 83]. Since
the defence industry is the world's major producer and consumer of real-time software it
seems likely that Ada will be the major language used in real-time work for theforeseeable future.

Ada's time expressibility is based upon the predefined package CALENDAR which
provides the type TIME and operations to manipulate that type, including a CLOCK
primitive which returns a representation of the current time in seconds. Ada also supplies
the del.ay primitive to suspend execution of a task for (at least) a given period. The
example below is taken from [USDOD 83] and causes an event to be repeated atintervals of not less than INTERVAL seconds.
(2.1)

decl.areuse CALENDAR;-- INTERVAL is a global constantNEXT TIME

TIME := CLOCK + INTERVAL;

begin
l.oop
del.ay NEXT_TIME - CLOCK;-- some event
NEXT TIME := NEXT TIME + INTERVAL;

end l.oop ;end;

The interval between occurrences of the event is only approximately equal to INTERVAL

21

because the delay primitive only guarantees a minimum waiting time. In the example
above the task could be kept waiting for much longer than INTERVAL if other tasks aresharing the same physical processor. There is no way of specifying in Ada that an event
must occur at a particular time. It is straightforward to specify that it must not occur

before a particular time, but the Ada programmer has no control over how long after
this time the event occurs.

Events are detected in Ada via the rendezvous mechanism. A real-time program
written in Ada is composed of one or more tasks, or processes, running in parallel.
Communication between tasks, and thus between an Ada program and its environment,
is via the rendezvous mechanism: a task may call an entry in another task and then wait
until the called task is willing to accept the call. When the call is accepted the tasks are
said to have rendezvoused and, after the code associated with the entry has been
executed, the tasks part and continue their independent execution.
A task may accept anyone of a number of calls from other tasks by using a selectconstruct. The example below will accept the events INC, DEC and CLEAR, each of whichcauses the value of the variable count to be changed in the obvious way.
(2.2)

selectaccept INC;
count ..= count + 1;

oraccept DEC;count := count

- 1;

or
accept CLEAR;
count := 0;
end select;

Whenever another task (or the hardware environment) issues a call to either INC, DEC or
CLEAR a rendezvous takes place and the count variable is updated. If there is a call tomore than one event already present when the select statement starts executing then an
arbitrary event is accepted. If there are no calls waiting then the select waits until a calloccurs.
22

The behaviour of select when there are no calls waiting initially is an example ofwhat we shall call implicit time determinance. In this situation select accepts thefirst call that arrives after it starts executing. The choice of which call to accept appears
non-detenninate from the text of the program but is not so if the implicit argument to theselect, time, is taken into account. Non-determinance is a powerful tool for abstracting

away from irrelevant details; however it seems somewhat bizarre to use
non-detenninance to abstract away from timing information in a real-time program,particularly since timing information constitutes half, and probably the more important
half, of the information available.
A further problem with select is its behaviour if there are calls already waiting
when it starts execution. In this case the called task decides to accept an arbitrary call andthe basis for this decision is not defined by the language. Once again this abstraction
seems somewhat bizarre in a real-time language. If the programmer does not know
which call will be accepted then he has no alternative but to program defensively toensure that the correct priority in accepting calls will be adopted.

Ada allows programs to detect the non occurrence of an event by a particular time via
the selective wait construct.

(2.3)

selectaccept MESSAGE;

ordelay 10*MILLI SECONDS;TIMEOUT;
end select;

If the MESSAGE event occurs within 10 milliseconds of the start of execution of theselect then TIMEOUT is avoided. Obviously, by using the CLOCK primitive, absolutetimes can be referenced in the delay as well as relative times as above.
The CLOCK primitive also allows Ada programs to monitor their progress in time andthus to check whether deadlines are going to be met. An alternative approach is offeredby the timed entry call which allows a calling task to abort a call if it is not accepted by acertain time.
23

se1ect(2.4)

MESSAGE;or
de1ay lO*MILLI_SECONDS;TIMEOUT;
end se1ect;

IT the entry call MES SAGE is not accepted within 10 milliseconds of the start of executionof the se1ect then TIMEOUT results. By using either of these methods an Ada program
can detect, and thus recover from, timing errors.

Ada is an important, probably the most important, real-time programming language
because of its adoption by the US Department of Defense and UK Ministry of Defence
as the standard implementation language for real-time applications and any realistic
survey of real-time languages must reflect this.
In many ways Ada can be regarded as the epitome of a language supporting
structured programming. It is strongly typed with a very rich type scheme and the
package construct allows good data abstraction and modular programming. Because Ada
was designed to fulfil all the US DoD's software requirements, and not just those in thereal-time domain, it is a very large and complex language. The complexity of Ada has
made the definition of a formal semantics and the production of transformation rules
very difficult (e.g. [Bjorner & Oest 80]). One of the major problems which anyone
attempting a semantics for Ada has to address is the use of the implicit time determinate
se1ect construct. A more serious criticism of Ada is that its time expressibility is

seriously flawed. Detecting that an event has not occurred by a particular time is fairly
straightforward as is the detection and recovery from potential and/or actual timing
errors. However, there is no way to specify that an event must occur at a particular time.
For a real-time language not to have this basic capability is a serious design flaw.
These problems are not specific to Ada but appear, to a greater or lesser extent, inmost imperative languages used for real-time programming (e.g. CORAL-66 [MoD 70],
and Modula-2 [Wirth 83]). In the next section we shall look at a group of languages
which are based not on the von Neumann model but upon the dataflow model ofcomputation.
24

2.3 The Dataflow Approach

2.3.1 Lucid

The dataflow language Lucid [Ashcroft & Wadge 76,77,80], [Wadge & Ashcroft85] is both a programming language and a notation for formal reasoning. The basic
principle of Lucid, in keeping with the dataflow model, is that identifiers and constantsin Lucid do not denote single values but infinite, indexed streams of values orhistories. For example, the constant 1 in Lucid denotes the history < 1, 1, 1, 1,... >.

The identifier x denotes a history containing successive values for x and is often written... >. Operators in Lucid work pointwise upon histories, for example<xo' xl' x2'

Let

x

and

y

=

<0,2,4,6,8,10,... ><1,3,5,7,9,11,... >then x + y

(2.5)

+ Y2'

<xo + YO,xl + Yl'

X2<1,5,9,13,17,21,

... >

... >

For constructing histories from other histories Lucid has the £by (followed by)operator which is similar to Cons in functional languages. £by constructs a new history
by adding the first element of its first history argument to the front of its second history
argument.
Letx = <0,2,4,6,8,10,

(2.6)

... >

<1,3,5,7,9,11, ... >and Ythen x £by Y = < 0 , 1, 3 , 5, 7 , 9, 11,... >The first element of a history can be discarded via the next operator.
Letx= <0,2,4,6,8,10,

(2.7)

... >

then next (x) = <2,4,6,8,10,... >Lucid is a referentially transparent language. Lucid programs are simply functions
from input histories to output histories. Consequently it has a simple formal semantics
which allows relatively easy reasoning and transformation.

25

2.3.2 Real-time Lucid

The basic Lucid paradigm has been extended in many directions. Indeed Lucid is notjust one language but a family of languages and, as might be expected, the area of
real-time programming has not escaped the attention of the Lucid community. Real-time
Lucid [Faustini & Lewis 85, 86], adds time expressibility to basic Lucid by associatingwith each value history (that is each identifier or constant's history) a time window
history defining when elements in the value history should be computed. Each elementof a value history's window history is a pair [1, u] ; the nth element of the value history
must not be produced before the time specified by the 1 value of the nth element of thewindow history, but must be produced before (or at) the time specified by the u value ofthe nth element of the window history. Windows are associated with value histories via
the @ operator.
Letxthen x=<0,2,4,6,8,

@ [x,

... >

(2.8)

next (x) ]= <0,2,4,6,8,... > @ <[0,2], [2,4], [4,6], [6,8], [8,10] ... >The first element of x must be produced between 0 and 2 (inclusive), the second
between 2 and 4, and so on. The window associated with an output value denotes theranges within which each element of the output value's history is to be delivered to theexternal environment. The window associated with an input value denotes the ranges
within which the real-time Lucid program will sample the input line.
Only input and output value histories are given "real" window histories by the
programmer. Histories which are purely internal to the program are given the default
window history in which all elements are [-00, +00], indicating that the values may be
produced at any time that is consistent with the input/output windows.

The time window mechanism is a very powerful one since it allows the real-time
Lucid programmer to directly express facts about the required temporal behaviour of his
real-time system. For example, that the value x is to be output (i.e. the event denoted by
x is to occur) every 10 time units ±3 time units would be expressed as overleaf.

26

x @ [index*10 - 3, index*10 + 3]

(2.9)

where
index

1 fby index+1 i

The fIrst output of x is in the window [7, 13] , the next within [1 7 , 23] and so on. If it
were required that x be output exactly every 10 time units then a point window could be
used.
x @ [index*10, index*10](2.10)

where
index

1 fby index+1 i

The nth output of x is in the window [n * 1 0, n * 1 0] . Since the earliest the output can beproduced (i.e. the event the output denotes can occur) is n * 1 0 and the latest it can beproduced is n*10 then it must be produced (the event must occur) at exactly n*10.

For detecting when an event occurs real-time Lucid supplies the time primitive.
Let x be as defined in (2. 10) above
then time (x)=<10, 20, 30, 40,(2.11).. >The problem with time is that its result cannot be determined from the text of the
program unless (as above) it is only applied to a value associated with a point window.
Otherwise the nth element of the history returned by time may be anywhere between thenth element of the corresponding 1 and u histories.

Let x be as defined in (2. 9) above(2 .12)then time (x) = <10±3, 2 0±3, 30±3, 40±3, .. >Since the result of time may be used as a normal value in a real-time Lucid program thisnon-determinance makes a formal semantics difficult to construct, though work on sucha semantics is in progress. In fact, time is another example of implicit time
determinance; if we knew when results were computed it would be totally determinate.

Detection of the non-occurrence of an event by a particular time depends on the27meaning real-time Lucid actually gives to input and output time windows. As mentioned
earlier, the window associated with an input value denotes the ranges within which thereal-time Lucid program should sample the input line. If no value is present on the input
line during a particular range (i.e. the input event has not occurred) then the program is
supplied with a time fault value, written tf.
Time faults are detected via the boolean operator istf. In the following example let
i be an input of "blip" values denoting that an event has occurred, and let us assume
that the fIrst four its are actually available to be input at times 0, 3, 4 and 7.
Let w = [index,index+2](2.13)and index = 1 fby index+1
index

w

time (i)

1

[1,3]

2

[2,4]

°

3
4

@w

istf (i @ w)

tf

true

3

blip

false

[3,5]

4

blip

false

[4, 6]

7

tf

true

The time fault at index=l in ii

@ w is caused by the input iarriving too soon; the timefault at index=4 is caused by it arriving too late.
Also as mentioned earlier the window associated with an output value denotes theranges within which each element of the output value's history is to be delivered to theexternal environment. Time faults are inserted into output histories whenever the
program fails to produce the desired value within the specified window. This is a simple
form of timing error detection and recovery. Were the language to allow windows to be
associated with internal values as well as input/output values the situation could begreatly improved by adding a supervisor to each output to detect when time faults areabout to occur and take corrective action. An example of this is shown overleaf.

28

out

@ wI

(2.14)

whereout

If istf(temp)
Then default value
Else temp;

temp"expression"

wI

[0,

w2
index

=

[0,

@ w2

(index* 4) + 1](index * 4) ] ;1 fby 1 + index;

If the result, temp, is not computed by the time specified in the "timeout" window w2then a default value is substituted for output within the (wider) window wI. There seems
no reason why windows could not be associated with internal values in this way.
However, as real-time Lucid stands, the programmer has no option but to assume thatthe environment will correctly handle any time fault values produced.

The production of time faults on an input history can be determined from the time theinputs occur and the specification of the time window associated with the input. The
production of time faults on an output can be determined from the time the outputs areproduced and the specification of the time window associated with the output. Thus the
production of time faults is another example of implicit time determinance. If the time atwhich inputs and outputs occur is taken into account then time fault production isdeterminate; if not it is non-determinate, making reasoning and transformation ofprograms very difficult.

The time expressibility of real-time Lucid is very good. Time windows are a directmodel of the real-time requirements for a program. The programmer can specify when
events should occur, either at a point in time or within a range of times. By using thetime operator the programmer can also detect when events actually did occur. However

the result produced by time cannot be determined from the text of a program unless it isapplied to events associated with point windows. The time fault mechanism allows thedetection of the non-occurrence of an event and supplies a rudimentary form of timing
error recovery.
29

Although Lucid has a fully fonnal semantics and proof system associated with it[Ashcroft & Wadge 76] there is, at present, no fully fonnal semantics for real-time
Lucid. This may well be due to the complexity of defining both the time primitive andthe time fault mechanism. Unless a semantics is given some explicit notion of real time
both these features will be non-determinate, making the specification of a semantics
much more complex.

2.3.3 LUSTRE

Real-time Lucid allows the user to specify when, within a range, interactions withthe environment must occur. This is done by associating a window history with eachvalue history. An alternative approach would be to have the indexes in the value history
actually specify a fixed time for such interaction. In other words, that the nth element in
an input (output) history be input (output) at time n.
This is the approach taken by the language LUSTRE ([Bergerand et. al. 85, 86],
[Caspi et. al. 87]) which shares the Lucid view of values as histories, but interprets the
position of an element in a history as defining the time at which the event it denotes
occurs. Thus the time expressibility in LUSTRE is based totally upon the position ofelements within histories.
The real-time interpretation of history positions has one major consequence.
Consider the following LUSTRE expression in which in is an input history and out an
output history.

out

in

+ 1

(2.15)As in all Lucid-like languages the nth element of the out history is obtained by adding 1
to the nth element of the in history. However, in order to be consistent with the meaningof an element's position the nth element of in must be input at time n and the nth elementof out must be output at time n. In other words input and output must be simultaneousand thus the addition must take zero time. This is the called the strong synchrony
hypothesis: all operators are assumed to react instantly to their inputs. On the surface the30strong synchrony hypothesis seems unrealistic as it requires computers to be infinitely
fast. In fact, all that is required is that the computer is fast enough that the external
environment does not notice that it is not infmitely fast. For example, a video game may
be receiving input from a user every tenth of a second; provided the system reacts to that
input within, say, a fiftieth of a second, the user will never notice that the system is not
responding to his input "at the same time" as he is providing it. In other words, provided
that the problem is sufficiently broad compared to the speed of the software the strong
synchrony hypothesis will cause no problems.

Instead of fby and next LUSTRE provides the operators -> and pre. The major
reason for this change is that Lucid's next is non-causal. That is, the result ofnext (input) could not be decided from the values input at time n, the system would

have to wait until time n +1 to obtain the nth element of the next (input) history. Thisobviously violates the strong synchrony hypothesis. pre and -> are causal operators:
their result element at time n can always be determined with information available at timen.

Let x = <0,2, 4, 6, 8,<1,3,5,7,9,
and y
then
pre (x)x(2.16)

... >
... >

<Nil,0,2,4,6,8,... >-> Y = <0,3,5,7,9, ... >pre inserts Nil at the start of its history argument, thus acting as a delaying operator.

-> replaces the first element of its second argument history with the first element of its

first argument history. Note the following equivalences between Lucid and LUSTRE
operators.
x fby next (y)
x

fby y

(2.17)

-> Y

~

x

~

x -> pre (y)In LUSTRE the position of an element in a history denotes the time at which theevent it denotes occurs. Thus the event denoted by the nth element in a history occurs attime n, or in other words at the nth "tick" of what LUSTRE calls the basic clock.
31

LUSTRE also allows values to have their timing dependent on clocks other than thebasic clock. A user defined clock is simply a boolean valued history, a tick being theelement true and a "non-tick" being denoted by false. The basic clock is thus the value
history denoted by true. For example a clock ticking at half the rate of the basic clock isdefined below.

c = true -> not(pre(c»(2.18)<true, false, true, false,... >For any value history x and clock c the operation x when c masks off all elements ofx for which the corresponding element of c is false. Thus, the result of x when c is avalue whose clock is c rather than the basic clock.
xc

Y = x when c

0

true

Yo = 0

1

false

2

true

3

false

4

true

5

false

6

true

Yl

2

Y2

3

(2.19)

Y3 = 5

Events in the history y occur at ticks 0, 2, 4, and 6 of the basic clock. The value of y atbasic clock tick 5 has no more meaning than the value of x at basic clock tick 1. 5. Y
does not exist at basic clock tick 5 any more than x exists between basic clock ticks.
Since clocks are simply boolean valued histories the LUSTRE programmer can treat
them in the same way as any other value which gives a very expressive notion of time.
In particular a clock must itself have a basic clock, thus allowing hierarchies of clocks

based upon each other to be constructed. For example, assuming that the basic clock
ticks every millisecond, a clock that ticks every second can be defined as below.

counto -> If pre (count) ~ 999
Then 0Else pre (count) + 1 ;secondIf count~

999 Then true Else false

32(2.20)

Since count is clocked on the basic, millisecond, clock second will be true every 1000
milliseconds, or in other words, every second. In the same way a minute clock could bebased upon second, an hour upon minute and so on. To define that an event computedby the expression E should occur every second (i.e. that E is based upon the second
clock rather than on the basic, millisecond, clock) the LUSTRE programmer writes
E when second(2.21)At all times other than when second is t rue the value of E is "masked off". Thus E
when second only has a value at exactly one second intervals.

By constructing and using clocks in this way it is simple for a LUSTRE programmer
to defme exactly when events should occur. If the clock upon which the event is based istrue then the event occurs and if it is false then the event does not occur. This also

makes the detection of the non-occurrence of an event simple. If an event does not occur
at or before time n then the clock on which that event is calculated will be false Up totime n. For example, assume that the value history denoting the event we are interested
in is based on the clock c. The following code fragment detects whether or not the event
occurs at n millisecond intervals.
counto -> If c Then 0 E1se pre (count) + 1 ;statusIf count;::: n Then "timeout" E1se "ok" ;(2.22)

Since c is based upon the basic, millisecond, clock, n successive false values meanthat n milliseconds have passed without the event occurring. Thus status becomes"t ime 0 u t ". This example

serves to illustrate one minor inconvenience caused

LUSTRE's implicit notion of time. There is no way of talking about time directly, but
only as the number of t rue ticks on a particular clock. Whether this inconveniencewould cause problems when writing large systems is an area for further research.
A much more serious problem is caused by the strong synchrony hypothesis itself.
This hypothesis is a very powerful one for the specification of real-time systems: itallows the user to ignore the time delays inherent in computation and concentrate on therequirements of the external environment. However there are problems with actually33

implementing real-time systems in a language such as LUSTRE because of theunderlying assumption of infinite execution speed.
Provided the problem is sufficiently broad, or in other words that the implementationof the language is sufficiently fast, strong synchrony poses no difficulties. Efficient
implementations of LUSTRE are possible by compiling the control structure of aprogram into a finite state automaton [Caspi et. al. 87], although there are problem with
distributing such implementations across parallel architectures. But even the mostefficient implementation will eventually prove too slow to cope with the deadlines
required by a particular environment. Because of strong synchrony LUSTRE has no
way of coping with such situations; in fact there is no concept in the language or its
underlying proof scheme of a timing error. Since all operations take zero time there is noway in which a value can take too long to compute.
LUSTRE thus fails our third requirement: it cannot detect and recover from timing
errors. Nonetheless, for a large class of real-time system in which software is so much
faster that its environment that timing errors will not occur languages based on strong
synchrony provide an elegant and expressive vehicle for implementation.

A fully formal semantics exists for LUSTRE, including a clock semantic~ allowing
reasoning about temporal behaviour. (See [Caspi et. al. 87] for an introduction). Since
LUSTRE, like Lucid, is referentially transparent and totally determinate this semantics isfairly simple and formal reasoning and transformation are relatively straightforward.
Other data flow based languages employing the strong synchrony hypothesis include
SIGNAL ([Le Guernic et. al. 85, 86], [Le Guemic & Benveniste 87]) which has a muchricher clock semantics associated with it than LUSTRE, and the imperative language
ESTEREL ([Berry & Cosserat 84], [Berry et. al. 86, 87a, 87b], historically the firstsynchronous language. The synchronous languages offer a simple, and very expressive,model of time. However this model depends on an assumption, the strong synchrony
hypothesis, which cannot be sustained in the real world and which makes theconstruction of defensive programs impossible.
In the next section we shall go on to look at our particular area of interest, functional
languages.
34

2.4 The Functional Approach

The major area of interest for this work is that of functional languages. In Chapter 1
we commented that there were two main reasons why functional languages had not beenused in the real-time field: their perceived inefficiency and the assumption of their basic
unsuitability. The efficiency of functional languages may soon equal, and may
eventually surpass, that of imperative languages, not least because referential
transparency increases the possibilities for parallel execution of functional programs.
The problem, then, seems to be that functional languages are not considered suitable forreal-time programming.
Functional languages offer many advantages over imperative ones, particularly insafety critical areas such as real-time, because they are referentially transparent andtotally determinate. This greatly aids reasoning about programs and the production oftransformation rules (e.g. [Backus 78], [Burstall & Darlington 77], [Darlington 82]).
The simpler the semantics of a language the easier it is to understand programs written in
it and the more confidence a user will have that they are correct. Finally, functional
languages, having a higher level of abstraction than imperative ones, are in general moreconcise. In general, shorter programs are easier to read and understand2.4.1 Streams and non-determinance

There has been little research on real-time programming with functional languages
but quite a substantial body of research has been carried out into the related area ofsystems programming with functional languages (e.g. [Abramsky & Sykes 85],
[Henderson 82], [Holmstrom 83], [Jones 84a, 84b], [Jones & Sinclair 89], [Stoye 86],
[Turner 87]). The major difference between systems programming and real-time
programming is that the former only requires knowledge of the relative ordering of
events whilst the latter requires knowledge of their absolute position in time (what wehave referred to as time expressibility). To support systems programming two basic
ideas have been used: stream processing and implicit time determinance. We shall refer35

to these languages as the implicit time detenninate languages.
Streams are a common way in which functional languages model input and output toand from a program's environment (e.g. [Ida & Tanaka 83,84]). For example, thefollowing function takes an input stream of integers as its argument and increments eachelement by one to produce the output stream.
outputf(input)(2.23)

wheref=lambda (in) . Stream_Cons (Head(in) +1, f(Tail(in»)

endwhere

Note that Stream_cons is a head strict operator: it fully evaluates Head(in) +1 before
consing it to the front of the rest of the output but does not attempt to evaluatef (Tail (in»before performing the cons. Streams are very similar to Lucid histories

save that the programmer must explicitly construct streams and reference their elements
in his program. In Lucid this is implicit so that (2.23) would be written
outputinput + 1

(2.24)

Implicit time determinance is used to decide between events (such as keyboard
inputs) on the basis of which happens first. What is at issue is the temporal ordering ofthese events and not, as would be the case in real-time, exactly when the events actuallyoccur. The constructs used vary but, in general, can all be reduced to the amb operator
fIrst used in [McCarthy 63]. McCarthy states that amb is a purely non-determinate binary
operator, returning either of its arguments at random. However, when used in theimplicit time determinate languages amb is always assumed to return the first of its
arguments that completes evaluation. Only if both arguments are already completely
evaluated when amb is applied is the choice potentially non-determinate and in fact, evenin this case, the choice is usually implemented as a fully determinate one : animplementation of amb usually polls its arguments in order to check whether theirevaluation has completed; the first arguments polled will be returned and polling isalways carried out in the same order.
The following example shows implicit time determinate amb being used to defIne the36function merge which interleaves two input streams, il and i2, in the order in which
the elements of those streams are computed (so called timewise merge).
merge(2.25 )

lambda (il,i2).
altl amb alt2
wherealtl = If il = Nil
Then i2
alt2

Else Stream_Cons(Head(il),merge(Tail(il),i2) ;If i2 = Nil
Then ilElse Stream_Cons(Head(i2),merge(il,Tail(i2»;endwhere

Here Nil is the usual empty stream marker. altl and alt2 cannot determine whether
their respective input streams are Nil until either a stream input or the Nil marker isinput. If a Nil is input then the alternate stream is returned; if a stream input is foundthen it can be returned and the merge continued.
In fact timewise merge and implicit time determinate amb are basically equivalent

operators since amb can be trivially implemented using merge.
amb(2.26)

lambda (vl,v2).

Head(merge(Stream_Cons(vl,Nil), Stream_Cons(v2,Nil»)

Generally speaking all the implicit time determinate languages use either amb- or
merge-like operators.

The basic problem with the use of amb in functional programs is its non-determinate
semantics. Non-determinance is difficult to deal with theoretically since expressions
denote sets of potential results and a powerdomain treatment is required (e.g. [Apt &Plotkin 81], [Apt & Olderog 83], [Broy 82]); this makes proof and transformation very
difficult. Further non-determinance also loses referentially transparency: evaluations of1

amb 2 do not always produce the same result as evaluations of 1 amb 2; this makes

programs difficult to understand and familiar transformation rules ([e.g. Darlington 82])37

are not valid.
In cases where non-determinance is required this is something that programmers
must learn to live with, but in systems programming, and by extension, real-time
programming, non-determinate behaviour is not the property that is required. In
general programmers do not require amb to be non-determinate, they require that it returnthe first of its arguments to become evaluated. However, because most language
semantics abstract away from time, language definers are usually reduced to defining
amb as a non-determinate operator and making vague, natural language, statements about

its real-time properties.

2.4.2 Herring-bone domains and ART

By considering time within a language's semantics it is simple to give a perfectly
determinate definition of ambo In [Broy 83] the language ART (Applicative language forReal-Time programming) is given a denotational semantics in just this way. Eachelement of the domain of values computed by programs (including ..1, the undefinedvalue) is given a timestamp denoting when it was computed (or in the case of ..1 that it
has not been computed by this time). Instead of expressions evaluating to simple values,
they evaluate to a pair <t, v> where v is the data value and t is the time at which it iscomputed. For example <10, t rue> denotes that the boolean value t rue which wascomputed at time 10 whereas <10, ..1> denotes a value that has not been computed at time10.
Fig 2 .27 overleaf is a diagram of the domain of booleans timestamped in just thisfashion. The shape of this diagram leads us to call such domains herring-bone domains.
In a sense time can be said to "flow" up a herring-bone domain; as computation proceeds
the semantic timestamps of..1 values become greater and greater until eventually the value
is computed and the semantic timestamp becomes fixed, or, if the value is nevercomputed, the <00,..1> element (undefined at time infinity) results. As commented in[Broy 83] it is a pleasing feature of herring-bone domains that the non-terminating
computation is not modelled by the weakest element, < 0, ..1>, as is usual in normal
38

domains, but by the "permanently undefined" element, <00,1.>. In the non real-time
domain any program which has not yet produced results conveys the same amount of
information as any other. When dealing with real-time a program which has produced no
results at time 10 conveys more information than a program which has produced no
results at time 5 : the behaviour of the program between times 5 and 10 is now known.
< 0,1.> denotes a computation which has not yet begun, and has thus produced no

results; <00,1.> denotes a computation which produces no results even after infinite time.
Clearly <00,1.> is the element which represents non-termination in a herring-bone
domain.

<00, 1. >•••<2,true>~~<2'falSe><2, 1. ><l,trUe>~~<l'falSe><1, 1. ><o,true>~~<O'falSe><0, 1. >Fig 2.27 : The herring-bone domain of boolean values

Using herring-bone domains a determinate definition of arab is quite straightforward.
(2.28)<t1,Vl> amb <t 2 ,v2>
<t 1 + 1, v 1 >if v 1 ::1= 1. and t 1 ~ t 2<t2 + 1, v 2>

if v 2 ::1= 1. and t 1 > t 2<min(t 1 ,t 2 ) + 1, 1.>

otherwise

Note that we do not assume the strong synchrony hypothesis here: to allow for the time
taken for the amb to be evaluated we increment the timestamp of the result by one. The

39

same approach is taken in the semantics of ART. If only one of amb's arguments isdefined (* J...) then that argument is selected. If both arguments are defined then amb
selects the one with the lower timestamp, or the left argument if the timestamps areequal. If neither argument is defined then the result of the amb is still undefined at theminimum of t l and t2 (plus one to allow for the amb). This is because min (t 1f t 2 > isthe last time about which we have certain knowledge. If t l is less than t2 then Vl may
become defined before t 2 . Likewise, if t2 is less than t l then V2 may become defined
before t 1 . Consequently all we can safely say is that the result of the amb is definitely
undefined at min (tI t2> +1.
f

amb is not an ART primitive, instead the related operator before which returns true

if its first argument is computed before its second, is used. The definition of before isgiven later in this section.

Although amb can now be given a determinate semantics we should note that it is not
sufficiently discriminating for use in a real-time language and that additional operators
will be required. amb can determine which of two events happens first, it cannot
determine when events actually occur and this is a basic requirement for a functional
programming language. The means by which amb was given a determinate definition,
the herring-bone domains, will, however, prove very useful in this work since they
provide a straightforward way for a denotational semantics to express information abouttime and a formal semantics was also a fundamental requirement for the language. A
fuller explanation of herring-bone domains and their properties will be given in Chapter
4 where they will form the basis for the full semantic defmition of the language Ruth.

The other fundamental requirement was that a real-time language should have goodtime expressibility. The implicit time determinate languages, with one exception which
will be discussed later, have no time expressibility. This is un surprising since they were
not designed with real-time problems in mind. ART was designed as a real-time
language and has two primitives which deal with time information. The delay primitive,
shown overleaf, delays the computation of its first argument until, at least, the time
specified by its second argument.
40

let x = <t1,v 1>
and y<t 2 , v 2 >then delay x for y(2.29)A more mnemonic syntax for this construct might be delay x until y. Note that thetimestamp of the result is incremented by one to allow for the time taken to evaluated thedelay. The result of the delay becomes available at V2 provided that V2 is greater thantl and t 2, the times at which the two arguments to delay are computed. Otherwise it

becomes available immediately execution of the delay is completed. Thus, so long as V2
denotes a time later than tl and t 2, the ART programmer can use delay to define when
events are to occur. Unfortunately ART supplies no operations which can detect when avalue is computed so that there is no way to check on the relative values of V2' tl andt 2. Consequently, using delay to specify when events are to occur is unreliable; an

event cannot occur until the values defining it are computed and if this is later than thetime the event was due then the event will not occur on time.
As mentioned above, instead of amb ART uses the operator before which tests
which of its two arguments became defined with the lower timestamp (i.e. soonest).
(2.30)<t1,Vl> before <t 2 ,v2>
<t 1 + 1, true>

if v 1 :1= ~ and t 1 ~ t 2<t2 + 1, false>

if v 2 :1= ~ and t 1 > t 2otherwise<min(t 1 ,t 2 ) + 1,~>

before, like amb, can detect the relative ordering of events and by using a combinationof before and delay timing errors can also be detected.
(2.31)

If timeout before result
Then timeout
Else result
wheretimeout

delay default value for deadline

result. .. ,

endwhere

If result is not computed before timeout then default_value will be returned.
timeout will not be computed until at least deadline but it may well be computed much41

later than this, for example if evaluation of the above code starts so close to deadlinethat default_value cannot be computed in the remaining time. Once again, the use ofdelay is problematic because a programmer cannot be sure when it will delay its result

until.
Since the semantics of ART define exactly when results are produced fromexpressions there is a solution to this problem: the result of a delay can be determinedby mathematically analysing the program containing it. Thus, although a program cannot
detect at run time whether or not time deadlines will be met, since ART has no primitivefor detecting when values are actually computed, deadline failures can be proven not to
occur in a program from the semantics of the language.
However, ART's assumption that it is possible to give a fixed duration for eachmachine operation may be no more realistic than the strong synchrony hypothesis due tothe variability in the duration of operations which normally occurs in a computer. For
example, the time a processor takes to perform a multiplication often depends on the sizeof the numbers being multiplied. In functional languages there are even more problems
due to storage management which could affect the duration of any operation. Further, on
any system which allows several computations to timeshare a single processor there isscheduling to consider. One possible solution could be to give a maximum duration foreach operation which allows for all these factors. However this implies that all
occurrences of this operation will take that maximum time; these operation durations
could be very large giving upper bounds which are too weak for real-time programming.

Both LUSTRE and ART make assumptions about the real-time properties of theirimplementations, assumptions that are probably unrealistic. This approach is in contrast
to that of languages like Ada which assume no real-time properties of implementations.
Instead, in line with the defensive programming philosophy, they provide primitives toallow programs to monitor their own progress in time by referencing a real-time clock.
In Ada this is done via the CLOCK primitive supplied by the CALENDAR package. In theimplicit time determinate language PFL [Holmstrom 83] the value of current time can beobtained by evaluating the primitive time which takes no arguments and returns a
representation of the current time in seconds. However, since time takes no arguments42

but will return a different result each time it is evaluated it is non referentiallytransparent, although it can be given a fully determinate definition using herring-bone
domains.

2.4.3 Real-time clocks in functional programming languages

A referentially transparent way of providing access to a real-time clock in afunctional language, suggested in [Burton 88], is to treat clock values as a lazily
evaluated input stream. Whenever the program wishes to know the time it references thehead of the clock stream. The system then instantiates the head of the clock to the current
time. Any subsequent reference to the head of the clock will obtain the same value sothis preserves referential transparency. For example, the program below waits until 1 0 0 0time units after the start of execution before echoing its input.

output(2.32 )

wait (input,lOOO,clock)where
wait = lambda (i,t,clock).
If t~

Head(clock)

Then iElse wait(i,t,Tail(clock»;endwhere

Note that after it is used each clock value is discarded, by taking clock'S tail, since it
no longer denotes the current value of time.

In the last section of this chapter we shall bring together what we have learned about
different approaches to real-time programming. From these alternative approaches, andfrom what we have discovered in this section about the remaining problems in applying
functional languages to real-time programming, we shall select the basic characteristicsof the language Ruth.

43

2.5 Conclusion

In this chapter we have examined the time expressibility offered by a range ofreal-time languages. Broadly we can identify two types of approach: the pragmatic,
defensive approach and the theoretical, optimistic approach.
The defensive languages, typified by Ada, assume nothing about the real-time
behaviour of a particular language implementation and give no guarantees that specified
deadlines will be met. When working with such languages programmers must programin a very defensive manner: if there is the slightest doubt as to whether software willmeet its constraints then it is rewritten. Defensive languages provide facilities to allow
software to monitor its own progress in time so as to detect, and recover from, failures
to meet deadlines. This usually involves writing a large amount of error handling code
which (hopefully) is never executed. Most, if not all, languages used industrially forreal-time work are defensive in nature.
The optimistic approach, typified by LUSTRE, assumes a particular real-time
behaviour from language implementations. In LUSTRE's case the assumption is that ofstrong synchrony: that machine operations take negligible time and thus specified
deadlines will always be met. LUSTRE thus provides no support for the detection of,and recovery from, failures to meet deadlines since such failures are assumed not to
occur. Programs written in LUSTRE concentrate upon specifying the temporal
behaviour required rather than on how that behaviour is to be achieved.
One of the advantages often cited for functional languages is that they allow the
programmer to concentrate upon specifying what result is required rather than how that
result is to be achieved; at first glance LUSTRE extends that benefit to temporal
behaviour. However, how to produce the required result automatically from a functional
program is a well understood problem; to guarantee the temporal behaviour implicit in a
LUSTRE program is not. A programmer could write programs for which correct
temporal behaviour requires that the implementation be able to perform, for example,
multiplications in negligible time.
The other optimistic language we considered, ART, does not assume strong
synchrony; instead the assumption is that the exact time taken for any machine operation44

is known. Thus temporal behaviour can be predicted from the semantics of the language.
This is not as strong an assumption as strong synchrony but may be equally unrealistic
due to the variability of duration of machine operations. Furthermore, proving the
temporal behaviour of a program from the semantics of language is a complex task for
all but the most trivial of programs, and is very error prone without substantial machine
assistance and checking.

In the future machine performance may improve to such an extent that the strong
synchrony hypothesis is viable for all but the narrowest of real-time problems. Equally,machine assisted program proving may also become possible. Until then we are forced
onto the defensive: real-time programs must be able to monitor their own progress intime and must also be able to detect and recover from failures to meet deadlines.

The implicit time determinate functional languages examined in Section 2.4 modelled
events as elements of infinite streams. This seems the obvious approach for functional
languages and is the approach we shall follow in Ruth. To allow Ruth to specify when
events are to occur, and to detect when events have occurred, we shall associate witheach stream element a time value, or timestamp, and will refer to such timestamped
streams as channels. By testing timestamp values a program can detect when eventsoccur. This approach is similar to that taken by real-time Lucid save the channels havesingle valued timestamps rather than time windows. The use of single valued timestamps
avoids implicit time determinance in the detection of when events occur. In common
with all implicit time determinate operators, real-time Lucid's time primitive can begiven a determinate definition via herring-bone domains; however, and once again incommon with all implicit time determinate operators, its result cannot be predicted fromthe text of a program without a great deal of semantic analysis. Although using single
values is less convenient than time windows we believe that easier understanding of aprogram's real-time behaviour more than compensates for this.
Partly for the same reason, but mostly because implicit time determinate operators
like amb are not sufficiently discriminating for a real-time language, we shall extend ourtest on channel timestamps to detect when events have not occurred: if the timestamp of45

a message in a channel is not less than a certain number then the event did not occur by
the time denoted by that number.
As a consequence of our adoption of the defensive approach Ruth will provide
access to a real-time clock input stream to allow programs to monitor their progress intime and so detect and recover from failures to meet deadlines.

Once again it must be emphasised that Ruth is a language concerned mostly withtime expressibility, software engineering issues having been tackled in some detailelsewhere. Many real-time systems are programmed as sets of parallel processes, bothfor reasons of program design and hardware structure. Rather than invest time and effort
in examining the issues this raises for language design Ruth will directly borrow, andsimplify, the occam [INMOS 84] model of a static set of processes communicating alongpoint to point channels.

46

Chapter 3 . The Language Ruth

3.1 Introduction: Configurations, Processes And Channels

In this chapter we introduce the language Ruth. It is assumed that the reader isfamiliar with functional programming languages and thus the presentation will be fairly
informal. The semantics of Ruth are outlined in the next two chapters and fully formallyin Appendices 1 and 2. The complete syntactic definition of Ruth is given in Appendix

3.

The first step of the presentation is to introduce the model of the real world which
Ruth assumes. We shall do this by informally specifying a real-time system andshowing how it would be implemented as a set of independent, communicating Ruth
processes. Consider the following system :-System

kbl
kb2

.....
......

....
...

kbs
Merge

....... Supervisor--.....

..... scrl.......

...,.. scr2

System takes two keyboard inputs, kbl and kb2, and produces output to two screens,scrl and scr2. System comprises two processes: Merge and Supervisor. Process
Merge takes kbl and kb2 as input and merges them into kbs, on the basis of time ofarrival of each message. Such timewise merges are fairly common in real-time systems,
we have already given an implicit time determinate specification of one in (2.25).
Supervisor takes kbs as input and echoes its contents to both scrl and scr2. There isno timing restriction on Me rge save that it execute as fast as possible, however,Supervisor must echo every message received on kbs to serl and ser2 within ten

time units of its arrival at Supervisor. Whenever Supervisor receives a message
which it cannot echo within this deadline it discards the message and sends 't ime
fault' upon serl and ser2. Whenever Supervisor has to wait for messages on kbs it

sends 'waiting' upon serl and ser2.

A Ruth program is a set of processes executing in parallel and communicating via
streams of timestamped messages, or channels. The set of processes and theirconfiguration is fixed at compile time. Ruth does not allow processes to be dynamicallycreated and/or destroyed at run time. To implement System in Ruth requires aconfiguration of two processes, Merge and Supervisor, communicating by theinter-process channel kbs. System also has four environment-process channels, kbl,
kb2, serl and ser2, carrying the keyboard inputs and screen outputs. In Ruth this isexpressed using the Configuration construct.

(3.1)

Configuration System
Outputserl,ser2

Input

kbl, kb2

Isserl, ser2

Supervisor (kbs)kbs

Merge (kbl, kb2)

end.

A channel is an infinite stream of timestamped data values, or messages, eachmessage denoting an event in the system. Each channel in a configuration must have aunique producing process, or be an input from the external environment, but may beconsumed by any number of processes, including its producer, and/or the environment(though System does not contain an example of this). Each process defines a mappingfrom a tuple of input channels to a tuple of output channels. A process may have any
number of input channels, including none at all; a process may also have any number of
output channels, but must have at least one.
Channel timestamps are represented by non-negative integers. This seems natural indigital computers which can only represent discrete values accurately. We assume thatthe timestamps on channel messages represent values in real-time with an error of ±1/2 a48

tick. Provided the duration of a tick in discrete time is small enough we can treat

timestamps as accurate representation of the continuous values. We shall assume that
this is the case.
The timestamp of a channel message is interpreted as denoting the time at which themessage will become available for use (i.e. will arrive) at its destination. Each message
in the screen output channels scrl and scr2 has a timestamp denoting when themessage should appear on the screen, that is, when the event corresponding to themessage should occur. The timestamps on the messages in kbl and kb2 denote the timeat which the keystroke was made, that is, when the keyboard event occurred.
A consequence of this interpretation of channel timestamps is that we must view theoccurrence of the keystroke and the arrival of the message denoting that event at Merge
as being simultaneous: channel communication is assumed to be infinitely fast. For aninter-process channel, particularly if the two processes are executing on the same
physical processor, communication delays are likely to be small enough to ignore.
However environment-process channels are likely to be carried by relatively long wires(e.g. of the order of a metre or more in an embedded system) and this will causesignificant delay. One possible approach would be to add fixed amounts to thetimestamps of environment-process channel messages to cope with the maximum
possible delay. However, as with machine operations, such a maximum delay is difficult
to specify and may cause large overheads if it is overestimated. In this work, forsimplicity, we shall assume that all communication delays are negligible, whilst being
aware that this is not entirely satisfactory and is an area requiring further work.
Note that although a message's timestamp denotes the earliest time at which its
receiving process can use it there is no reason that the message will be used at that time.
A process may choose to keep messages waiting until it is ready to deal with them, as,for example, Supervisor will do if Merge produces messages too quickly. We assume,
however, that the environment never keeps messages waiting but reacts to them as soon
as they arrive.
Given this interpretation of message timestamps the detection of events and when
they occur simply requires a test on the value of a channel message's timestamp.
However, as we shall see in Section 3.3, the detection of the non-occurrence of an event49

is not quite that straightforward, although basically, it is still a test on the timestamps ofchannel messages.
Returning to our example, System, we see that process Merge takes kbl and kb2 as
input channels and produces channel kbs as its output. In Ruth this is written
Process Merge
Inputkbl, kb2

Clock

c

Is

Expression(3.2)

Unlike a configuration definition, a process definition does not name its output channels
but does name a clock, in this case c. A unique clock is automatically supplied to each

Ruth process at run-time, to provide real-time information, and the Clock keyword
allows the programmer to provide a name by which the clock is referred to in
Expression. Expression may be any Ruth expression and is called the processexpression; it defines a mapping from the tuple of input channels listed after Input,
and the named clock, to the tuple of output channels. In other words Expression
defines a function from the input channels and the clock to the output channels: theprocess function. Of course, a Configuration or a Process definition is not a Ruth
expresslOn.
For simplicity we shall assume that there is no clock skewing between processes. If
the processes are all executing on a single physical processor then they will all use thesame physical clock and thus clock skewing cannot occur. If different physicalprocessors are being used then skewing will almost certainly occur. [Lamport 78] gives
an algorithm by which physical clocks on different processors can be synchronised,within certain fixed limits, by sending timestamped messages between the processors.
The size of the limits depend on the frequency with which messages are exchanged andthe communication delays involved. By using Lamport's algorithm, or somethingsimilar, it is possible to make clock skewing invisible to the Ruth programmer andconsequently in the rest of this work we shall assume it does not occur.

In this section we have been concerned with laying the basic framework of a Ruth

program as a static configuration of parallel processes communicating via channels, each50

process defining a function from its (possibly empty) tuple of input channels and clock
input to its tuple of output channels. A channel is produced by exactly one process but
may be consumed by any number of processes, including its producer. The timestamps
on channel messages denote when the message will arrive at its destination, thus
allowing the programmer to define when events are to occur and, by testing timestamp
values, to determine when events did occur.

In the next section we shall briefly introduce the standard functional part of Ruth.

Section 3.3 discusses channels and, in particular, the way in which Ruth programs
detect the non-occurrence of an event. Section 3.4 concerns real-time clocks and how
they are used. In Section 3.5 we show how Ruth can be used to solve real-time
problems by completing the definition of the fairly simple System, given above.

51

3.2 The Standard Subset Of Ruth

The primitive, or atomic, data objects used in Ruth programs are strings, integers
and booleans. Strings are delimited by , and " for example 'This

is

a

valid

s t ring'. The usual arithmetic operations on integers are provided : addition (+),

subtraction (-), multiplication (*), division (I) and modulus (\); and the usual testing
operators: greater/less than (», greater/less than or equal to (~). Equality (=) and nonequality (~) are defined on all atomic objects. On booleans Ruth provides the usual
operators, And, Or and Not.

Ruth also provides the traditional If ... Then ... Else construct, for example
If (a + b ~ 27) Or (c \ d

* 4)

(3.3)

Then 'OK'
Else 'Not OK'

Functions are denoted in Ruth by lambda abstractions
lambda (a, b, c)(3.4). a + b - c

and function application is by juxtaposition as usual( lambda ( a , b, c ). a+ b - c) ( 4 , 5 , 6 )(3.5)

Identifiers can be associated with values via where definitions.
a + b + (a/b) where a

27

(3.6)

32 ; endwhereb

where does not allow recursive definitions, for this purpose the whererec (whererecursive) construct is provided.
(3.7)

fact(3)whererecfact = lambda (n). If no Then 1 Else n * fact

endwhererec

52

(n-l)

;

For data structuring purposes Ruth uses the LISP notion of the s-expression. Any
atomic value (Le. a string, integer or boolean) is an s-expression; the primitive operator
Cons pairs together two s-expressions to produce a new s-expression and the primitive
operators Head and Tail return the first and second elements of a consed pairrespectively.
Cons ('Hello', 5)[ , Hello', 5]Head (['Hello', 5])'Hello'Tail (['Hello', 5])

5

(3.8)

The empty s-expression is denoted by the keyword Nil and the predicate isNil has
the obvious meaning. A further predicate, Atom tests whether or not an s-expression is
an atomic value. Note that in LISP Nil is an atom whereas in Ruth it is not.
isNil (5)false

isNil (['Hello', 5])

false

isNil (Nil)true

Atom (5)true

Atom (['Hello', 5])

false

Atom (Nil)

false

(3.9)

The semantics of Ruth given in Chapter 5 assume a normal order evaluation strategy
such as is provided by the technique of lazy evaluation (e.g. [Henderson & Morris 76],
[Friedman & Wise 76]). Consequently whererec can be used to define infinite data
structures.

This completes our survey of the standard functional subset of Ruth. The
assumption throughout this section has been that the reader is familiar enough withfunctional programming languages to require nothing more detailed.
In the next section we shall look at the first major step in providing Ruth with time

expressibility : the introduction of timestamped streams of data values allowing Ruth
programs both to determine when events took place and to define when events shouldtake place.

53

3.3 Channels, Timestamps, And The Ready Test

In Section 3.1 we introduced the notion of a channel : an infinite stream of
messages denoting events. The data value in a message defines what the event is and thetimestamp when the event is to occur.
In Ruth the timestamps in channel messages are represented by non-negative
integers and only atomic data objects are allowed as message data values. The major
reason for this restriction is that of efficiency and simplicity of communication. Since thesemantics of Ruth assume normal order evaluation data structures are only evaluated as
far as is necessary to produce the immediately required result. Any s-expression may
contain evaluated and unevaluated parts. The unevaluated parts are represented by,potentially very large, "recipes" for computing their values. If s-expressions are allowed
as message data values an implementation must either traverse their whole structure andcompute the values of all the recipes, or must transmit the recipes as part of the message.
Either strategy would be a significant overhead, both in time and complexity. By
restricting message data values to be atomic objects Ruth avoids this problem since anatomic object is either totally defined or totally undefined, it contains no recipes. If theatomic object is defined it is transmitted; if it is undefined the recipe representing it isforced and the resulting atomic object is transmitted.

We shall denote channel messages by enclosing them between" {" and"} "; forexample It, a} denotes the atom a stamped with the time t.

A channel is a head-strict, infinite, stream of messages. That is to say that Ruth
insists that the first, or head, message in a channel must be completely evaluated toconstruct the channel so as to avoid the problems with partially evaluated messages
outlined above. However the sending of the head message in a channel is totally
unaffected by the contents of the rest, or tail, of the channel, and thus the tail need not be
evaluated for the head message to be sent.
Channels will be delimited by " [" and"] ", for example the channel whose firstmessage is {O, 'Hello'} and whose subsequent messages form the channel rest will54

be written[{O,'Hello'},rest](3.10)

There is one further important property of Ruth channels : the times denoted by thetimestamps in channel messages must be strictly increasing. The interpretation of achannel is that it is an ordered sequence of messages, each of which denotes an event in
the system and the implication of channels being head-strict objects is that their messages
are produced in the order they occur in the channel. In other words we require that thefIrst message in a channel denotes an event which occurs earlier than the events denotedby the messages in the remainder of the channel.
To ensure this we place an incremental interpretation upon channel timestamps. Let
the fIrst message in a channel be {t 1 , al}' the second {t 2 , a2}' and so on. The time atwhich the event denoted by {t l ' a l} occurs is t 1; the time at which the event denoted by{ t 2 , a 2} occurs is t 1 +t 2 + 1. In general, if the time denoted by the timestamp of the nthmessage is Tn then the time denoted by the timestamp of the n + 1 th message isTn+tn+l +1. Note that the +1 ensures that zero valued timestamps still denote a later timethan their predecessor. For convenience, the Ruth programmer will use absolute timevalues for timestamps; the incremental interpretation of timestamps is simply a notational
convenience when expressing the semantics of the language.

The data value part of the first message in a channel is referenced by the Ruth
primitive HeadCh (head channel) and the Time primitive returns the timestamp of thefirst message, that is, when the event it denotes occurs. The tail of the channel isreturned by the primitive TailCh (tail channel).
HeadCh ([{t,a},rest])= a( [ {t, a },re s t] )t

Time

TailCh ([{t,a},(3.11)[{t',a'}, rest']])[ { t +t ' + 1 , a'},re s t ' ]Note the required adjustment to the timestamp of the tail of the channel made in thecalculation of TailCh.

55

The Ruth channel constructor is called ConsCh (cons channel). ConsCh takes asarguments an atomic data value and a number, together defining a message, which it
adds at the head of the channel which is its third argument.
ConsCh (a, t, ch)[{t,a},(3.12)(t ~ t ' ~ 1.,[{t'-t-1, a'}, rest]

) ]

where
[{t',a'}, rest]ch,Here 1. denotes the undefined value. The message to be added to ch must have a lower
timestamp than that at the head of ch since the ordering of channel messages is identicalto the ordering of the events they denote in time. If this is not the case then a channel
containing only the new message results; ch is "ignored" since it is inconsistent with the
new message. Note that the timestamp of the head message of ch is adjusted in line with
the incremental interpretation of channel timestamps when the result channel isconstructed.
There is one other important restriction on channel construction which (3.12) above
does not mention. Since message timestamps denote the time at which the message must
be available at its destination it is obviously an error to add a message with timestamp t
to a channel at a real-time later than t as there is no way that the message can bedelivered on time. Ruth programmers must program in a defensive way, by using theclock inputs to monitor programs' progress in time, so as to detect situations where thismight occur and take corrective action.
Note that the possibility that a message might be computed with an out of datetimestamp can only be expressed in a semantic model which allows the expression oftiming information. Consch will be fully specified when the semantics of Ruth are given
in Chapter 5.

In Section 3.1 we commented that Ruth processes map tuples of input channels into

tuples of output channels. In Ruth tuples are constructed by listing their component
channels between" {" and"}" and channels are selected from tuples via the! operator,
overleaf.

56

{ ch 1 ,•..

(1

ch n }

! m

m ~ n

~

,

~

(3.13)

ch m, .1..)

Note that the channels in a tuple are numbered from 1.

We have now introduced enough of Ruth to allow us to write programs which candefine when events are to occur and respond to when events do occur. For example, theprocess Merge from Section 3.1 requires that two input channels be merged into one
output channel on the basis of when the input messages arrive: a timewise merge. A
Ruth function for such a merge is given below.
merge(3.14)

lambda (ch1, ch2).

If Time(ch1)~Time(ch2)

Then ConsCh(HeadCh(ch1), Time(ch1)+d,

merge (TailCh(ch1), ch2))

Else ConsCh(HeadCh(ch2), Time(ch2)+d,

merge (ch1, TailCh(ch2»

)

where

d = ...;-- a non-negative integer constantendwhere

In Ruth "- -" denotes the start of a comment and comments are terminated by the end of

the line. Each time a message is produced by merge its timestamp is increased by d sothat merge must process messages within d time units of their arrival to avoid channel
construction errors.
The question is, will this definition of me rge evaluate fast enough to meet thisrequirement? The answer is almost certainly not. The expression
Time (ch1)~(3.15 )

Time(ch2)cannot be evaluated unless the first message in both ch1 and ch2 is available. However
all we are trying to determine is which of the two channels produces a message first. If
ch 1 has produced a message and ch2 has not then (3. 15) is obviously t rue and weneed not wait for ch2. In many situations we certainly would not want to wait for ch2 to
produce a message, for example, if chl carried messages from a smoke detector and ch257

carried messages from a keyboard. It highly likely that if a smoke detector has sensed
the presence of smoke it will be a considerable time before another key is pressed on the
keyboard. We would wish to pass on the smoke detector signal immediately and nothave to wait for a keyboard input. Having to wait for both channels to produce a
message before deciding between them will almost certainly ensure that the delay of dtime units will be exceeded.
In fact, timewise merging is just a specific case of one of our requirements for areal-time language: the ability to detect that an event has not occurred. Having to wait
until an event does occur in order to detect that it did not occur by a particular time isclearly undesirable; a check for an event at time t should produce a result at, or as close
as possible, to time t. Since Ruth timestamps denote the actual times that events occur
such a test is trivial to define: the Ready test.
Ready ([{t,a},rest], n)

t

~

n

(3.16)

The advantage of using Ready over using the Time function is that we can rely on
the timestamps denoting the actual real-time at which the channel's messages become
available to the Ready. An evaluation of the expression Ready ( [ {t, a} , rest] , n) canreturn a result immediately if the channel ch already has a message available. If there isno message currently available in ch then evaluation need only be suspended till after thetime denoted by n; after n has passed there is no way that a message with a timestamp
less than or equal to n can appear in ch : the Ready test evaluates to false. Note that thistimeout ability can only be defined in a semantic model containing timing informationand this is done in Chapter 5.

U sing Ready we can rewrite me rge as shown overleaf.

58

merge(3.17)

lambda (ch1, ch2, n).
If Ready(ch1,n)Then If Ready(ch2,n)Then If Time(ch1) ~ Time (ch2) Then ans1 Else ans2
Else ans1
Else If Ready(ch2,n) Then ans2 Else merge (ch1, ch2, n+k)
where
ans1

=

ConsCh(HeadCh(ch1), Time(ch1)+d,
merge(TailCh(ch1), ch2, n+k)

ans2

;

ConsCh(HeadCh(ch2), Time(ch2)+d,
merge (ch1, TailCh(ch2), n+k)

d
k

) ;

a non-negative integer constant;a non-negative integer constantendwhere

Here k is a constant detennining the sampling rate of merge, that is, how often merge
checks for messages. If the sampling rate is too slow (i.e. k > d) then we will certainly
violate the timing requirement by keeping a message waiting for longer than d time units.
However the sampling rate must not be faster than the underlying implementation ofmerge can cope with. If each evaluation of merge takes i time units and i > k then thevalue of n is going to fall further and further behind the current time and the timing
requirement will eventually be violated. Thus, the correct value for k is in the range i tod. Obviously, in the case where d < ithere is no possibility of satisfying the timing

requirement. The value of d is known but detennining that of i is more problematical,
given the problems of predicting the exact timing behaviour of a computer.
Although, without knowing the value of i, we cannot justify ourselves formally, we
can pragmatically argue that our new version of merge has a much better chance ofsatisfying the timing requirement since it will not waste time waiting for unavailable
messages, and thus its value for i will be lower.

In many cases we require that the program be able to detect at run time if it is likely

to fail to meet its deadlines and take remedial action. This is only possible if the program
knows what the current time is. Channels are little help in this: although a channel
timestamp denotes when a message arrives at its destination it does not denote when the59message is finally referenced. A process may leave its inputs queued for some time
before referencing them, so that the timestamps will bear little connection to the current
time. In the next section we consider the clock inputs which are supplied to Ruth
programs and show how they can be used to provide reference to the real-time.

60

3.4 Clocks And "Real" Real-TimeIn the semantics given in Chapter 5 every Ruth program is supplied with a tree oftime values (or clock) as suggested in [Burton 88] and each Ruth process is given a
different sub-tree of the clock so that each process has a unique notion of the current
time. The only reason for using a tree in preference to a linear list for clocks is so thatunique sub-trees can be easily extracted in the semantics to allow for time independent
evaluation of sub-expressions; operationally a process will simply build a list of values
read from its processor's physical clock and thus to the Ruth programmer a clock is justa list of time values.
A clock tree is composed of a node holding a non-negative integer denoting thecurrent time and two sub-trees containing the times of future events. As the tree is(lazily) evaluated each of the nodes is instantiated with the value of system time at thetime at which the node is instantiated, thus giving programs reference to the current
time. We shall denote a clock as a triple enclosed between " [" and "] ", for example[t, 1, r] denotes the clock with node value t

and sub-trees 1 and r.

Since clock nodes will be instantiated in order (i.e. parent node, then child nodes)
the values held in the child trees' nodes must denote times later than the parent's node
value. To ensure this clock node values are given the same incremental interpretation
as was given to channel timestamps. The number in the root node of a clock tree, say t,
denotes the current time; the times in the roots of its immediate children, say tl and t r ,denote the times t+tl +1 and t+tr+1 respectively. In general, if the time denoted bynode in a clock tree is T and the node values of its immediate child trees are t 1 and t pthen the times denoted by the child node values are T+t 1 +1 and T+tr+1 respectively. As
with channels, the Ruth programmer will deal only with absolute time values, theincremental representation of clock times is merely a notational convenience.
The Ruth primitives for accessing clock trees are the functions HeadClk and
TailClk which are defined overleaf. (The names were chosen to emphasise the pointthat to a Ruth expression a clock is just a list of time values).

61

HeadClk ([ t , 1 , r])
TailClk ([t, 1, r])t=(3.18)[ t +t 1+ 1 , 11 '

r 1]

where

TailClk simply returns the left child of the clock tree, so treating the clock as a simple

list. There is no Ruth primitive for constructing clock trees : they are purely inputs to theprogram, the programmer cannot build his own. Obviously the programmer should be
careful that HeadClk is not supplied with a clock which has already had its node value
instantiated since, if that were the case, the value returned by HeadClk would not
represent the current real-time.

With HeadClk and TailClk we can write functions which explicitly respond to thepassage of time. In the last section we gave a version of merge which scanned its input
channels every k time units. We pointed out that determining what the value of k should
be is difficult : too large and messages will be kept waiting too long; too small andmerge would not be able to execute fast enough. By using the clock input to return thecurrent value of time we can remove the need for k altogether and simply check the input
channels "now".
(3.19)

merge
lambda (ch1, ch2, clk).
If Ready(ch1,now)
Then If Ready(ch2,now)

Then If Time(ch1) ~ Time(ch2) Then ans1 Else ans2
Else ans1
Else If Ready(ch2,now) Then ans2 Else merge (ch1,ch2,tclk)
where
ans1

=

ConsCh(HeadCh(ch1), Time(ch1)+d,
merge(TailCh(ch1), ch2, tclk)

ans2

;

ConsCh(HeadCh(ch2), Time(ch2)+d,
merge (ch1, TailCh(ch2), tclk)
;

d

) ;

-- a non-negative integer constantnow

HeadClk(clk)tclk

TailClk(clk);

endwhere62By using the clock input clk to provide values for the current time this version of merge
is effectively parametrised with its speed of execution. This is a better implementation of
our original specification for the Merge process from Section 3.1 in which we stated thatthe only timing requirement for Merge was that it execute "as fast as possible". However
merge has a stronger timing requirement than executing as fast as it possibly can: it

cannot delay an input message by more than d time units or a channel construction error
will be produced. That restriction can be easily removed to produce a me rge functionthat exactly meets the specification for process Merge.
merge(3.20)

lambda (ch1, ch2, clk).
If Ready(ch1,now)
Then If Ready(ch2,now)
Then If T~(ch1)~ T~(ch2)

Then ans1 Else ans2

Else ans1
Else If Ready (ch2, now) Then ans2 Else merge (ch1,ch2,tclk)
where
ans1 = ConsCh(HeadCh(ch1), now + delta,
merge(TailCh(ch1), ch2, tclk)
ans2;

ConsCh(HeadCh(ch2), now + delta,
merge (ch1, TailCh(ch2), tclk)

delta

;

) ;

-- a non-negative integer constantnow

HeadClk(clk)tclk

TailClk(clk)

endwhereIn (3. 19) OUtput messages were timestamped with the time they arrived at merge plus
d. Here output messages are timestamped with the current time plus delta. It would be

tempting to timestamp output messages with the current time alone but this would be anerror. The clock must be instantiated to produce the timestamp before the message can besent and thus, even assuming no transmission delays, the timestamp must be out of date
before the message arrives at its destination. The delta value is used to allow for theunavoidable delay between channel construction and message arrival.

In real-time programs it is a common operation to timewise merge two or morechannels and apply some function to the resulting channel. In the case of (3.20) the63

function applied is the identity function. It would be useful to include a higher-orderfunction which would take as arguments a tuple of channels and a function and would
apply the function to the timewise merge of the channels. This is only one example of
the way in which higher-order functions, in this context often called I/O combinators,
can be used to aid the writing of clear, concise functional programs. For further details
see [Thompson 86], [Bird & Wadler 88] and [Jones & Sinclair 89].

This completes the informal description of Ruth. In the next section we shallcomplete our implementation of System from Section 3.1. This will serve two purposes: to show that Ruth can be used to solve real-time problems, even though the problem
itself is somewhat trivial; and, more importantly, to further illuminate the language itself.

64

3.5 A Worked Example

In Section 3.1 we gave an informal specification of the simple real-time systempictured below.

System

kbl
kb2

....
...

.

kbs
Merge

...

.

...
Supervisor---..

.. serl.. ser2

The purpose of this system is to send all messages received from kbl and kb2 toboth serl and ser2. Messages are to be sent to serl and ser2 in the order they arrived
at kbl and kb2, to ensure which they are timewise merged by the process Merge. The
only timing restriction on Merge is that it process messages as fast as possible. Process
Supervisor takes the merged channel produced by Merge and sends it to both serl andser2. The timing restriction upon Supervisor is that it must pass on all the messages

on kbs within ten time units of their arrival and any message which cannot be output
within this deadline results in the message' time fault' being output. There is norestriction on how often Supervisor checks for messages in kbs, but whenever a checkis made and no message is present the message' waiting' must be output.
The skeleton Ruth program to implement System is as follows
Process Merge

Input kbl, kb2 Clock elkl Is
Clock elk2 Is

Process Supervisor Input kbs

Configuration System
Outputserl,ser2

Input

kbl, kb2

Isserl, ser2

Supervisor (kbs)kbs

Merge (kbl, kb2)

end.

65

(3.21)

We ftrst deftne the process and then the way in which they are configured to form
System. In (3.20) we gave a deftnition of a timewise merge of the form required forprocess Merge. Thus the complete definition of Merge is
Process Merge(3.22)

Input kbl, kb2
Clock elkIs{merge (kbl, kb2, elk)}

whererecmerge = lambda (chI, eh2, elk)... ; -- As (3.20)

endwhererec

Notice that the call of merge function is enclosed between" {" and "}" thus embedding
its result channel into a tuple. This is required because Ruth processes produce tuples as
their results. Note also that Ruth is a case sensitive language: there is no confusion
between the process Merge and the function merge.

The skeleton for Supervisor is(3.23)

Process Supervisor
Input kbs
Clock elkIs{out, out
whererecout = supervisor(kbs, elk)
endwhererec

Since Supervisor sends the same output channel to both serl and ser2 the resultof the application of the function supervisor is simply given twice in the output tuple.
The function supervisor is defined overleaf.

66

supervisor(3.24)

lambda (kbs, clk).
If Ready(kbs, now)
Then If next out - 10 > Time(kbs)
Then ConsCh(1time fault 1 , next_out, rest)
Else ConsCh(HeadCh(kbs), next_out, rest)
Else ConsCh(1 wa iting 1 , next_out, supervisor (kbs, tclk»
whererecnow

HeadClk(clk)tclk

TailClk(clk)next out

now + delta

delta

;

;

-- a non-negative integer constantrest

supervisor(TailCh(kbs), tclk)

tclk

TailClk(clk);;

endwhererec

Note the use of delta to allow for the delay between constructing the channel and themessage being sent. If the fIrst message on the channel arrives before next _ ou t -10,Supervisor cannot meet its deadline and the 1time fault 1 message will be sent

instead.

As suggested by its name, Supervisor acts as a simple output supervisor for
System, detecting, and recovering from, timing errors caused either by the lack of input

from the keyboards (1waiting1) or through its own failure to execute quickly enough(1 time fault 1). More complex strategies could easily be defined. For example, incertain cases a large backlog of messages may build up on kbs because Merge is
producing messages faster than Supervisor can consume them, and sending a timefault message for each message in the queue which could not be delivered in time could
cause Supervisor to fall further and further behind. A more sophisticated approach
would be to remove all messages from the queue which arrived before next_out -10,since these messages can defInitely not be delivered in time, and only produce one 'time
fault 1 message. The function discard removes all messages in a channel withtimestamps less than, or equal to, a given value. discard is defmed overleaf.

67discard(3.25)= lambda (ch, t).
If Ready(ch, t)
Then discard (TailCh (ch) , t)Else chTo implement our more sophisticated recovery strategy we simply replace the Thenbranch of the inner If ... Then ... Else of (3 . 24) , which tests whether a message canbe output within the deadline, by
ConsCh('time fault', next_out,(3.26)

supervisor(discard(kbs,next_out - 10), tclk»

More complicated systems could easily be defined. For example, we might extend
our requirement that Supervisor delay messages by no more than ten time units to thewhole of System. This would involve using the me rge function from (3. 19) , andallowing, say, five time units for Merge and five for Supervisor.

The purpose of this section was to show how Ruth programs can be used to
implement real-time systems. Although the problem chosen was a very simple one itdoes exhibit the essential feature of a real-time system: the necessity to meet deadlines.
A more complex problem, an interactive computer game, is the subject of Chapter 5.

683.6 Conclusion

A Ruth program is a static configuration of processes communicating with eachother, and with the external environment, via infinite streams of timestamped messages,
or channels. A process is a function from a tuple of input channels and a real-time clock
to a tuple of output channels. Each channel in a configuration is produced by a single
process, or by the external environment, but may be consumed by any number ofprocesses, including its producing process, and/or the external environment. A channel
message denotes an event in the real-time system; its data value denotes what the event isand its timestamp when the event is to occur.
Ruth programmers can define when events are to happen by setting the timestamps

in messages, and can detect when events occurred by checking timestamp values.
However, checking message timestamps requires that a message be available to check,and so detecting that an event has not occurred cannot be done by simply checking amessage's timestamp since, until the event does occur, the message will not exist. Ruth
provides a primitive which will timeout messages: the Ready test. Although Readyappears to the Ruth programmer to be a simple test on message timestamps it relies upon
the fact that message timestamps define when messages become available to allow it toreturn false if a message does not arrive by the specified time. In this way Ruth
programs can also detect the non-occurrence of an event as well as its occurrence.

The remaining requirement is for a formal semantics allowing reasoning andtransformation with Ruth programs. In the next chapter we construct a denotationalsemantics for Ruth based on the herring-bone domains introduced in Chapter 2.

69

Chapter 4 : Semantic Domains For Real-Time

Programming

4.1 Introduction

It was noted in the last chapter that to define the semantics of Ruth requires asemantic model which incorporates timing information. In Chapter 2 we saw just such amodel: the denotational semantics based upon herring-bone domains used in [Broy 83]
to specify the semantics of the language ART.
Just as timestamps can be used to allow programmers to specify timing informationin programs they can be used to add timing information to a semantics. The example
given in Chapter 2 was of a herring-bone domain of booleans which can be represented
diagrammatically as<00, 1.. >•••<2,true>'"<2,<l,true>~~<l'false><1, 1.. ><o,true>~~<O'false><0, 1.. >When discussing herring-bone domains we shall observe the following convention:
given a domain D (for example BOOL) the herring-bone domain which is constructedfrom it will be written as W) (e.g. ~~). For the domain BOOL, the set of elements in thecorresponding herring-bone domain ~~ is{<t.b>I t E NUM,b E BOOL} u {<=,~>}(4.1)

For the definition of BOOL, the primitive domain of booleans, the reader is referred toAppendix 1. In (4. 1) NUM is the set of non-negative integers which is used in preference
to NUN, the primitive domain of non negative integers, since it does not contain a ~element and this avoids the possibility of ~ time values.
The ordering required on §@@~, as can be seen from the diagram, isV t 1 , t2

E

NUM, b 1 , b 2 E BOOL

<t 1 , b 1 > !; <t 2 , b 1 >

<=>

(t 1

(4.2)

t2 /\ b 1 !;BOOL b 2 ) V(t 1 ~ t2 /\ b 1= ~)A herring-bone domain, such as §@@~, contains a chain of elements of the form

(4.3)

which, for obvious reasons, we shall refer to as its spine. Computation of an element ofa herring-bone domain can be viewed as the production of increasing elements of thespine (i.e. undefined elements with greater and greater semantic timestamps) until thevalue becomes defined and the semantic timestamp becomes fixed, or, if computation of
the value never terminates, the <=, ~> element eventually results. The interpretation ofelements in a herring-bone domain is thus as follows :-<t, ~> denotes that computation of the value has not been completed by time t.
<t, v> where vt~

denotes that computation of the value v was completed at time t.

<=, ~> denotes that computation of the value is never completed.

In the ordering defined by (4.2) non-~ data values are incomparable unless they are

paired with identical timestamps. On the surface this seems an unusual ordering; a morenatural ordering might be thought to be that specified in (4. 4) below

V tl't2

E

NUM, bl' b 2 E<tl'b 1 > !; <t 2 ,b 1 >and <t 1 , ~>

!;

(4.4)

BOOL

<=>

(t 1 ~ t2 /\ b 1 !;BOOL b 2 )<=, ~>

71

but this is not the case. One of the major reasons for using herring-bone domains is todefme the timeout properties of the Ready teSt. The ordering chosen for §@@~ will carryover into all other herring-bone domains, including @~, the herring-bone domain ofchannels, which is defined later in this chapter. Assuming @~ is ordered by analogy
with (4. 4) we have the following situationa) Ready «10, [msg,rest]>, 10) = true

(4.5)b) Ready «11, [msg,rest]>, 10) = false

and, since <10, [msg, rest] >b;<11, [msg, rest] >, for Ready to be monotonic

requires that true b; false which is clearly undesirable. As will be seen in Section 4.3
this is a somewhat simplistic picture of the semantics of the Ready test but the generalprinciple holds: the ordering from (4.4) would make the Ready test non-monotonic.
Because of the required ordering, and because of the <oo,.l> "top" element, §@@~
cannot be directly constructed as a product of the NUM and BOOL domains. [Broy 83]
makes no mention of how herring-bone domains might be constructed but by using
lifted domains (e.g. [Cartwright & Donahue 82]) to model the semantic timestamps adefinition can be given and this is done in the next section.

The purpose of this section was to introduce herring-bone domains and to outline
some of their properties. The way in which herring-bone domains can be constructed isshown in the next section and the remaining sections of this chapter contain thedefinitions of the domains required to define the semantics of Ruth.
Once again it is assumed that the reader has a reasonable knowledge of denotationalsemantics and domain theory (see [Stoy 77], [Schmidt 86] for details) and so theapproach will be fairly informal. This is to avoid obscuring the discussion with finemathematical detail in the hope of more clearly exposing the underlying concepts.
Appendix 1 contains the fully formal definitions of the domains shown in this chapter.

72

4.2 Herring-Bone Domain Construction

Before defining the domains to be used in giving the semantics of Ruth we mustfirst show how herring-bone domains can be defined using the standard operators of
domain theory. To illustrate the approach the definition of rn@@~ introduced in the lastsection will be given initially; the approach will then be generalised to any cpo.
The definition uses the standard domain operators ffi (coalesced sum) and 1- (domain
lifting) which are defined in Appendix 1. The following constructors and selectors areused on sum domains.
The coalesced sum of two domains A and B is written A ffi B

Constructors :

(4.6)

1-

Selectors:
such thatinA

A~ A ffi B where inA (1-A )inB

B~ A ffi B(Cases x of isA (a)(Cases inA(a)=(/\.(x).el)

where inB (1-B )~elf isB (b)of isA(x)(A(y) .e 2 )

1-

~

e2 )

~

elf isB(y)

~

e2)

~

elf isB(y)

~

e2)

(a)

(Cases inB(b) of isA(x)

=

= 1-

(b)

(Cases 1- of isA(x) ~ elf isB(y) ~ e2)=1-

inA, inB, isA and isB are often called domain injection and projection functions; where

it would cause no confusion they will be omitted from semantic equations. A further
notational convenience is the introduction of an else clause to the Cases notion defmed
above.
(Cases x of isA(a)such that~elf else(Cases inA (a) of isA(x)=(A(X) .el)(Cases inB(b)

~

e2)

(4.7)

~

elf else

~

e 2)

~

elf else

~

e 2)

(a)

of isA(x)= e2(Cases 1- of isA (x)

~

= 1-

73

el f

else

~

e 2)

The constructors and selectors used with lifted domains are as follows
For any domain A the lifted domain is written A .1

Constructor:

(4.8)

..1

lift

Selector:

A

~

A.l

by pattern matching on lift (a) elements.

Having introduced the necessary notation the definition of §@@~ can now be given.
§@@~

BOOL ffi §@@~.l(4.9)

This defmition does not directly mention semantic timestamps, instead they are modelled
via the lifted domain §@@~.1<0,.1>

is modelled by.1(4.10)<0, true>inBOOL(true)<O,false>

inBOOL(false)<1,..1>in§@@~.l (lift (.i) )<l,true>in§@@~.l(lift(inBOOL(true»)<l,false>in§@@~.l(lift(inBOOL(false»)<2,.1>in§@@~.1 (lift (in§@@~.1 (lift (.i) ) ) )<00,1><00,1>

•

•

•

•

•

•

<2.true>",/ < 2 . false>lift(lift(true)),,/

lift (lift (1) )<2,1><1. true>",/lift (true)<1. false>

lift (false)

\/
\/

<1,1>

<o.true>~lift (lift (false))

lift (1)true/ < 0 . false>
<0,1>

1

74

false

The number of times an element of §@@~ has been lifted into §@@~.l models thesemantic timestamp to be associated with it. The "top" element <00,1..> is thus modelledby the limit of the spine elements of §@@~ : that is, byu{(},,(x) .in§@@~.l(lift(x»)t<-i)

I t~O}(4.11)

where, for any function, f
fO (x)= x

f t +1 (x)= f (ft (x) )For reasons of space <00, 1..> was used to represent this limit element in the diagram
given in (4. 10) above.
This isomorphism is proved in Appendix 1. The approach generalises in the obvious
way to any non-recursively defined domain as shown below.
For any domain expression E and domain D such that D is defined(4.12)by D = E and E does not refer to D, the herring-bone domain
corresponding to D is defined by @ = E E!3 IID.l

Elements of domains defined as specified in (4.12) have exactly one semantic
timestamp. When dealing with infinite structures like channels an infinite number oftimestamps will be required, one for each message in the channel. In domain theory
domains containing infinite and potentially infinite structures are defined by means ofrecursive definitions; for example the domain of head-strict infinite lists of non negative
numbers could be defined
LIST

NUM

® LIST.l(4.13)

Here ® is the coalesced product domain operator which is defined in Appendix 1;
elements of product domains will be denoted by listing their components between " ["and "] ", for example [6, l i f t (.i)] is an element of LIST. To form the herring-bone
domain ~~§rg a semantic timestamp must be included for each [number, list] pair in alist and this is achieved by the following definition(4.14)

75

Note that this definition has the same fonn and interpretation as (4. 9) in that thesemantic timestamps are modelled by the number of times a particular element has been
lifted into ~~§~-1' However the recursive use of ~~§~ in (NUM ® ~~§~-1) means that asemantic timestamp is associated with every [number, list] pair. Thus elements of~~§~ have the following structure:(4.15)The use of ® in the definition of ~~§~ ensures that if the number is undefined then
the whole list is undefined. However the tail of the list is lifted so that if it is the weakest
element in ~~§~, <0,1.>, this does not cause the whole channel to be <0,1.>. This isrequired for the head-strictness of lists : if the first element is undefined then the whole
list is undefined; however, provided the first element is defined the list can always beconstructed whatever the value of its tail. It is important that there should be no
confusion between this use of domain lifting and its use on the right hand side of EB tofonn the herring-bone domain.
Note that (4. 14) is very similar to the definition of @~, the domain of channels,
given later in this chapter.

Generalising this to any recursive or non-recursive domain, a herring-bone domain
can be constructed as follows :Given a domain definition D = F (D), where F (D) is a domain(4.16)

expression which mayor may not refer to D, the corresponding
herring-bone domain l]) is defined l]) = F (!Ql) EB l])-1(4.12) is simply a special case of (4.17). The constructors used for a herring-bone

domain are
NUM x

F (l])(4.17)~ l])~l])

Of course (4.17) does not actually construct a herring-bone domain with numericaltimestamps, but a domain which is isomorphic to this. The isomorphism was shown for76the §@@~ domain in (4. 1 0) and (4. 11) above, and is proved in Appendix 1; its
essential feature is that the numeric timestamps in the herring-bone domain are modelled
as injections into a lifted domain as follows :V t E NUM, fd E F (lID) , fd *- -LF (19))(4.18)<t, fd> =(},,(x) .inlID.l(lift (x»)t(inF(lID)<t,-L>(A(x) .inlID.l(lift (x»)t(-L)<oo,-L>

U{ (A (x) . inlID.l (lift (x) ) ) t (-L) I t(fd) )~

O}

where, for any function ffO (x)=

xft+l (x) = f (ft (x) )Isomorphism is a strong enough property for us to assume that domains defined using(4 .16) are actually the required herring-bone domains.

The selector used for herring-bone domains is as follows(OO§'lS@I!ID. <t, v> \13~'lS!ID. <t', -L> ~ el' <t', fd ,> ~ e2)(4.19)

such that(OO§'lS@I!ID. <t, -L> ~~'lS!ID. <t', -L> ~ e l , <t', fd' > ~ e 2 )= (A(t') .e l ) (t)(OO§'lS@I!ID. <t, fd> ~~'lS!ID. <t', -L> ~ e l , <t', fd ,> ~ e 2 )= (A(t',fd').e2)(t,d)

where fd *- -L

Although herring-bone domains are defined recursively as a sum of their basis domains(i.e. F (lID») and the lifted herring-bone domain itself (i.e. lID.l ), the constructors andselectors defined above still use the <t, d> notation introduced in Chapter 2. It is bothmore convenient and more intuitive to refer to the semantics timestamps directly as
numbers rather than as a number of domain lifts and injections. <00, -L> is used toconstruct the limit of the spine elements of a herring-bone domain since it is convenient
to have a way of expressing non-termination directly. However, no case for <00, -L> isrequired in the OO§'lS@I!ID. ••• ~~'lS!ID. ••• selector since, by continuity, the result of applying
the selector to <00, -L> is the limit of the results of applying it to all the spine elements.
Note the potential for the ~§'lS@I!ID. ••• ~~'lS!ID. ••• selector to be used in a
non-monotonic fashion because it explicitly tests for the spine elements. The only place77

in which such a test is required is to define the timeout behaviour of Ready when it isapplied to <t, 1.> channels; in all other cases it will be sufficient to map <t, 1.> elements
to <t, 1.> as is done by the «< ••. ~ notation defined below.
«< <t,v><t ' , fd ,> ~ e ~(4.20)

such that«< <t, v> : <t', fd ,> ~ e(~'i.S@!lli~<t, v> 'l9~'i.Slli<t' ,1.>~<t' ,1.>,<t' , fd' > ~(~'i.S@!lli(A(t',fd') .e)<t" , 1.>~(t',fd')) 'l9~'i.S~<max (t ' , t") , 1.> ,<t",v"> ~ <max(t' ,ttl) ,v">max

NUM x NUM ~ NUM

max

A (t 1 ,t 2). (t 1 > t2 ~ tl' t 2)

Only the case for which the data value part of the herring-bone domain element is non-1.
is given in the «g ••• ~ notation, all <t, 1.> elements are mapped to <t, 1.>. Furthermore,
the notation ensures that, for arbitrary v, the result for <t, v> is not weaker than that for<t, ..1>. Therefore the «g ••• ~ notation cannot be used non-monotonically and sopreserves the monotonicity of functions which use it to access herring-bone domains.
Where there is no possibility of confusion we shall abbreviate the «g ••• ~ notation as
follows:«g<t, v> ~ e ~(4.21)

such that<t, v> ~ e ~«gIn essence, what the «g

•••

«g

<t, v><t,v> ~ e ~~ notation ensures is that the result of a function on anelement of a herring-bone domain cannot be available until the element itself becomes
available; in other words, that time cannot flow backwards. It is a pleasing attribute ofherring-bone domains that mono tonicity of functions can be interpreted in this way.

78

4.3 Definitions Of The Domains Required For The Semantics
Of Ruth
4.3.1 ~: The domain of expressible values

The most important domain used in the semantic definition of Ruth is theherring-bone domain of expressible values, W~, since this domain contains all possible
results of evaluating a Ruth expression.
(S-EXP EF> FUNC EF> TUPLE EF> @~~ EF> @~)EF> W~1.

(4.22)

Apart from the recursive reference to W~~1. required to construct the herring-bone
domain W~ is the coalesced sum of the domains S-EXP (the domain of s-expressions),
FUNC (functions), TUPLE (tuples), @~~ (clocks) and @m~ (channels), each of which

will be defined later in this section. Note that the domains of clocks and channels arethemselves herring-bone domains. The semantic timestamps in @~~ will be used torepresent the time values in a clock and those in ~ to represent the values of the user
defined message timestamps in channels.
Note also that the use of the coalesced sum operator in (4. 22) results in theweakest, <0, .1>, elements of @~~ and @m~ being identified with the weakest, .1,
element of S-EXP EF>

FUNC EF> TUPLE EF> @~~ EF> @m~rn. This could be seen as

undesirable since even a zero semantic timestamp conveys some information whichshould not be lost, but in fact, as will be seen later, this is not the case.

4.3.2 S-EXP : The domain of s-expressions

The first domain to be defined is that of s-expressions. As was seen in Chapter 3
s-expressions are made up of atoms, that is, of booleans, integers and strings. Thus wehave the domain of atoms, ATOM.
(4.23)

ATOM = BOOL EF> INT EF> STRING

79

The primitive domains of booleans (BOOL), integers (INT), and strings (STRING) are theusual, flat, cpos. A further component of the s-expression domain is the primitive cpo
NIL which contains, besides .1, the element Nil which is used to denote the empty list.

The definition of S-EXP is thus
S-EXP

= NIL ffi ATOM ffi PAIR

PAIR(§=§~ x§=§~S-EXP ffi

(4.24)§=§~)~§=§~ ~

Here x is the product operator on domains and is defined in Appendix 1. The domain
PAIR contains pairs of s-expressions constructed via the Cons primitive. Note that PAIR

is actually composed of a pair of herring-boned s-expression domains. Note also that thepair is lifted to avoid identifying the pair [< 0 , .1>, < 0 , .1> ] with the .1 element of S - EXP .
Both these actions are taken because s-expressions are lazily evaluated in Ruth: theelements of a consed pair need not be evaluated in order for the Cons to be evaluated.
Even if the elements of a Con sed pair are undefined the Cons itself may be performed
and thus [< 0,.1>, < 0, .1>] is distinct from .1 in S -EXP. Further, since under a lazy
strategy the elements of a Cons are not evaluated at the same time as the Cons itself,
semantic timestamps are required for these elements; hence the herring-boned domain§=§~ must be used.

4.3.3 FUNC : The domain of functions

The semantic timestamp added to elements of FUNC when they are embedded in ~denotes when the function is available to be applied to its arguments (operationally,
when the code corresponding to the function is loaded from memory). The function
space domain F on elements of the expressible values domain W&J1 is(4.25)

Note that F contains only single argument functions whilst Ruth allows any (finite)
number of arguments to functions. This gives the following definition
80

F

W~ ~

(F ffi W~)(4.26)

There is one further consideration. In Ruth both lambda expressions and process
definitions produce elements of the function space. A function may be applied several
times during the evaluation of a program, and thus at several different real times. This isrepresented in the semantics of Ruth by supplying a function with a clock argumentfrom which it obtains the times at which its results become available.
@~~ F

FUNC

(4.27)

When an element of FUNC is applied to a clock the result is an element of F
"parameterised" with its evaluation time. This use of clocks is called clock-driven timing
and will be discussed in some detail in the next chapter.

4.3.4 TUPLE: The domain of tuples

TUPLE is similar to the domain PAIR defined above in that it contains herring-bone

sub-domains. Each channel in a tuple may be evaluated independently of any other, andof construction of the tuple itself, and consequently each channel requires a separate
semantic timestamp.

TUPLE

=

§~~

= @rnlM:i EiJ §~~.lO~~~.l® TUPLE) EiJ NIL(4.28)

Note the use of the NIL domain to mark the end of a tuple. Also note that elements of the§~§~ domain are identical in structure to elements of @ID&rn embedded in W~ : they

comprise an element of @.IWm1 with an extra semantic timestamp added.
The use of ® in the equation defining TUPLE ensures that tuples must have a finite
length; however ® has the effect of coalescing the least, <0, .1>, elements of its argument
domains into one least element in the TUPLE domain. We wish to distinguish between atuple containing a <0, .1> member of §~§~ and a totally undefined tuple and so eachmember of §IT!!§~ is lifted to add a new least element which can be coalesced into the81least element of TUPLE.
Elements of the tuple domain will be constructed by listing them between "{" and" }" as below{}, ... ,
such that
{

~

TUPLE

~

TUPLE

(4.29){ } = inNIL (Nil){ el l,e1 2 , · · · , e l m}

Selection from elements of the tuple domain will be by pattern matching on{ell' e12' ... , elm} structures.

4.3.5 @~gs : The domain of clocks

There are two uses for @~gs in the semantics of Ruth. Firstly, its elements are used
to support clock-driven timing; secondly, @~gs is embedded into W~ and its elements
used to provide Ruth programmers with real-time clocks. We shall refer to these two
types of clocks as semantic and program clocks respectively. In the last chapter it was
assumed that a clock tree contained numbers. In fact clocks are defined using aherring-bone domain, the semantic timestamps being used to represent the real-timevalues.
(4.30)

A clock of the form <t c '.1> contains no information beyond that its next time value will
be no less than tc' Once the sub-clocks become defined, that is once the clock is of theform <t c ' [lcf rc] >, the value of tc is fixed and denotes the first time value on theclock. Because of this interpretation of @~gs elements the weakest clock, <0, .1>,
conveys no useful information. Thus, although the use of Ef> in (4.3 0) means that the
weakest element of@~gs x @~, [<0,.1>,<0,.1>], will be identified with the weakest
element of @~gs, <0, .1>, this loses no information.
When @~gs is embedded into W&~ to provide program clocks an extra semantic
82

timestamp is added to each clock. Thus, a clock of the form <t c ' [Ic' rc J > becomes a
program clock of the form <t, <t c ' [Ic' rc J > > when embedded into W&~. It is
important that the difference between the meanings of t and tc is clear. The semantic
timestamp on elements of W~, such as t, denote when values are computed; in the caseof clocks when, for example, the result of a TailClk or an identifier reference to theclock is evaluated. The timestamps within clocks, such as t c ' denote actual values ofreal-time independent of when those values become available to the Ruth program. We
shall refer to these values as clock timestamps and note that there need be no connection
between clock timestamps and semantic timestamps, for example if a clock has alreadyhad its clock timestamps instantiated when it is accessed.
When a clock of the form <t c ' .1> is embedded into W~ it becomes a program clockof the form <t, <tc'.1> >. Since <0,.1> is the weakest element of @~~ the use of EB in
the definition of W~ (4.22) causes <0,.1> to be identified with the weakest element of
S-EXP EB FUNC EB TUPLE EB @~~ EB @rn&m. Thus, when the <0,.1> clock is embedded

into W&~ to form a program clock a <t,.1> element of W&~, for some semantic
timestamp t, results. Once again however, since a < 0,.1> clock contains no useful
information this causes no problems.
A final point to note about clocks is that the incremental interpretation of clocks
mentioned in the last chapter still holds. Given a clock tree <t c' [1 c' r c J > the timedenoted by its root tc is tc; the times denoted by the roots of Ic and r c , say tl and tr
are tl +tc+1 and tr+tc+1 respectively.

4.3.6 @rn&m: The domain of channels

A channel is a head-strict list of timestamped atomic values, or messages. The
domain ~ is thus defined (c.f. (4.14))(4.31)The timestamps of messages in channels are supplied by the programmer in the ConsChconstruct. In the herring-bone domain @lIll.mJ the message timestamps are represented by83the semantic timestamps. Thus, where in Chapter 3 we wrote [{ 10, 'Hello' } , rest]
for the channel containing the message' Hello' at (user defined) time 10, followed by
the channel rest, we now write <10, [ 'Hello' , lift (rest) ] >.

As with clocks the incremental interpretation of channel timestamps mentioned in thelast chapter still holds. Given a channel <t, [a, lift (rest) ] > the actual time denotedby its first timestamp t is t; the time denoted by the first timestamp in rest, say tr is
t+tr+1.

Also as with @~~, when @~ is embedded into W~ an extra timestamp is added.
Thus the channel <t, [a, lift (rest)] > becomes <tv' <t, [a, lift (rest)] », and thechannel <t, ~> becomes <tv' <t, ~». Once again it is important to be clear about thedifference in the meanings of tv and t. The semantic timestamp, tv' denotes the time atwhich the channel is computed, that is, the time at which the result of a ConsCh, TailChor identifier reference to a channel is evaluated. The t values, one for each channel
message, denote the user defined timestamps for each message, and will be referred toas message timestamps in the rest of this work.

The final point to note is the treatment of the <0 , ~> element of ©ffl&m when @~ isembedded into WlNf!J. Because of the use of Ef> in (4. 22) this element is identified withthe ~ element of S-EXP Ef> FUNC Ef> TUPLE Ef> @~~ Ef> @~ and thus a <t,~> element
ofw&~, for some semantic timestamp t, results. Just as with @~~ however no useful

information is lost; a <0, ~> channel is a channel whose first message cannot have atimestamp of less than 0, which is something which is trivially true for all channels.

4.3.7 ENV: The domain of environments

The final domain required is ENV, the domain of mappings from syntactic identifiers
to elements of~.

ENV

Id ~

(4.32)(UNDEF Ef> W~)

84

Here Id is the syntactic domain of identifiers and UNDEF is the primitive domain
containing the elements {l., Undef} which is used to indicate that an identifier is notdefined in a particular environment. The constructors and selectors for ENV are

Constructors :(4.33)o~ENV&

Selector:such that

Id x W~~ENV

ENV x ENV

~ENV[

ENV x Id ~ UNDEF EB W~

]

0 [I]
=

[I

inUNDEF (Undef)
~

v]

[I']

= (I = I'~

inW~(v),

inUNDEF(Undef))(Pl & P2) [I](Cases P2[I]ofisUNDEF (Undef)~

Pl [I]

else

~

P2[I]

In (4.33) P is used to denote an environment and this convention will be followed in therest of this work.

85

4.4 Conclusion

This chapter has concerned the semantic domains required to specify the language
Ruth. The first section explored the elements and ordering required for herring-bone

domains and explained the real-time interpretation of herring-bone domain elements.
Section 4.2 showed how herring-bone domains could be constructed from any domain
by a simple syntactic transformation of that domain's definition. Following this Section
4.3 gave the definitions of the particular domains required to specify the semantics of
Ruth, both herring-bone and otherwise.

Having specified the domains required, the next chapter outlines the semantics of
Ruth.

86

Chapter 5 . The Semantic Definition Of Ruth

5.1 Introduction

In this chapter we shall use the domains defmed in Chapter 4 to outline the semantics

of Ruth. Domain injection and projection functions have been omitted where this causes
no confusion. The fully formal definition of Ruth can be found in Appendix 2.

The semantics of Ruth presented here will be based upon the herring-bone domains
defined in the last chapter. Using herring-bone domains allows us to determine whenvalues are evaluated since the information is contained in their timestamps. The firstquestion to be answered is : how are the semantic timestamps to be paired with data
values determined? In other words, assuming that the time at which the sub-expressionsof an expression produced their results is known, when will the expression produce its
result?
In Chapter 2 we saw two possible approaches to this problem. The strong
synchrony hypothesis, used in LUSTRE, is an example of what we shall refer to as
data-driven timing. Since all machine operations are assumed to take zero time the timeat which an expression produces a result is totally determined by when the input datarequired by that expression becomes available. An alternative approach, which we shallcall delay-driven timing, was used in specifying the semantics of the language ART:
all machine operations are assumed to take a fixed, and specifiable, amount of time toperform.
Data-driven timing gives us a very simple abstraction from implementation details
and makes the semantics easy to work with. Unfortunately it is not a very accurate
model of the real world since it implies that computers are infinitely fast and so gives noreal information about real-time behaviour.
On the other hand delay-driven timing requires that exact durations for every
machine operation be specified and this can be difficult due to the variability of operation
durations that usually occurs in a computer. It may be possible to put upper bounds onthese durations but these upper bounds will usually be much larger than the average
operation times, and, since any implementation will be constrained to take the specified
amount of time to perform each operation, this will waste valuable computing time.
Further, to give a delay-driven semantics to a language forces the specification of many
low level details, for example the order of evaluation of function arguments, and, in alazily evaluated language, when recipes are to be updated with with their values. Finally,
the machine operation times specified in a delay-driven semantics will be implementation
dependent: a particular delay-driven semantics will only apply to the language when it isexecuted by a particular implementation on a particular processor.
These problems with delay-driven timing are essentially caused by its prescriptive
nature. They can be avoided by specifying a more descriptive semantics : instead of
specifying exactly how long each machine operation is to take the semantics of Ruth will
be parametrised with a clock from which the times at which expressions produce results
will be read. This provides a higher level of abstraction than delay-driven timing sincesuch things as evaluation orders need not be specified. Yet it allows the real world to be
more accurately modelled than is possible with data-driven timing; by constraining thevalues read from the semantic clocks in certain ways we can express data dependency,
for example that the result of an addition cannot be available until after the two operands
are computed. We shall call this approach clock-driven timing.

For example, assume that the semantics are parametrised with the clock c. The
logical And of two booleans could be defmed as overleaf

88

a f te r

W&.ThJ x@~ ~W&.ThJ

after
A(v,c) .
~c : <t c ' [lc,r c ]>~~v : <t,d>~from :@~gs(t c > t~<tc'v>, after«t,d>,from(lc,t c )x NUM ~ @~gs

from = A(c,n). ~ c : <t c ' [lc,r c ]> ~ <tc+n+1, [lc,r c ]> ~The function after models the passage of time during execution of an operation which
in a delay-driven semantics is achieved by simply adding a fixed amount to the value's
semantic timestamp. When supplied with a <semantic timestamp, data value> pairafter returns a pair comprising the data value with a semantic timestamp read from theclock but constrained to be strictly greater than its original semantic timestamp. We shallrefer to this process as ageing. Note the use of the from function to take account of theincremental interpretation of clock values.

In the rest of this chapter we shall use herring-bone domains and clock-driven timing

to specify the semantics of Ruth. In the next section we lay the foundations for thisspecification by defining some useful semantic functions. Section 5.3 outlines thesemantics of the standard non real-time subset of Ruth and Section 5.4 covers thesemantics of those parts of Ruth which have been added to cope with real-time systems:
clocks, channels and, in particular, the Ready test.

89

5.2 Useful Semantic Functions

The semantics of Ruth expressions are defined using the evaluation function tv
which has the following signature(5.2)

Here Exp is the domain of syntactic expressions. tv also takes as arguments anenvironment, and a clock to facilitate clock-driven timing. The environment holds
identifier/value bindings and, as can be seen from (4. 33) , if a particular identifier is notbound in an environment the Undef value results. Rather than deal with Undef values
explicitly in the semantics the function lookup is used.
lookupld x ENV ~ W~ (5. 3)

lookupA(l,P) .

(Cases P[l] ofisUNDEF(Undef)~ <~,~>

isW~ «t, v»~<t, v>

If the identifier is undefined in the environment the <~, ~> element results.
Operationally, if an expression attempts to reference an undefined identifier then theexpression will never produce a result: the program will crash.
When writing the semantic equations it will frequently be necessary to extract
sub-clocks from the clock supplied to tv to allow for the independent evaluation ofsub-expressions. For this purpose the extract function will be used.

extract(5.4)

extract
A(c,n) .
~c : <t,[l,r]>~(n ~ 0 ~ from(l,t), extract(from(r,t),n-l))

For the remainder of this work we adopt the following notational conventions:90

VeE @~, n E NUM

en denotes extraet(e,n)(5.5)

VeE @~, n E NUM, P E ENV, En E Exp<tn,vn> denotes ~ [En] P en

It will often prove useful to ensure that all the timestamps in a clock are greater than aspecific time and this is done by the ageing function eloekafter.

eloekafter
eloekafter(5.6)~(e,n).

from(e,n)This completes the definitions of "utility" functions used in specifying the semantics of
Ruth.

91

5.3 The Standard Subset Of Ruth

5.3.1 Constants and identifiers

The simplest Ruth expression is the constant integer, boolean or string expression,for example 10, true or 'A string'. Taking booleans as an example:~ [true] p c~ [ false] p cafter «O,true>,

c)

(5.7)

after«O,false>, c)

When a constant is evaluated the result is available almost immediately; operationally asingle "load constant" instruction is usually the most that will be required. Thus thesemantic timestamp of the result of a constant reference is taken to be the ftrst time on theclock c. Rather than deal with the clock explicitly the after function is used; giving thevalue argument to after a semantic timestamp of 0 ensures that the first time in theclock will be returned. This technique for avoiding explicitly dealing with the clock insemantic equations will be used wherever possible in this work.

Identifter reference is defmed as follows~ [ I ]

P cafter(lookup(I,p), c)(5.8)

Note the ageing of the result to allow for the time taken to look up the identifier in theenvironment; operationally to load the required value from memory.

5.3.2 Binary Operations

In Section 5.1 the semantics of the boolean And operator were given informally(5 • 1)

as an example of the semantics of binary operators in Ruth. Using the apparatus

introduced in Section 5.2 the definition can now be given in a more formal manner andthis is done overleaf.

92

tv [ EI And E2 ] P c= after
~

(5.9)

(

<t l , vI>~ ~<t 2 , v 2 >~<max (t l , t 2 ), vI A v 2 >~~,extract (c, 0»

where

tv [ EI ] P extract (c,l)
tv [ E2 ] P extract (c,2)
or, written in tenns of the conventions given in (5.5)(5.10)

after (~

<tl'v I >~~<t 2 , v 2 > ~ <max (t l , t 2 ), vI A V2 >~~,Note that in this definition a different sub-clock is used to evaluate each of thearguments, EI and E 2. Thus the semantics place no restriction on the order in which thearguments to binary operations are evaluated, though they must obviously be evaluatedbefore the result is produced.
Equation (5.10) allows sequential or parallel evaluation but, by using the clockafter
function, it is simple to specify strictly sequential evaluation.

tv [ EI And E2 ] P c(5.11)

after (~

<tl'v I >~ ~ <t2,v 2 > ~ <t2,

VI Av2> ~

~,

co)

where

tv [ EI ] P cI
~ [ E2 ] P clockafter(c 2 ,t l )Using clockafter to provide a clock which only contains time values bigger than thetime of evaluation of EI specifies that the evaluation of E2 must be perfonned with a93semantic clock which only contains times later than t 1 , the time at which evaluation ofEl

was completed. This does not force an implementation to evaluate El and E2

sequentially but operationally it would appear that the simplest way to ensure that
evaluation of E2 is performed with times strictly greater than tl would be to evaluate
them sequentially.
Although indicating desired evaluation orders in this way is simple, evaluation orderis outside the scope of the descriptive semantics being constructed here. Consequently
equation (5. 10) will be taken to be that defining the semantics of boolean And

Note that although only the And primitive has been considered here all the otherbinary operations in Ruth (Le. boolean Or, equality and the arithmetic operators) aredefined in the same way as And with the relevant operator being substituted for 1\ in(5 . 10) . Their definitions can be found in Appendix 2.

5.3.3 If ... Then ... Else ...

€v [ If El Then E2 Else E3 ] P c~(5.12)<tl'vl>-7 (v 1 -7

€v [E 2 ] P clockafter (c 2 ,t 1 ),€v [E 3 ] P clockafter(c 3 ,t 1 )whereNote the use of clockafter to specify that evaluation of the Then and Else expressions
should not be begun until after the boolean value defined by El has been evaluated and adecision between Then and Else can be made. If clockafter were omitted an
implementor of Ruth would have the freedom to evaluate E 1 , E2 and E3 in parallel; since
the result of either E2 or E3 will not be required some of this work would be discarded.
When working with real-time systems it seems undesirable to allow processing
resources to be consumed by work which may be unnecessary since this may result in94

deadlines not being met; this is prevented by the use of clockafter.

5.3.4 Function definition and application

When FUNC, the domain of functions, was defined in the last section, we saw that
Ruth functions take a semantic clock as an implicit argument; this clock is supplied

when the function is applied and is used to facilitate clock-driven timing.
~ [ lambda (Io ... I n ). E ] P c(5.13)

after«O,f>,c)

where
f

= AOe·AO O ••••AOn·E;[E](P & [Io ~

°

0]

&

••.

&

[In

~ On]) 0e

Here 0e is the place holder for the semantic clock argument and the expression E will be
evaluated using the clock to be supplied as its semantic clock upon function application.
Note that the result of the lambda expression is assumed to be available at the fIrst timeon the clock c, or in other words at some time after its evaluation is begun.
~ [ E1 (E 2 · .. E n ) ] P c~(5.14)<t 1 , f1>~

f1 clockafter(c o,t 1 ) <t 2 ,v 2> ... <tn,vn >When a function is applied the semantic clock supplied to it is constrained by the use ofclockafter to contain times strictly greater than the time at which the function isevaluated; operationally, evaluation of the function body cannot take place until the codefor the function body is loaded from memory. Note that each of the "real" (i.e. explicitlyuser defined) arguments is evaluated with a unique clock; thus function arguments may
be evaluated in parallel or not, as an implementor wishes. Also note that the semantic
timestamps of the "real" arguments have no bearing upon when evaluation of thefunction body starts. Operationally this is in line with lazy evaluation: the time ofavailability (semantic timestamp) of the result of a function application will only depend95

on the times of availability of those arguments required to produce that result. If anargument is referenced its semantic timestamp will be taken into account in the semantic
timestamps of the result of any expression referring to it. If the identifier is notreferenced then its semantic timestamp is irrelevant to the result of the function
application.

5.3.5 Identifier definitions

Identifiers in Ruth are defined by being bound to the value of an expression by awhere or whererec construct.

~ [ E where D endwhere ] p C(5.15)= ~[E] (~[D] P cl) Co~ [ E whererec D endwhererec ] p C£v[E] pI Co
where

pI

=

fix (AP" . P & ~[D]P" C l )Here fix is the usual fixed point function and is defined in Appendix 1, D is a memberof Dec, the syntactic domain of declarations, and CD is the meaning function for
declarations which is defmed(5.16)

cD[r=E;D]pC

c []pc=0D

Note that each declaration in a list of declarations is evaluated using a unique clock, thus
allowing for them to be evaluated in parallel if desired.

96

5.3.6 S-expression manipulation

Atomic and Nil valued s-expressions have a straightforward semantics and thereader is referred to Appendix 2 for details. Our interest here is focused upons-expressions which are consed pairs.
~ [ Cons (E l , E 2 ) ]Pc(5.17)= after«O,lift([<t l ,vl>,<t 2 ,v 2 >]»,c o )The time at which El and E2 are evaluated has no bearing upon when the s-expression isevaluated because of lazy evaluation and thus the fIrst value from the clock provides thesemantic timestamp for the pair. Note that because the head and tail of the pair may be
independently evaluated they retain their own semantic timestamps in the consed pair.
When Head or Tail is applied to the pair these semantic timestamps are used to defIne
when the result is becomes available.
~ [ Head (E l )]Pc(5.18)

after (
egg

<tl'v l >~(Cases vl oflift([<tH,sH>,<tT,sT>])~~else<max(tl,tH),sH><00,1->~,The result of the Head becomes available after the maximum of tl and t H; operationallythe result of a Head cannot be available until both the Cons and the head element itself
have been evaluated. Note that if the argument to Head is not a pair the non-terminating
computation, <00,1->, results. Tail is similar and its definition is given overleaf.

97

~ [ Tail(E 1 )]

P c(5.19)

after (~

<tl'v 1>
-7(Cases v 1 oflift([<t H,sH>,<t T,sT>])-7 <max(t1,tT),sT>else-7 <00,1..>~,This completes the definitions of the standard subset of Ruth. The next section gives
the specification of the semantics of those parts of the language directly concerned withthe programming of real-time systems.

985.4 The Real-Time Subset Of Ruth

5.4.1 Channel construction and reference

When dealing with channels in the semantics of Ruth we will normally be dealing
with elements of @ffi&.rn embedded in w&.~, that is, with objects of the form
<tv' <t ch ' [a, lift (ch) ]»and <tv,<tch,-i». Here tv is the semantic timestamp and,in the fITst case, tch is the message timestamp of the fIrst message a, and in the second adenotation of a time by which the channel has not yet produced a message.
As was commented in Chapter 4 there need be no connection between the values oftv and t ch ' For example, a process references a channel from another process, or fromthe external environment, via the corresponding identifIer given in its Input list. In thiscase the value of tv denotes when the receiving process has identifIed which channel it is
attempting to access. Obviously this is totally independent of t ch ' the time at which thesending process puts the first message in the channel. A simpler case is that a channel
may be be created much earlier than the timestamp on its first message. Finally, theageing of the results of, for example, references to identifiers bound to channels inenvironments, will result in the value of tv growing larger without changing that of t ch 'However there is one point at which it is desirable to enforce a relationship between
tv and tch and that is when channels are created via a ConsCh. The required relationshipis that tv be no bigger than t ch ' or in other words that the channel has not been createdafter the time denoted by its first message timestamp. The desired interpretation of
message timestamps in channels is that they denote the time at which the message
containing them is first available to be referenced. Clearly any channel which is createdat time tv cannot be referenced before tv and therefore neither can any of its messages.
It is clearly nonsense to allow a program to decide at time 10 (tv) that it will produce a
message at time 5 (t ch )'Thus to allow a channel to be created of the form
(5.20)

would obviously be undesirable since the message cannot be used until after tv (and99

thus after t ch )' Of course after a channel has been constructed no such restriction can be,or should be, enforced for the reasons given above. After a channel has been constructed
the desired restriction is simply that the channel message cannot be referenced before
time t ch ; when the message actually is referenced is the responsibility of whatever isreceiving the channel. The implicit assumption is that external hardware devices will
always use messages as soon as they receive them.
Operationally a ConsCh can be viewed as constructing its result in two parts: fIrstly,
the atomic data value and the numerical timestamp arguments are evaluated to form theinitial message; after the message is sent the third argument is evaluated to provide therest of the channel. The defmition of ConsCh given below is also partitioned in this way:
( 5 .21) below defInes how the first message of the channel is evaluated; the rest of thechannel, denoted by rest in (5.21) is dealt with in (5.22).
~ [ ConsCh (E l , E 2 , E 3 ) ]Pc(5.21)

after (~<t l , vl>~ ~<t 2 ,v 2 > ~ (v2

:$;

t

~

<00,1->, <t,ch»

~

~,

where
<t,ch>

Note that unless the timestamp value, V2' denotes a time at or after completion of the
ConsCh the <00,1-> element of W~ results.

rest(5.22)<t"-(v 2+1),v">

where<t",v">~<t 3 , v3>
~

~

v3

<t',[a',lift(ch')]>~(t'~t3~

A t' > V2<t', [a',lift(ch')]>, <00,1->

Note that E3 evaluates to an element of @rn&m embedded in W~ and not merely an100element of ©~. IT the timestamp of the fIrst message in V3' t', is no bigger than V2 oris less than t 3 then the value of rest is the <00,..1> element of @J"M\m. t' must be bigger
than V2 to maintain the restriction that message timestamps in a channel must be strictlyincreasing. t3 is the time at which the channel denoted by E3 was referenced by the
ConsCh, which will be after the time at which the channel was first created because ofageing. IT t' is smaller than t3 then at least the fIrst message in the channel will not be
available for use at the time denoted by its timestamp. Finally, note that the value of thefIrst message timestamp in rest is adjusted in line with the incremental interpretation of
message timestamps.

Channels are referenced via HeadCh, Time and TailCh.
~ [ HeadCh (E 1 ) ] P c(5.23)

after (~

<tl'v 1><t, [a,lift(ch)]> ~ <max(t1,t),a> ~The result of a HeadCh becomes available after the maximum of the semantic timestamp
and the message timestamp of the fIrst message in the channel. Operationally the resultof a HeadCh cannot become available until both the channel has been computed and it has
produced a message. The definition of Time is similar.
~ [ Time (E 1 )](5.24)

P cafter (~

<tl'vl><t, [a,lift(ch)]> ~ <max(t1,t),t> ~TailCh is slightly more complex since the first message timestamp in the tail of thechannel must be replaced with the time it actually represents under the incremental
interpretation of message timestamps.

101

~ [ TailCh (E 1 ) ] P c(5.25)

after (~

<t 1 , v 1>
<t, [a, lift (ch) ] >~<max(t1,t), <t'+t+l,v'> >where<t',v'> = ~ ch : <t r , [ar,lift(ch r )]>~<t r , [arT lift (ch r ) ] >~,The time at which the result of a TailCh becomes available is after the maximum of thesemantic timestamp of the channel and the first message timestamp in the channel.
Operationally, the ftrst message in a channel cannot be discarded until both the channel
has been identifted and its ftrst message received.

5.4.2 The Ready test

One reason for using herring-bone domains was to enable the Ready function to be
specifted as a non-blocking test on a channel. The basic principle is that if a channel is
undeftned at a time greater than the Ready test is checking for then Ready can timeout thechannel. It must be remembered that the Ready test is a test upon user defined message
timestamps and not upon the semantic timestamps. If a Ready test is supplied with a<t, 1.> element of W~ it cannot timeout on the basis of t since t has no connection withthe values of the message timestamps. Operationally a <t, 1.> element of W~~
corresponds to the situation that the expression identifying which channel is to be tested
has not yet been evaluated. Clearly a Ready test cannot timeout the channel if it has not
yet even identified which channel it is testing.
The definition of Ready is given overleaf and can most easily be explained byconsidering each labelled case of the ~\5@Jli1 ... ~~\5li1 ... construct in tum.

102

~ [

Ready (E l ,E2 ) ]

Pc(5.26)

after<t l , v l >

~

~

~

<t 2 ,v2>~(i)(~'If,@lID. v

l~~{5.lID.

<t,.1>
~

(t

(ia)

> v2
~<max(tl,t2,v2),false>,(ib)<max(t l ,t 2 ,t),.1>( ii)<t, [a, lift (ch) ] >
~

(t

> v2

(iia)

~<max(tl,t2,v2),false>,(iib)<max(t 1 ,t 2 ,t),true>>>>~,

The channel is <t,.1> : no message has been produced up to time t, though a(i)message could still be produced at time t. There are two sub-cases to consider.
(ia)t> V2 : the channel did not produce a message before, or at, the time being

tested for and consequently the channel can be timed out and the result of
the Ready test is false. The result is produced at some time after the
maximum of the time at which the two arguments to the Ready test arecalculated and the time which is being tested for since, operationally, Readycannot return a result until its arguments have been calculated and thetimeout time has passed.
(ib)t~ V2 : the channel has not yet produced a message but it cannot be timedout since the testing time has not yet passed. The result of the Ready test isthus undefined with a semantic timestamp after the maximum of the time atwhich the two arguments to the Ready test are calculated and the time bywhich the channel has not produced a message.

(ii)

The channel is <t, [a, lift (ch)] > : a message has been produced at time t.
103

Once again there are two sub-cases to consider.
(iia)

t

> V2 : the channel did not produce the message before, or at, the time

being tested for. The result is identical to that for case (ia) since thechannel will be timed out by the Ready test.
(iib)

t

~ V2 : the channel produced the message before, or at, the time being

tested for. The result of the Ready test is true at the maximum of the time atwhich the two arguments to the Ready test are calculated and the time atwhich the message arrived since, operationally, Ready will return a result assoon as its arguments have been calculated and the message arrives.

(ia)and (iia) are the most interesting since they show how the non-blocking,timeout behaviour of Ruth is specified in the semantics.

5.4.3 Tuple construction and reference

The only other channel operators are those connected with tuples. Tuple construction
is defined as follows.
~ [{E 1 ... En} ] P cafter«O, {<t1,ch 1 >,(5.27)... , <tn,ch n >}>, cO)

The times at which the channels are identified have no bearing on when the tuple isactually constructed. The result of a tuple construction becomes available at the first timeread from the clock; operationally at some time after evaluation of the tuple
construction commences.
Elements of a tuple are referenced via the ! operator which is defined overleaf.

104

~ [ El ! E2 ] P c(5.28)

after (~

<tl'v 1>~~

<t 2 ,v 2> : <t 2 ,i>~(1 ~ i ~ m ~ <max(tl,t2,ti),chi>,<~,~»

where{<t1,ch 1 >,... , <tm,chm>}

v1

>>>
~,

The result of a tuple reference becomes available at some time after the tuple isconstructed and the channel being referenced is identified. Note that tuple elements areindexed from one and if the index number defined by E2 is not within the required range
the result is <~, ~>.

5.4.4 Process definition and application

The major reason for considering process definition and application here is to show
how the semantics of Ruth correctly specifies the essential real-time requirement of thelanguage: that message timestamps denote the earliest time at which messages become
available for use at their destinations. Such a check was used in the definition of ConsChand, since a new message in a channel is available for use within the process perfonning
the ConsCh as soon as the ConsCh is completed, that check is sufficient to ensure thereal-time requirement provided the channel is never communicated to another process. If
the channel being constructed is being communicated to another process then simply
checking when the channel is constructed will not be sufficient.
To illustrate this consider the following process definition.

Process P Input I Clock c Is {I} ;(5.29)

When I is constructed in its origin process its message timestamps will be checked toensure that its messages can be delivered to P within the deadlines they denote. P simply
passes I on unchanged so that there is a possibility these deadlines will have passed
105

before I'S messages can be delivered to their ultimate destination. A check must be madein p to ensure this does not occur and the obvious place to make this check is when amessage is transmitted from p to another process. In the semantics this is modelled in thedefinition of process application via the function filter (see (5.32) below).

Firstly, let us consider process definition which is defined using the semantic
function t; (evaluate process).
Proe

~

ENV

(5.30)e [Process I Input 1 1 " .I n Clock Ie Is E ]
p

[I

~

<O,f>]

wheref= AO se ·A0 1 ,

Ev[E]

...

AOn.AOpe .

([1 1 ~

D1 ]& ••• & [In

~ Dn]

& [Ie

~ Dpe]) Dse

Here P roc is the syntactic domain of process definitions. Evaluation of a process
definition results in an environment in which the process function it denotes is bound to
the process's name. Because we wish to store the process function in an environment
we must turn it into an element of W~ by adding a semantic timestamp of 0 indicatingthat the process function is defined at the start of evaluation of the program.
Operationally a process function is loaded before the program begins to run andtherefore is available for access at time o. Dse and Dpe denote that two clocks are required
as arguments to the process function: Dse is the semantic clock which is used to provide
timing information to the semantics of the process function; Dpe is the program clock
which supplies timing information to the Ruth process itself. These two clocks will be
provided when the process function is applied.

Process application is defined overleaf using the semantic function epA (evaluate
process application).

106

Pr-App

epA [

~

ENV

11 ... Im = I~ @~ ~

ENV(5.31)(I 1 ... I n ) ] P c[1 1 ~ <0,ch 1 >] & ... & [1 m ~ <O,ch m>]

where
chj = ~ <tj,ch j > ~ filter(chj,O,clockafter(cj,max(t',t j ») ~<t', {<t 1 ,ch 1>, ... , <tm,ch m>}>= ~ lookup ( I, P)~f: <t, f>sc i 1 . . . i n <O,pc>

where
i k = lookup(Ik,P)
sc = extract (co'O)
pc = extract (c o ,l)Here Pr-App is the syntactic domain of process applications. The process function isretrieved from the environment produced by (5.3 0) and applied to its input channels.
The process application also extracts two sub-clocks from Co (converting one of theminto an element of W~, for use as the program clock, by adding a semantic timestamp of0) for the process function to use as its semantic and program clocks. Each of the output

channels is stored in environment which results from the process application. This
environment is referenced by the definition of process configurations, given in Appendix
2, to produce the result of a Ruth program. In order to store the channels in anenvironment they must be embedded in W~ and this requires the addition of an extra
semantic timestamp. The value of this extra semantic timestamp is°since the channels

can be identified by their destination processes as soon as the program starts running.
The earliest the process will be able to output any message is t ' , the time at which
the tuple of output channels is constructed. Consequently, when the real-time constraint
on each output channel's messages is checked by the function filter the starting time
for the checking is max (t ' , t j) ; t j is the time at which the process identifies the output
channel j. filter is defined overleaf.

107

filter@~ x NUM x @~ ~ ~ (5.32)

filterA(ch,n,c) .<t-n,v>

where
<t,v>

~

c

: <t c ' [lc' rc] >~~ch : <t, [a, lift (rest) ] >
~

(t c

~

~<t

t

+ n
+ n, [a,lift(rest')]>,

<~,~>

where
rest'

filter (rest,t+n+l,from(lc,t c ) )}})Each message timestamp is checked to ensure that it denotes a time greater than thecurrent time by testing it against the first time in the clock. Note the use of the argumentn to handle the incremental nature of channel timestamps. n denotes the value that must

be added to the fIrst message timestamp in the channel to provide the actual time that it
denotes; thus n is initially o. If the actual time denoted by the fIrst message timestamp in
the channel is no less than the current time, t c ' then the first message in the channel may
be output; otherwise the <~, ~> channel results.

5.4.5 Program clocks

As with the channel domain @m~, the clock domain @~~ is embedded in thedomain of expressible values W~~ and thus a clock has two types of timestamp, thesemantic timestamp denoting when the clock is identifIed and the "clock" timestamps
denoting the time values in the clock. There need be no connection between the semantic
timestamp associated with a clock and the first clock timestamp since the clock may
already have been instantiated by previous references to it.

108

Ruth has two operators on program clocks: HeadClk and TailClk.
~ [ HeadClk (E 1 )P c](5.33)

after(~<tl'v 1><t, [l,r]> ~ <max (tl't) ,t>~~,

The time of availability of a clock reference must be after the maximum of the time ofavailability of the clock and the actual time value read from it. This models the fact that avalue read from a clock is out of date as soon as it is obtained. A real-time programmer
should never fall into the trap of assuming that a value read from a clock denotes thecurrent value of real-time; it denotes what the real-time was at some point in the (more orless) recent past when the clock was actually referenced. In Ruth this situation can bemade worse by references to clocks which have already had their values instantiated, andso contain values for times from the past. The conclusion must be that real-time
programmers in general, and Ruth programmers in particular, should treat real-timeclock values with extreme caution.
~ [ TailClk (E 1 )]Pc(5.34)

after(~<t1,v 1 >~,Note here that the "tail" of the clock has a time of availability after the maximum of theidentification time of the whole clock and the first clock timestamp. Note also that thevalue in the root of the left sub-tree must be adjusted to be the time it actually denotes
under the incremental interpretation of clock values before this sub-tree is returned as theresult.

109

5.5 Conclusion

The purpose of this chapter has been to give a definition of the semantics of Ruth.
Such a semantics requires the use of a model that allows timing infonnation to be
expressed and, following [Broy 83], we chose to use a denotational semantic model
based upon herring-bone domains. An important consideration in specifying thesemantics of a real-time language is how to model the durations of machine operations.
The method chosen here was that of clock-driven timing because it offers a way ofmodelling operation durations and data dependencies without the necessity of specifying
low-level operational detail.
Without herring-bone domains it would have been impossible to define thenon-blocking nature of the Ready test; the best that could have been done would havebeen to use implicit time detenninance and natural language. The same is true of thereal-time restrictions upon channel construction and channel messages crossing process
boundaries.

In the next chapter we turn from the theoretical issues which have occupied Chapters

4 and 5 towards the more practical concern of using Ruth to program a real-time system,in this case a real-time computer game.

110Chapter 6 . Using Ruth: A Real-Time ComputerGame

6.1 Introduction

Real-time computer games are a type of real-time system which are often ignored byresearchers in the area. This is perhaps surprising since they are very useful vehicles fortesting out different approaches to the problem of constructing real-time software. In a
real-time computer game we are faced with the usual problem in real-time systems ofmaking events happen at the right time. Although the deadlines within which a gamemust react are relatively large, because games interact with humans and not machinery,the consequences of failure to meet deadlines could be disastrous : noticeable delays will
dissuade people from playing the game.
Whilst computer games impose the same type of real-time constraints as otherreal-time systems, they do have the advantage of being simpler to construct and test thanothers. For example an engine controller program would require the software designer tohave information about the workings of the engine being controlled. A computer gamecontrols only very simple hardware (i.e. input keys, a screen and a loud speaker) and,in a lot of cases, a standard VDU meets all the hardware requirements.

The game we shall consider in this chapter is called Minesweep and the complete
text of the program is given in Appendix 4. The major area of interest is in seeing how

Ruth copes with the real-time requirements of the game and consequently this
implementation abstracts away from issues such as driving the screen display in favourof concentration on the real-time issues.
In the next section we shall describe the game and in Sections 6.3 through 6.6 theRuth program which implements it. Finally, we relate what we have learned about Ruth
from the exercise.

6.2 Minesweep

Minesweep is played on a fifteen by fifteen square board. We refer to the positions
on the board as cells. There are three states which a cell may be in : null (indicated on theboard by '-'); mine ('*'); and scoring ('1' to '9'). A typical board is shown below.
- 4

(6.1)

* - - - 6
- --- 3 - - 8

- - - **

- - - - 2

-

-

-

8

1 3 - - - - - - 9 @* --* - - - - - 7 - 3- - - 9- - - - 56

* - - - - * - - -- - - 2* -- - - - - - -- - - - 3

Initially all the cells on the board are null. The player starts the game on the top,lefthand corner cell and then moves around the board either horizontally or vertic all y,scoring points by landing on the numbered cells. If the player, indicated by '@' in the
diagram above, moves one cell to his left he will score nine points. However if hemoves one cell to his right the game will be over since that cell is a mine and will "blowup" any player who lands on it. If the player moves one cell up or down nothing
happens since these cells are in the null state.
To make the game a little more difficult the cells periodically change state. Initiallythe interval between changes of cell state (that is, between the occurrence of one statechange and the next) is (about) 20 seconds; this value is referred to as the period. Inorder to prevent all the cells changing simultaneously a random factor of + half theperiod is added. Thus, initially, a cell will change state at random intervals of 20 + 10
seconds (i.e. between 10 and 30 seconds). Each time a cell changes state it decreases its
period by 0.25 seconds down to a limit of 2.5 seconds. Thus the longer the gamecontinues the faster the cells change state until they reach the limiting period of 2.5 ±1.25 seconds between state changes.
If the player is on a cell which changes state he is unaffected. That is, if the cellbecomes a scoring one he does not score any points and if it becomes a mine he is not112

blown up. The player must move onto a cell for its current state to have any effect on the
progress of the game.

A cell may change into anyone of the three states at random; its current state has no
bearing on what it's next state will be. (Note that a cell's new state may be the same as
it's previous state). There is always a SO% chance that a cell will be a scoring one but the
chance of a cell being a mine (referred to as the danger) varies as the game progresses.
Initially there is only a S% danger but this increases by O.S% each time the cell changes
state until it reaches a limit of 40%. Consequently the chances of a cell being null are
initially 4S% but this declines to a limit of 10% as the game proceeds.

It only remains to specify the implementation's real-time performance requirements.
A player may make moves as rapidly as he wishes, however the implementation need
only respond to player moves at 0.2 second intervals; any extra moves will be queued.
Thus the fastest the player can move on the screen is five times a second. Assuming thatthe player does not make more than five moves a second the response time to moves (thetime between his making a move and that move appearing on the screen) should be

O.OOS seconds. If the response time is large enough for the player to notice it this will
detract from his enjoyment of the game; O.OOS seconds should be a small enough delay.
Of course, in a real-time system it is impossible to guarantee that specified deadlines
will be met and recovery action in the case of failure must also be specified. In this casea failure to meet the O.OOS second window should result in the move appearing on thescreen as soon as possible after that time. Although failure to meet the deadline isundesirable not displaying the move at all would be worse : a system which responds
erratically to player inputs is bad enough, one which discards player moves wheneverconvenient would be disastrous.
Finally there is the obvious real-time constraint that cell state changes should appear
on the screen at the time specified by the cell. However, in cases where this deadline is
not met the state change will be ignored. Since a cell's new state may be the same as its
old state anyway this is an acceptable situation. Rather than display a state change later
than the time specified, the system assumes that no change of state occurred.
113

6.3 Overview of the implementation

6.3.1 System Configuration

The obvious way to implement the Minesweep board is as a set of processes, one
for each cell. The first thing we note is that there are 225 cells on the Minesweepboard. To avoid having to list all 225 cell processes and their associated channels weshall restrict this implementation to only 4 cells; this restriction does not effect thecomplexity of the system, merely the amount of processes and channels that must be
listed in the configuration.

The overall structure of the system is as below.

Minesweep
keyboard

keyboardf

Validate
Process-val

f - valscore

Monitor
Process
Cell
Process - n
rnd- nf - cell

rnd n

n

f

-

cell- nIn the above diagram the boxes represent processes and the arrows channels. Insteadof explicitly including all four cell processes and their input and output channels a single
Cell Process_n box (for 1 ~ n ~ 4) is shown; in the same way the fat arrows
represent the inputs and output channels, rnd_nand f _ cell_n for each cell process.

114

This system configuration is thus
Configuration Minesweep(6.2)

Output score, f_cell_l, f_cell_2, f_cell_3,
Input

f_cell_4, f val

keyboard, rnd_l, rnd_2, rnd_3, rnd 4

Is
score

f cell 1 = Cell Process (rnd_l);f cell 2

Cell Process (rnd_2);

f cell 3

Cell Process (rnd_3);

f cell 4 = Cell Process (rnd_4)

;

f val

Validate Process (keyboard)end.

6.3.2. System inputs and outputs

The Minesweep configuration takes the player's moves as input, via channel
keyboard, in the form of ASCII characters, and produces six channels: an f_cell_nchannel for each cell carrying the cell's state changes; score, which carries integers
representing the player's score so far; and f _val carrying integers representing the cell
the player has just moved to. We shall assume the existence of a hardware "process"which will display the original state of the screen (all cells null, score 0 and the player on
the top left cell) and will then display the output from score and f_cell_n on the screenin the required format at the times denoted by the message timestamps. This hardware
process will also display the player character, '@', on the cell indicated by the messages
in f _val; it is also assumed that the hardware process will never overwrite the player
character with a cell state in the case where the cell changes state whilst the player is onit.

It is simple to implement any screen driver we might require in Ruth but this would
unnecessarily add to the complexity of our system so we shall not do so here.

The tables below define the input and output formats. Table (6.3) defines the115characters the Minesweep system will receive from channel keyboard and the player
moves they denote; table (6.4) defines the integers sent on the f _ cell_n channels andthe cell states they denote.

Ascn Characterud1rInteger-1-2
1 to 9Player MoveOne cell upwards
One cell downwards
One cell left
One cell right(6.3)

Cell State
Null

(6.4)

Mine

Scoring cell

The system also takes four channels rnd_ n (1 ~ n ~ 4) containing random integers
in the range 1 to 1000. These are used to generate the cell state changes and the random
part of the cells' periods; the rnd channels are assumed to be always Ready, that is,always able to provide a message. Effectively the rnd channels produce messages in ademand driven manner.

Finally, the end of the game, (when the player lands on a mine) is signalled to theexternal world by the sending of a -1 message on channel score.

6.3.3.System processes

Validate_Process takes the player's moves from channel keyboard, checks that

he is not trying to move off the board and limits him to one move every fifth of asecond. Assuming the move is a valid one the player's new position is sent to theexternal world and to Monitor_Process along the f_val channel. The player's position
is represented by a number between 1 and 4 which identify cells as shown below
1 2
3 4

116

f_cell_n carries the state changes of cell n. Each Cell_Process computes a newstate at intervals defined by its period and communicates them along f_cell_n to theexternal world and to Monitor_Process. As mentioned in Section 6.2 the value of eachcell's period is reduced after each state change until a limit is reached, the input channel
rnd_ n being used to generate the variations in the value of the period.

The purpose of Monitor_Process is two-fold. Firstly, it takes the cell states and theplayer position as inputs from channels f_cell_n and f_val and uses this information
to calculate the player's score which it communicates to the external world via channel
score; secondly, it detects when the player moves onto a mine cell and sends a -Ionscore to indicate that the game is over.

As usual all of the processes also take a real-time clock as an input, though this is notshown on the diagram. It is assumed that in this system time is measured inmilliseconds.

The next four sections outline the actual Ruth code which implements the processes
outlined above. The complete text of the Minesweep program can be found in
Appendix 4.

117

6.4 The Validate Process
6.4.1 Overview

keyboard --..-t~

Validate
Process

....

f val

Validate_Process is the simplest process in the Minesweep system. It receives

the player's moves on keyboard, checks that they are valid, and if so sends the new
player position to the external world and to Monitor Process on f val.
Validate_Process will delay each move made by the player until at least 200

milliseconds after the previous move. This enforces the restriction that player moves are
only responded to at fifth of a second intervals. The structure of Validate_Process is
Process Validate Process(6.5)

Input keyboard
Clock cIs { Time_Check (output, c)}

whererecoutputValidate (keyboard, startyos, first_move)

startyos

1 ; first move = 0 ;Time Check = lambda (output, c) . . . . ;Validate = lambda (kb, pos, next_move).

endwhererec ;;Validate Process

Note that the single output channel from Validate_Process is enclosed between' {'and '}' to embed it in a tuple.
Validate Process is made up of the functions Time_Check and Validate.
Validate takes as its arguments the keyboard input, the player's starting position (cell1) and the next time at which the player is allowed to make a move (initially 0).
Validate checks that the player is not trying to move off the board and ensures there is

a 200 millisecond gap between messages. The result of Va 1 i da t e is a list of118

[playeryosition, time_of_move] pairs to be sent as channel messages in f_val.

The output supervisor Time_Check takes this list as an input argument and checks it
to ensure that time_of_move is late enough to be used as a messages timestamp, (i.e.
that the time it is to denote has not already passed so that the message will be timed out).
If time_of_move is late enough for the message to be sent this is done, if not themessage is sent with time_of_move replaced by a timestamp large enough to avoid
timeout. Time_Check is a simple example of defensive programming: if Validate
misses a deadline Time_Check takes correcting action.

6.4.2 The Validate function

Validate passes the keyboard input onto the function Check_and_Move forchecking; the result returned by Check_and_Move being the number of the cell that theplayer is on after the move is completed (if the move is invalid Check_ and_Move returns
the current position). Check_and_Move is straightforward and will not be further
discussed here; the reader is referred to Appendix 4 for details.
Function Validate is thus
( 6 . 6)

Validate
lambda (kb, pos, next_move).
If newyos = pos

Then Validate (TailCh(kb), pos, move_time + interval)
Else Cons(Cons(new~os,

move_time),

Validate(TailCh(kb),new~os,

move time + interval))
whererec200 ;comp_delay

5 ; interval

newyosCheck and Move (move, pos)

move

HeadCh (kb) ;move time

If

T~

=

(kb) + comp_delay < next move

Then next move
Else

T~

(kb) + comp_delay;

endwhererec ; -- Validate
next move is the earliest time at which the next player move can be output from119

Val ida t e _P roc e s s

and is 200 milliseconds after the last output from

Validate_Process. If the player attempts to move to another cell within 200

milliseconds of his last move Validate_Process will not forward the move until
next_move, effectively restricting the player to one move in every 200 millisecond

period.
comp_delay allows for the time between Validate_Process receiving the player's

move and being able to output the new position on f_ val. When specifying theMinesweep system 5 milliseconds were allowed for this. If, in a particular case, morethat 5 milliseconds elapse so that move _time is not a valid timestamp this will be
detected by Time_Check and the appropriate action taken.
It is because of this uncertainty about the validity of move _time as a message

timestamp that Validate returns a list of pairs instead of a channel. If a channel wereused there is a potential for it to be timed out and no more player moves would beprocessed. Instead the process is written defensively: channels are only constructed
after their message timestamps' validity has been checked; this is done by the output
supervisor Time_Check.

6.4.3. The Time Check function

Time_Check checks each of the potential message timestamps in the list produced by
Validate against the current time read from the clock c, replaces those that are too early

to be used as message timestamps and constructs a channel of player positions to be sent
to the screen driver and to Monitor_Process. The Ruth code for Time_Check is given
overleaf.

120

Time Check
=

(6.7)

lambda (output, c).
If out time ~ soonest
Then ConsCh (out_data, out_time,
Time_Check (Tail (output) , TailClk(c)))
Else ConsCh (out_data, soonest,
Time Check (Tail (output) , TailClk(c)))
whererecout time

Tail(Head(output)) ;out data

Head(Head(output)) ;soonestHeadClk (c) + check_delay ;check_delay

1;

endwhererec;

Time Check

Note the use of check_delay to allow for the time taken after the clock is read toconstruct the channel and to output the message. Even when timestamps are checked asabove it is impossible to guarantee that messages will be sent: there may be a longer
delay than allowed for by check_delay before an attempt is made to output the message
so that a timeout will occur. However the situation is not as bad as it might appear since
Time_Check is a fairly small and simple function and we can be fairly certain thattimeouts will not occur.
The bigger the value of check_delay the more probable that timeouts will not occur,
but, on the other hand, the earlier that Validate will have to produce a result to avoid
Time_Check taking its error recovery action. The compromise taken here is that
Validate should produce its result with 20% of its allotted time (i.e. 1 millisecond)remaining to allow time for Time_Check to operate. Of course, this is just an informed
estimate of the amount of time that will be required for Time_Check, and will be
modified if it proves to be too big or too small. Estimating delay values in this way iscommon practice in the real-time field.

Time_Check is a passive output supervisor in that it waits for Validate to produce

messages for output and then checks them for validity. In Time_Check messages whichhave missed deadlines are simply re-timestamped, though other strategies, for example
discarding any incorrect messages, are obviously possible. However, all a passive121

output supervisor can ensure is that messages which have missed deadlines are not sent
(i.e. that events do not occur at the wrong time). In many cases it is desirable to send amessage to meet every deadline, even if the message does not denote the required event,and this requires an active output supervisor. An active output supervisor monitors theprocess's output, waiting for the deadline and sending a default message if the "real"
message is not produced by the deadline. This ensures that an event will occur at therequired time, even if the event is not the exact event required.
An active output supervisor is not required in the case of Validate_Process since
failures to meet deadlines are not very serious: processing player input is a soft real-time
problem. However it would be straightforward to provide Validate_Process with anactive output supervisor by passing f_val to process Active.
(6.8)

Process Active
Input f val
Clock cIs Check(f_val, c, 0)
whererecChecklambda (f_val, c, last_output).
If Ready (f_val, last_output + allowed interval)
Then ConsCh (HeadCh(f_val), out_time,

Check(TailCh(f_val),TailClk(c),Time(f_val)))Else ConsCh (default, out_time,
Check(f_val,TailClk(c),out_time))
whererecout time

HeadClk(c) + check_delay

default. .. ,

allowed interval

1000 ;

check_delay

5 ;endwhererec ; -- Check
endwhererec; -- Active Process

The Check function monitors the f _val channel and if too great a time elapses between
messages (in this case 1000 milliseconds) assumes that a timeout has occurred and sends
the default message. Otherwise received messages are passed on unchanged, apartfrom having their timestamps updated.

122After a timeout has occurred process Check simply carries on monitoring f_val
although once a Ruth channel message has been timed out the channel will never containany more messages. What we would prefer in such situations is that Check be able tosend a message to the timed out process instructing it to reinitialise itself. Unfortunately,
it is likely that any process which has had a channel message timed out has itself crashedand would thus not respond to such an instruction. The obvious solution is to simply
create a new instance of the process but Ruth does not allow dynamic process creation.
This restriction should be removed in later versions of the language and dynamic processcreation is discussed further in the conclusion of this chapter and in Chapter 7.

1236.5 The Cell Processes

6.5.1 Overview

rnd

~

Cell
Process ;---II.~ f cell

- - - t I I..L..._ _ _ _ __Each cell process periodically calculates a new state and communicates it to theexternal world and to Monitor_Process via its f_cell channel. The frequency withwhich new states are computed depends upon the cell's period value and upon a random
number input from channel rnd. The period value is decremented after each new state iscomputed until it reaches a limit of 2500 milliseconds; thus as the game progresses thecells change state faster and faster.
The states computed also depend on a random number read from rnd. If that value is
500 (50%) or over the cell will be a scoring one; otherwise the chance that the new state
will be mine or null depends on the cell's danger value, the higher the danger the morechance that the new state will be mine. The danger value is incremented after each statechange, up to a limit of 400 (40%).
( 6 . 9)Process Cell Process
Input rnd
Clock cIs { Time_Check (output, c)}

whererecoutput = Cell (rnd, 0, init_state, init_danger, init_period)

Time Check

lambda (output, c) . . . .

init state

null

init_danger

50

limit_danger

400

inc_danger

5

inityeriod

20000;

limityeriod

2500;

decyeriod

250;;

null = -1;

mine = -2

Cell = lambda (rnd, last_out, state, danger, period) . . . .
Calculate State = lambda (n,danger)
endwhererec ; -- Cell Process
124

... ,

Cell_Process is similar in structure to Validate_Process. The list produced by Cellis checked for the validity of its time values by the passive output supervisor
Time_Check. It is unlikely that timing errors will occur because the fastest a cell needever produce messages is once every 1250 milliseconds; nonetheless the check is
included for safety.

6.5.2 The Cell function

Cell takes as arguments the channel rnd, last_out, the time of the last statechange, the current value of the state and the current values of danger and period andproduces as its result a list of [state, time_of_change] pairs.
Cell(6.10)
lambda (rnd, last_out, state, danger, period).
If new state = state
Then Cell (TailCh(TailCh(rnd», out_time, state,
new_danger, new-period)
Else Cons (Cons (new_state, out_time),
Cell (TailCh(TailCh(rnd», out_time, new_state,
new_danger, new-period»
whererecout time

last_out + period +«HeadCh(rnd) - 500)

* period)/ 1000 ;new stateCalculate State(HeadCh(TailCh(rnd»,danger)

new-period

If (period - dec-period)~

limit-period

Then limit-period
Else period - dec_period ;new_danger

If (danger + inc_danger)~

limit_danger

Then limit_danger
Else danger + inc_danger
endwhererec ; -- Cell

The Cell function uses the Calculate_State function to produce the new states
and builds them into a list of [state, time of change] pairs. Calculate_State isstraightforward and will not be discussed further; the reader is referred to Appendix 4

125

for details. Note that both the time of the next state change and the new state depend on arandom number input. Note also the limiting of the values of the danger and period tolimit_danger and limityeriod respectively.

6.5.3 The Time_Check function

The Time_Check function used in the cell processes is almost identical to that used in
Validate_Process; the only difference being the action taken when a timing error isencountered.
Time Check(6.11)

lambda (output, c).
If out time ~ soonest
Then ConsCh (out_data, out_time,
Time_Check (Tail (output) , TailClk(c»)
Else Time Check (Tail(output), TailClk(c»whererecout time

Tail(Head(output»out data

Head(Head(output»

soonestHeadClk (c) + check_delay

check_delay

250;

endwhererec;

Time Check

Whenever the Cell function defines a state change to occur at a time that is too early for
Cell_Process to be sure of sending the message in time the state change is simply

discarded. Since it is always possible for the cell's new state to be the same as its oldstate this is a safe strategy for error recovery.
The smallest interval between two successive state changes is 1250 milliseconds andconsequently we would expect timing errors to be infrequent. In Validate_Process
20% of the available computation time was assumed to be reserved for the Time_Check
function; here 20% of the minimum available time is allocated to Time_Check and thus
check_delay is 250 milliseconds. As with the check_delay value used in Time_Checkin Validate this value is an informed estimate based on real-time domain experience.

1266.6 The Monitor Process
6.6.1 Overview

f val
Monitor
Processscore

f cell n

Monitor_Process takes as input the player's moves from Validate_Process (viaf_val) and the state changes from each each Cell_Process (via the f_cell_nchannels). Each time the player moves it calculates his new score and, if the score haschanged, sends the new score along channel score. If the player moves onto a mine cell
Monitor_Process infonns the external world by sending -1 along score.

Process Monitor Process
Input f_cell_1, f_cell_2, f_cell_3, f_cell_4, f val
Cl.ock c
Is { Time_Check (output, c)}

whererecoutputMonitor (inputs,init_state,init-player-pos,init_score)

inputsScan and Sort (f_cell_1, f_cell_2, f_cell_3, f_cell_4,
f_val, in it scan);

init-player-pos

1

in it scoreoinit scan

200 ; scan interval

200 ;

mine

-2

-1

in it state; null;Cons(null,Cons(null,Cons(null,Cons(null,Nil))));

Time Checkl.ambda (output, c) . . . . ;Scan and Sort

l.ambda (f_cell_1, f_cell_2, f_cell_3, f_cell_4,
f_val, scan_time)

Monitorendwhererec;. . .. ,= l.ambda (inputs, state, player-pos, score)....

Monitor Process

Monitor Process operates III much the same way as Validate Process and127

Cell_Process in that it uses a passive output supervisor Time_Check to check a list of[score, time] pairs before converting them into channel messages. The input channels

to Monitor_Process are timewise merged into the list inputs by the function
Scan_and_Sort; thus the earlier a message arrives at Monitor_Process the earlier it

appears in inputs. This simplicity in ensuring that events are processed in the order
they occur is a major advantage of the explicit timestamps used by Ruth.
The list of [score, time] pairs is produced by the function Monitor which takes as
its arguments the list inputs, the state of the board (initially all the cells are null), theplayer's current position (initially on cell 1) and the current score (initially 0). Monitor
works down the inputs list processing each message, and thus each event in thesystem, in the order in which they occurred. Each cell state change message results inMonitor updating its state value; each player move results in the score being updated

if the player moved onto a scoring cell, the sending of -1 if the player moved onto amine, and no message at all if the cell is null.

6.6.2 Getting the inputs

The Scan- and- Sort function operates in exactly the way its name implies.
Periodically it scans all the input channels and builds a list of all the messages that
arrived since the last scan. Scan_and_Sort assumes that only one message can havearrived from each of the other processes since the last scan. In order to ensure thisScan_and_Sort must scan the channels at least every 200 milliseconds. This is thesmallest possible interval between messages on f _val. None of the other channels willproduce messages as fast as this so this is the limiting case.
The general principle behind Scan_and_Sort is that all the input messages available
at this scan time are collected into an event_list which is then sorted by order ofoccurrence of the events they denote (earliest ftrst). The resulting list is appended to thelist resulting from recursively applying Scan_and_Sort to the input channels with themessages already received removed. Thus the result of Scan_and_Sort is a list
containing all the events reported to Monitor_Process in order of their occurrence : a128

timewise merge of its inputs.
Scan_and_Sort=(6.12)

lambda (f_cell_l, f_cell_2, f_cell_3, f_cell_4, f_val,
scan_time) .
Append(Quicksort(event- list , Nil) ,Scan_and_Sort(new f cell l,new f cell 2

--

-

--

-'

new_f_cell_3,new_f_cell_4,
new_f_val,scan_time + scan_interval»

whererecevent list
Get Events ({f_cell_l, f_cell_2, f_cell 3,
f_cell_4, f_val}, 5, scan_time»

new f cell 1

New Chan (f_cell- 1, scan_time)

new f cell 2

New Chan (f cell- 2, scan_time)-

new f cell 3

New Chan (f- cell 3, scan_time)-

new f cell 4

New Chan (f- cell 4, scan_time)-

new f val

endwhererec=;

New Chan (f_val,

;

;

;

scan_time)

Scan and Sort

Here Append is the usual function for appending two lists and Quicksort performs
a quicksort on the event_list according to the timestamps of the messages. Function
New_Chan simply returns the TailCh of its channel argument if it is Ready at the timedenoted by its second argument. Thus it discards all messages which have been
incorporated in event_list in this scan. For the text of these functions the reader isreferred to Appendix 4.

Because all the events are combined into one list they must be tagged to show their
origin. Thus every element of event_list is a pair comprising an origin tag and theevent itself. To tag the events we use the index of their origin channel in the list of inputs
to Monitor_Process, starting at 1. Thus f_val events are tagged 5. Note that the event
itself is a pair whose fIrst element is a new cell state or the cell that the player has moved
to, and whose second element is the timestamp of the message. The tagging is
performed by the function Get_Event when it reads the messages from the input
channels.
129Get Events(6.13)

lambda (chs, n, t).
If n < 1
Then Nil
Else If Ready(chs!n, t)
Then Cons(Cons(n, event), Get Events (chs, n-1, t)Else Get Events (chs, n-1, t)

)

;

where
event = Cons(HeadCh(chs!n),T~(chs!n)) ;endwhere ; -- Get Events

Get_Events

collects the messages which have arrived since the last scan;

Quicksort sorts these messages into order of arrival. Since there are so many input

channels it is clearer and simpler to separate these two operations from each other than to
combine them into one function as is done be the timewise merge functions seen earlier.

6.6.3 The Monitor function

The Monitor function works down the list of events inputs, processing the eventsin tum and updating the score and state of the cells in accordance with each event.
(6.14)

Monitorlambda (inputs, state,player~os,

score).

score out
whererecevent

Head(inputs)

event_type

Head (event)

event data

Head(Tail(event»

event time

Tail(Tail(event»out time

event time + comp_delay

comp_delay

50 ;score out

;
;
;

;

endwhererec ; -- Monitor

Monitor takes the first event in the list of events inputs and decomposes it into130

event_type, event_data and event_time. event_type is the tag attached to theevent by Scan_and_Sort and so denotes the origin of the event message. event_data
is the data part of the message denoting a new position if the event came from the player
and a new state if the event originated from a cell. event_time is the time the event
occurred.
The updated score is output at out_time which is 50 milliseconds after the event
actually occurred. This allows for the time involved in processing the message within
Monitor_Process, though if 50 milliseconds proves to be too short a time the output

supervisor will trap the error.

score out is calculated as follows

score out

If Lookup (new_state,new-player-pos)mine(6.15)

Then Cons (Cons(-l,out_time), Nil)
Else If new score* scoreThen Cons (Cons(new score,out_time), rest)
Else rest

restscore out

Monitor(Tail(inputs),new_state,new-player-pos,new_score)

new score = ... ;new-player-pos =new state

=

...

;

Lookup = lambda (table, n) . . . . ;Here new score is the the updated value of score, new-player-pos is the new player
position and new_state is the new cell state list. If the event was a player move thennew state will have the same value as state; if the event was a cell state change thennew_score and new_player-pos will have the same values as score and player_pos

respectively. Lookup returns the nth element of the list table. These definitions are
straightforward and the reader is referred to Appendix 4 for details.
Note that if the player lands on a mine, so ending the game, the pair [-1, out_time]is produced followed by Nil. Since the game is over Monitor processes no more
events.

131

6.6.4 The Time_Check function

The output supervisor for Monitor_Process is similar to that for the other two
process, the only difference once again being its behaviour in the advent of timing
errors.
Time Check(6.16)= lambda (output, c).
If out time ~ soonest

Then ConsCh (out_data, out_time,
Time_Check (Tail(output), TailClk(c)))
Else ConsCh (-1, soonest, stop)whererecout time

Tail(Head(output)) ;out data

Head(Head(output)) ;soonestHeadClk (c) + check delay

stop

ConsCh (-1, 0, stop) ;check_delay

10 ;endwhererec

Time Check

When a timing error is detected Time_Check terminates the game. A more sophisticatedstrategy, such as sending the score as soon as possible in a similar way to
Validate_Process, is obviously possible. However, since Monitor_Process is themost important process in the Minesweep system we choose to regard any timing
failures within it a fatal errors. The most useful course of action would be topre-emptively reinitialise the whole system but Ruth provides no primitive forpre-empting processes.
Instead Monitor_Process produces the -1 message, so ending the game, andceases to process messages. There is no elegant way of terminating a channel in Ruth
since it is slightly unusual for a real-time system ever to terminate. The only way toachieve the desired effect is with the recursive definition of stop above which willproduce a timeout error since it attempts to use a zero timestamp. Note that 20% of theavailable computation time (i.e. 10 milliseconds) is reserved for Time_Check.This
ensures, as far as is possible in a real-time system, that the -1 message will not be timedout but will be received by the external world. Once again, the value chosen for132check_delay is an infonned estimate and may change as a result of experiences running
the implementation.

The total delay between messages reaching Monitor_Process and the production ofa message in response is 50 milliseconds. Thus when the player makes a move anychange in his score will not be visible to him for 55 milliseconds: a 50 millisecond delay
in Monitor_Process and a 5 millisecond delay in Validate_Process. As far as theplayer is concerned his moves occur when he presses one of the lUI, 'd', 'I' or 'f 'keys;
as far as Monitor_Process and the external world are concerned the player actually
makes his move 5 milliseconds after a key is pressed, and he is not credited with anyscore for the move for a further 50 milliseconds. However, as far as the user isconcerned, cell state changes occur when they appear upon the screen and thus, to theuser, there seems to be an unfair delay in processing his moves.

A partial solution to this problem would be to delay cell state changes by 5
milliseconds in the Scan and Sort function. Thus the state of the board held in
Monitor would always be consistent with a 5 millisecond delay on both the player

moves and the cell state changes and the player would not find himself moving onto amine cell which was not a mine when he made the move. Unfortunately this would beinconsistent with what actually appeared on the screen as a cell would appear to change
state 5 milliseconds before the new state had any affect on the progress of the game.
There is no total solution to this problem since it is caused by the player's perceptionof reality : a cell changes state when the new state appears on the screen; the player
moves when he presses a key. Such problems with the perception of when events occur
are common to real-time systems and derive from the fact that it takes time for acomputer to process its inputs and produce its outputs. There is no way that a real-time
program can ever have a totally up to date picture of the external world and this issomething that the real-time programmer must learn to live with.

This completes the definition of the Minesweep implementation. To see how it all
fits together the reader is once again referred to Appendix 4 where the full text of the133implementation is given.
In the next, concluding, section of this chapter we shall examine and evaluate oursolution to the problem of implementing the Minesweep specification.

1346.7 Conclusion

The purpose of this chapter has been to evaluate the suitability of the language Ruth
for implementing real-time systems by applying it to a substantial real-time problem. The
problem chosen was the real-time computer game Minesweep. Computer games
exhibit fairly complex real-time behaviour but have the advantage of requiring no
specialist knowledge to implement and/or explain.

The emphasis has been upon the real-time problems posed by Minesweep and thesuitability of Ruth for expressing solutions to these problems. Consequently we haveabstracted away from several non real-time issues: for example how the screen is to be
driven and where the random number inputs are generated.
It could well be argued that we have been somewhat pedantic in specifying real-time
behaviour in the Minesweep program. A computer game interfaces to a human as
opposed to machinery and human reaction times are very slow in comparison to amachine's. (i.e. seconds rather than milliseconds). Thus a real implementation of
Minesweep could probably dispense with the Quicksort function in Scan_and_Sort
and simply treat all the events detected in a scanning phase as happening simultaneously.
This strategy would, however, lead to several discrepancies in the real-time behaviour ofthe system. For example Monitor_Process could receive two messages in a scan: theplayer moves off cell n, and cell n changes state from a scoring cell to a mine. If both
events are assumed to occur simultaneously then the game is over since the player has
landed on a mine. However the player could have moved onto the cell before the cellchanged state in which case his score should be increased by the relevant amount.
Although it is very unlikely that the player would notice any discrepancies in thereal-time behaviour of a Minesweep implementation given the very small (to a human)time periods involved, in a narrow real-time system such discrepancies would be"noticed", and could have disastrous effects. To maintain consistency of real-time
behaviour requires that the real-time language used be able to detect exactly when eventsoccurred or did not occur, and the ability to specify exactly when events should occur:in other words time expressibility. By checking the timestamps on channel messages
135using Ready and Time the Minesweep program maintains the consistency of its
real-time behaviour.

The Minesweep program also exhibited the use of defensive programming
techniques in Ruth : each process's output was checked by the Time_Check passive
output supervisor. However a passive output supervisor is not a total solution to thedefensive programming problem since it can only prevent incorrect messages being
output; it cannot output default messages to ensure that deadlines are always met.
Although it is possible to write active output supervisor processes in Ruth there is noway in the functional framework for such a process to preempt a rogue process andforce it to take corrective action. The obvious solution is simply to create a new versionof the process and ignore the rogue but Ruth does not allow dynamic process creation.
In the next chapter we shall look at a way in which this situation could be improved.

Ruth's insistence on the explicit naming of all channels and processes in aconfiguration causes problems with handling large numbers of processes and channels.
This led us to restrict the Minesweep board to only four cells.
The handling of channels within the language generally is definitely an area which
could be greatly improved. The only data structure available for use with channels is thetuple and a tuple can only be constructed by listing all its elements. There is no operation
like Cons on s-expressions which would allow us to add channels to tuples and thus wecannot write recursive functions that "map" down tuples to produce other tuples. This
restriction was particularly felt in Monitor_Process, for example in the separate
definitions of new- f - cell- 1 through new_f_val in Scan_and_Sort.

The problems mentioned above are largely peripheral to the central goal of Ruth
which was to prove that there is no reason why a purely functional language could not
be used for writing real-time systems. The Minesweep program suggests that we havesucceeded in this aim. Although certain features of the language could be improved thosedealing with specifically with real-time (channels, clocks and their associated operations)
are more than adequate for dealing with real-time systems.

136

In the final chapter of this thesis we shall make a fuller review of what has beenachieved in this work. In particular we will consider future directions for the work, bothin terms of language improvements and theoretical issues.

137Chapter 7 · Review, Assessment And Future Work

7.1 Review

7.1.1 What is a real-time system ?

A real-time problem can be classified as one in which when events occur is as
important as what events occur. A further refinement can be made along two axes : theamount of time a system has to react to an event and the scale of damage if thesedeadlines are not met. The importance of when things happen in a real-time system has
two major implications : the system must specify when it wishes events to happen and it
must be able to detect when events have happened. Thus, any language used for the
implementation of real-time systems must have what we have called time expressibility :the ability to express facts about time.

The timing constraints inherent in real-time programming also have a major impact
on the type of algorithms that are used. Real-time programmers tend to program in avery defensive manner: if there is the slightest doubt as to whether a program will meetits constraints then it is rewritten. In most real-time systems the time-critical part of thesoftware can be expected to complete its tasks in as little as half the time available to it.
Even so, individual processes in a real-time system are usually written in such a way thatthe failure of another process to meet its time constraints can be recovered from. This
usually involves writing a large amount of error handling code which (hopefully) isnever executed.

7.1.2 Current approaches to real-time language design

In Chapter 2 we looked at three different approaches to real-time language design,imperative, dataflow and functional, and examined their relative merits in terms of time

expressibility and defensive programming. As a result of this survey two general types
of approach were identified: the pragmatic, defensive approach exemplified bylanguages such as Ada, and the theoretical, optimistic approach exemplified by
LUSTRE.
The defensive languages assume nothing about the real-time characteristics of aparticular language implementation and give no guarantees that deadlines will be met.
Instead facilities are provided to support defensive programming: software can monitor
its own progress in time and take recovery action if deadlines are not met.
The optimistic languages assume a particular real-time behaviour from language
implementations. For example LUSTRE assumes the strong synchrony hypothesis :machine operations take negligible time and deadlines are always met. Thus LUSTRE
provides no support for detecting and recovering from timing errors; the focus is upon
specifying the temporal behaviour required rather than whether that behaviour can beachieved. The other optimistic language considered, ART, assumes merely that the exact
time taken for each machine operation is known and thus that temporal behaviour can bepredicted from the semantics of the language. Although this is not as strong anassumption as strong synchrony it may well be equally unrealistic for many, more
complex, language operations; also, determining the real-time behaviour of a program
requires that the complete program be proved from the semantics which is a lengthy andpotentially error prone task at present.

Given that the strong synchrony hypothesis is unrealistic when working withreal-time systems, and that the current state of the art of program proving is not generally
practical, we are forced onto the defensive. The basic principles of the language Ruth
are thus those of a defensive language: nothing is assumed about an implementation's
real-time characteristics and the language provides facilities for monitoring progress intime and detecting and recovering from timing errors.

1397.1.3 The language Ruth

A Ruth program comprises a static set of processes communicating via streams of(numerically) timestamped atomic messages, in which each message denotes an event in
the system. Such streams are called channels in Ruth and each process is a function
mapping a tuple of input channels to a tuple of output channels.
The timestamp on a channel message defines when the message is required to arrive
at its intended destination (either another process or the external world) so giving the
Ruth programmer the ability to specify when events happen. For simplicity, we haveassumed no communications delays on channels and no clock skewing between
processes.
A process also takes a real-time clock stream as input. As the program executes thevalues in the clock stream are (lazily) instantiated with the current value of real-time, thus
allowing the programmer access to real-time information. This approach was firstsuggested in [Burton 88].
In order to detect the occurrence of an event Ruth supplies an operation for testing

the timestamp of the first message in a channel against an integer value: the Ready test.
Ready is a predicate which returns t rue if the timestamp of the first message in thechannel is less than or equal to the number being tested against and false otherwise.
The most important requirement of Ready is that it should be non-blocking, that is, thatthe event need not have happened (there need be no message in the channel) for Ready toreturn a result. In real-time systems the non-occurrence of an event by a particular time
carries (almost) as much information as its occurrence and Ready must be able to detect
this situation.

7.1.4 Herring-bone domains and clock-driven timing

To give a formal definition of operations such as Ready requires that the semantic
model used be able to express facts about time. The herring-bone domains used in [Broy83] to give the semantics of ART are just such a model and they were used to provide a140

framework for the semantic defmition of Ruth.
When dealing with the semantics of real-time programming languages one of themost important things that must be defined is when expressions produce results. In thesemantics of Ruth these times depended upon values read from a clock, an approach we
called clock-driven timing. Clock-driven timing gives a higher level of abstraction thanusing fixed durations for each machine operation (delay-driven timing) since there is noneed to fix such things as evaluation orders. Yet it more accurately models the real world
than assuming no delays at all (data-driven timing). Moreover, by constraining thevalues read from the semantic clocks in certain ways data dependencies can be expressed(e.g. the result of an addition cannot be available until after the two numbers to be added
are computed) without defining low level implementation details.

7.1.5 Conclusion

The next section of this chapter assesses the merits and failings of Ruth as areal-time programming language and suggests several improvements. Section 7.3
outlines a prototype implementation for the language. In Section 7.4 the focus is upon
theoretical issues and in particular upon what kinds of formal reasoning andtransformation are possible with real-time software. Based on this Section 7.5 indicatesa possible direction for future work.

141

7.2 Ruth As A Real-Time Programming Language
7.2.1 Time expressibility

Our primary goal with Ruth was to produce a purely functional programming
language for writing real-time software. The essential feature of a real-time language is
its time expressibility, that is, the data types for representing temporal information andthe operations on those data types. In Ruth time is represented by the integer values ofchannel timestamps and clock times. In general this method has proved highly effective:
channel timestamps allow the Ruth programmer to detect when events happen and to
specify when events should happen in a simple and elegant way. By treating a real-timeclock as an input stream Ruth allows access to the current time in a purely functionalmanner.

One restrictive feature of the channeVtimestamp model is the fact that a programmer
must always specify a timestamp even when he does not care when the message isdelivered, provided that it will be delivered eventually. In real-time systems there is often
a need to handle "don't care" outputs, for example the logging of errors in an engine
control system. The only timing restriction is that all errors should be logged"eventually" .
[Harrison 87] proposed that "don't care" output could be expressed by supplying acomplete clock as the second argument to ConsCh. Operationally the intention was thatthe clock should be instantiated at the moment the message is sent, thus avoiding
timeouts. This was abandoned because there seemed to be no way of providing asemantic definition for it within the semantic model being used. According to this modela program is supplied with clock tree as an input and nothing can be assumed about thevalues contained in that tree.

A better approach is simply to allow Ruth processes to produce lazy streams of(untimestamped) atoms as output as well as channels. No timestamps are specified since
the programmer does not care when the atoms in the streams arrive at their destinations.
142

This has the disadvantage that a receiving process could not use Time or, more
importantly, Ready on such an input stream. The view taken here is that if the time atwhich a particular atom is produced is of no importance to the producer of the atom thenit has no importance to the consumer. If this is not the case then a channel should be

used.

If a Ruth process fails to meet a time deadline this is treated as a fatal error. In otherwords, if an attempt is made either to construct a channel with a message timestamp thatis less than the current value of time, or to send an out of date channel message toanother process, then a timeout occurs and the <00,..L> element of ~ results.
An alternative approach would be to replace the erroneous message with a "timefault" message as is done in real-time Lucid. This has the obvious advantage that theprocess which produced the late message is not assumed to be fatally flawed and may go
on to produce further (hopefully) on-time messages. The only disadvantage is that wecannot predict from the semantics when a message will be replaced by a time fault. In achannel construction such replacement depends upon when the channel is constructed
and at a process boundary it depends upon when the attempt is made to output themessage. In the semantics both of these times are read from the semantic clock and wehave no information about the values in clocks. On the other hand the robustness of
Ruth programs would be markedly improved by the introduction of time faults since theprocess producing the time fault could be informed of this by the process receiving it,
and could thus take correcting action. For this reason time faults are a necessary addition
to Ruth.

A problem which which occurred when writing the Minesweep program was thatof finite channels. Normally a real-time program is never expected to terminate, but to go
on producing results "for ever" and consequently it was felt there was no need toconsider a means for signalling the end of a channel. Even if all real-time programs
never terminate, and the Minesweep program shows that this is not true, there is still a
use for a channel terminator, particularly if Ruth were to allow dynamic process creation(see below).
143

To allow the programmer to tenninate a channel Ruth should provide a primitive
such as End_Chan below
End Chan (n)<n, End>(7 .1)and the definitions of HeadCh, TailCh, Time and Ready would be augmented in theobvious way.

7.2.2 Defensive programming and dynamic process creation

As was seen in the Minesweep program it is simple to write passive output
supervisors in Ruth to support defensive programming. However passive output
supervisors have an important weakness : they can only react to incorrect message
timestamps to prevent timeouts, they cannot send messages to ensure deadlines are met.
The latter requires an active output supervisor.

In Ruth an active output supervisor would be written as a process which acts as awatchdog on a producing process's output channel(s). When a deadline is not met adefault message would be inserted. Once such a situation has occurred it is frequently
the case that some form of re-initialisation of the producing process is required. Since
there is no way to preempt a process in a functional language, and thus force it toreinitialise, the obvious technique would be to create a new version of the producing
process and rely on the underlying implementation to "garbage collect" the original.
Unfortunately dynamic process creation is not allowed in Ruth so this strategy cannot be
used. This is a serious weakness of Ruth.

The process structuring facilities in Ruth were influenced strongly by those ofoccam. This was largely for reasons of simplicity since our primary concern was thefeatures of the language supporting its time expressibility and not the process structure.
Consequently a Ruth program is a static configuration of processes, and processes are
distinct from functions.
In retrospect there seems no reason why a process should not be treated as a function
144

which produces tuples of channels as results. The language semantics already treats
processes in just this way. Instead of a Ruth program being a configuration of processes
it would be itself a process whose process expression was allowed to define and apply

other processes.

7.2.3 Clock skewing and communication delays

Throughout this work we have made two simplifying assumptions which are notjustified in the real world. Firstly, that the real-time clocks on different physicalprocessors will always be synchronised (Le. there will be no clock skewing); andsecondly, that channel communication is instantaneous. Before Ruth could be used onreal world problems these assumptions must be discharged.

Clock skewing between processors can be dealt with at the implementation level via
methods such as Lamport's algorithm [Lamport 78] mentioned in Chapter 3. Any
realistic implementation of Ruth on a distributed set of processors would have to use
such an algorithm.
Channel communication delays are slightly more complex to handle. Unpredictablecommunication delays are a fundamental problem in real-time programming to which
there seems no obvious solution. Once again it seems that the real-time programmer isforced onto the defensive. Programs must be written in such a way that messages willreach their destinations on time in all but the worst situations. When a message does failto meet its time deadlines a real-time program must be able to recover.
It should be noted that the use of the filter function in the definition of processapplication could be interpreted as modelling unpredictable communication delays.
filter uses the clock values to denote the time that messages become available at theirdestinations. Although we have assumed that this is the same as the time at which themessage leaves its source this assumption has no bearing on filter which reads thetime values it checks against directly from a semantic clock about whose values we haveno information. It could equally well be assumed that the times read from the clock145denote only the arrival time of the message, which is strictly greater than the sendingtime.

7.2.4 Conclusion

In this section we have looked at Ruth as a programming language and have found it

wanting in several respects. For Ruth to be regarded as useful in the real world theimprovements mentioned in this section, and possibly several others, would have to be
made. It should be noted however that we have found Ruth IS underlying notion ofreal-time systems as a set of real-time processes communicating via streams oftimes tamped messages to be a simple, powerful and elegant modeL This model forms
the basis of the language STRuth which is introduced in Section 7.5.

146

7.3 Outline Implementation

This section outlines a possible prototype implementation for Ruth. The intention is
to show that there is no conceptual difficulty in producing an implementation for Ruth;
no implication that this approach is the optimal one is intended.

7.3.1 Overview

A Ruth program is a configuration of several processes executing in parallel. We
propose that each process should be mapped onto one of a set of processing agents
which will execute it. Each agent thus has two tasks: to execute its Ruth process and tocommunicate the process's results to other agents and to the outside world. We shallassume that agents execute Ruth processes via lazy SECD machines ([Landin 64],
[Henderson 80], [Henderson et. al. 83]). Channels are implemented as head-strict
streams of <timestamp, atom> pairs and the Ruth SECD machine is extended to allow
for multiple I/O channels along the lines of [Jones 84a, 84b].
The system will be implemented in occam and will run on one transputer [INMOS87]. Thus each agent (and therefore each Ruth process) is implemented as one occam
process. The implementation is restricted to one transputer to avoid the problem of clock
skewing and message transmission delays.

Agents will communicate via occam channels; each occam channel will carry one
Ruth channel. We shall refer to these occam channels as pipes. occam channels may beeither soft channels linking different occam processes on the same chip via on-chip
memory locations, or hard channels linking occam processes with the external
environment via the transputer's communication links. Channels between Ruth
processes will be implemented as soft occam channels; channels between Ruth
processes and the external environment will be implemented as hard occam channels.
A Ruth channel has exactly one source process, though it may be consumed by any
number of destination processes. However, since channels are implemented as occam
147channels, and since an occam channel has exactly one source and one target process, thisprototype implementation imposes the added restriction that each Ruth channel may only
be consumed by one destination process.

An agent executes a Ruth process via a series of transitions, each of which has twophases : an execution phase and a communication phase. In the execution phase theagent will perform an SECD machine transition and in the communication phase it will
send and receive messages to and from other agents and the external environment.
Agents perform this cycle asynchronously; two agents cannot transfer messages between
themselves unless both agent is in its communication phase.

The state of an agent can be represented as a tuple of the form
A :

[M,

I,

0,

T]

(7 .2)

Here A is the agent number (1 ~ A ~ Number of agents). M is the SECD machine
executing the Ruth process. I is a list of lists, one list for each input pipe; each list
contains messages that have been received by the agent but not yet read by the Ruth
process. 0 contains an entry for each output pipe; at the end of an execution phase eachentry contains the timestamped message (if any) produced by the last execution phase for
output on that output pipe. Messages are sent to their destinations in the communication
phase immediately following the execution phase that produces them, and are thenremoved from o. Consequently, at the end of a communication phase there will be no
messages stored in o. The receiving agent has the responsibility for storing messages
until they can be dealt with. Finally, T is the agent's integer value for the current time; T
is incremented at the end of each communication phase from the processor's hardware
clock by amounts which depend on that clock (and thus on the speed of theimplementation).

The working of the execution phase is essentially identical to that given in [Jones84a]. Three points should be noted:(i)

As in any functional language implementation the cell space must be allocated148dynamically and periodically garbage collected. It would be possible to use
traditional mark-sweep garbage collection on an agent's cell space but thiswould produce unpredictable (and fairly large) delays on agent operations
which is highly undesirable in a real-time system. Instead an incremental,
copying method such as that of [Baker 78] or the more efficient [Liebermannand Hewitt 83] will be used.
(li) Instead of performing I/O directly with the external environment an SEeD

machine executing a Ruth process will perform I/O via it's agent's I and 0
registers. Instead of reading input directly from I/O devices the SEeD machinereads messages from the I register. Thus, the SEeD machine instruction INPUT
is modified to read its result from the relevant I register entry, instead of
directly from the external world. Similarly, instead of sending output directly to
I/O devices the SEeD machine instruction OUTPUT sends messages to therelevant 0 register.
The INPUT instruction is a blocking input: if there are no messages in therelevant I register when the SEeD machine executes an input instruction thenthe execution phase terminates and the communication phase is entered. Whenthe communication phase ends the INPUT instruction is re-tried.This cycle
continues until a message is put in the relevant I register. The OUTPUT
instruction always succeeds in placing its argument in the relevant 0 register.
(iii) Program clocks are implemented as head-strict streams of integers; the values inthe stream are instantiated with the value of T whenever the SEeD machine M
executes a HEADCLK instruction.

Apart from a brief discussion in Section 7.3.3 on the implementation of the Ready test
the execution phase will not concern us further here. For further details the reader isreferred to [Jones 84a, 84b].

149

7.3.2 The communication phase

The input and output registers are of the form
(pk,mk ) )I(7 .3)(pj,lj»Each (pi, mi) pair in the list 0 denotes that the timestamped message mi is to be sentalong the pipe pi in the next communication phase. If there is no message to betransmitted for an output pipe pi then mi is Nil. Each (Pi' Ii) pair in the list I denotesthat the list of timestamped messages Ii have been received along the pipe Pi and have
not yet been read by the agent's SEeD machine, M. If there are no messages received
from Pi which have not been read by M then Ii is Nil.
Note that it is the responsibility of the receiving agent to buffer messages if a sending
agent is producing messages faster than a receiving agent wishes to read them. Thus I
must store a list of messages for each input pipe. 0 need only store a single message per
output pipe since each execution phase cannot produce more than one message perchannel (see [Jones 84a] for details), and these messages are immediately forwarded totheir destinations.
A further responsibility of a receiving agent is to check that the timestamps onincoming messages are not out of date. Each of the messages sent to an agent A ischecked against the current time T when it is received. If a message has a timestamp lessthan than the value of T then it is out of date and a timeout error has occurred. Instead of
appending the message to the relevant Ii an error value is appended indicating that atimeout has occurred. All further messages in this pipe will be ignored by agent A.
When giving the semantics of Ruth the check on message timestamps is performedby an application of the f i I te r function in the sending process. In this prototype
implementation the check is actually performed in the receiving process. This allows foreasier handling of communication delays in future multi-processor implementations andis no more complex than performing the check in the sending process.

To give a flavour of how channel communication proceeds in the communication
150

phase consider two agents Al and A 2 " At the start of a communication phase Al wishes tosend the message d with timestamp t along the pipe p to A2 • For simplicity, assume that
Al is executing a Ruth process with only one output channel, and thus that p is the only

pipe in AI'S output register. Similarly, assume that the Ruth process being executed byagent A2 has only one input channel, and thus, that p is the only pipe in A2 's input
register. We shall also assume that Al receives no input messages during thiscommunication phase and that A2 sends no output messages.
At the start of the communication phase the states of Al and A2 are( (p,(t,d))),T1 ](7 • 4)( (p,l) ),Here 1 is the list of messages which A2 has received on pipe p which have not yet beenread by the Ruth process being executed by M2 . If T2 is no later than t then the message(t, d)

is appended to 1 since it has arrived at A2 in time. Otherwise 1 records that (t, d)

is an out of date message by appending error to the message list for p in A2 " Anyfurther messages received on p will be ignored so that the Ruth process being executedby A2 will receive no more messages from A2 after the timeout.
Thus, at the end of the communication phase, the agent's states are(7 .5)(p,append(l,(t,d)))),° 2 ,

T 2 +0 2 ]iff T2 $ t(p,append(l,error))),° 2 ,

T2

2]otherwise

+°

where
appendlambda (l,m).
If 1 = error
Then error
Else If IsNil(l)Then Cons(m, Nil)
Else Cons (Head(l) , append(Tail(l), m))

Tl and T2 are incremented by 01 and 02 respectively, thus modelling the passage of time

as execution proceeds. 01 and 02 will probably not be the same since the time Al takes to151

send the message and remove it from 0 will probably be different to the time taken by A2
to receive the message and store it in I.

This simple case generalises in a fairly straight forward way to cases involving
several messages and agents.

As mentioned above both Al and A2 must be in a communication phase for a message
to transferred between them. An attempt to send a message from an 0 register blocks anagent: Al cannot proceed with its next execution phase until A2 has received the (t, d)message. Thus Al must wait for A2 to enter its communication phase. An attempt to input
a message to an I register does not block and agent: Al can simply scan for inputs and if
none are available it proceeds. The INPUT SEeD machine instruction ensures that an
attempt by a Ruth process to read a message from a channel will always be blocked until
a message has arrived. An agent must, however, be able to scan for input messages in a
non-blocking manner so that the Ready test can be successfully implemented (seeSection 7.3.3 below). In the worst case a source agent may enter its communication
phase and try to send a message just after the destination agent has completed its scan.
The source agent will be delayed through the rest of the destination agent's
communication phase and the following execution phase before it can send the message
and proceed.
An agent must scan its inputs and send its outputs in parallel to avoid deadlock. For
example, if agent Al attempts to send a message to agent A2 and A2 attempts to send amessage to A 1 • Both agents are attempting to send messages and thus, unless they arescanning for inputs in parallel with this, deadlock will occur.

7.3.3 Implementing the Ready test

As mentioned above, an SEeD machine executing a Ruth process performs all its
I/O with its agents I and 0 registers. To implement the Ruth Ready test requires the
addition of an extra instruction, READY, to the SEeD machine given in [Jones 84a, 84b].
The READY instruction tests whether a channel contains a message by the current time152

which is held in the T register. The test is petfonned on the entry in the agent's I registercorresponding to the channel being tested. Assume that this entry is (p,l) and that thecurrent value of the agent's time register is T. Let the result of the READY instruction be
denoted by r.
r=

If ISNil(l) Or (1error)(7 . 6)

Then false
Else If timestamp > T
Then false
Else true
wheretimestamp

Head (Head (1) );If an out of date message has been received on p then any subsequent Ready test isfalse. If 1 is Nil the Ready test is also false since any further messages on p musthave timestamps greater than T or they will cause a timeout error. This allows the abilityof the Ready test to timeout messages to be implemented. Finally, if there is a message
in 1 then the result of Ready can be determined from its timestamp.

7.3.4 Conclusion

In this section we have outlined a possible implementation for Ruth. The purpose

was to show that such an implementation presents no major difficulties and the two-levelapproach chosen was dictated by simplicity and ease of explanation. A moresophisticated implementation using some of the techniques detailed in [Peyton Jones 87]
would almost certainly prove more efficient. An efficient implementation of Ruth is not,however, the purpose of this work.

153

7.4 Theoretical Issues

One of the major reasons for giving a formal semantics for a programming language
is to facilitate formal reasoning and correctness preserving transformation. In this section
we examine just what kind of reasoning and transformation is possible in a real-time
context.

7.4.1 Reasoning with real-time programs

Consider the following Ruth function defmition.
flambda (n). ConsCh ('Any', n + 10, f(n + 10))(7 .7)In the absence of timeouts the expression f ( 0) would produce the channel<10,['Any', <20,['Any', < ... >]>]>(7 .8)

but if a timeout occurs at any point the remainder of the channel will be <00, ~>. Whether
or not a timeout occurs depends on the values held in the semantic clock about which wehave no information. A similar effect is caused by the filter function at process
boundaries.
Since the message timestamps in a channel denote exactly when the messages will
arrive at their destinations we have the situation that in the absence of timeouts it ispossible to prove not just what data values are produced by a Ruth program but also

when those values will be produced. If a timeout does occur then no further messages
will be produced.
It might appear that we are able to prove a form of partial correctness : the rightmessages will be produced at the right time or no messages will be produced at all.
However this is not the whole story. In a real-time system a failure to produce results
conveys (almost) as much information as the results themselves and it is to detect suchsituations that Ruth has the Ready test.
Consider two possible evaluations of f (0) : (i) in which the fIrst message is timed154

out and (ii) in which the fIrst message is not timed out.
(i)Ready (f(0),15)

true

(li)

Ready (f(0),15)

false

if no timeout occurs
if timeout occurs(7 • 9)Since the occurrence of a timeout depends upon the values in the semantic clock there is
no way in which the result of a Ready test can be predicted from the text of a Ruth
program.
Were the Ready test to be removed from Ruth we would at least have the ability toprove partial correctness: that if any answers are produced they will be the "correct"
ones. It would, however, be impractical to omit the Ready test from Ruth for reasonsmentioned above.
If it were possible to predict when timeouts would occur we would have a totalsolution to the problem: the results of a Ruth program could be predicted from the textof the program. The major advantage of clock-driven timing is also its major
disadvantage: all the information about time is abstracted in to the semantic clocks
leaving us no way of reasoning about the occurrence of timeouts.

7.4.2 Correctness preserving transformation with real-time programs

The basis for formal transformation of program is the notion of referential
transparency : equivalent expressions can be interchanged at will. Consider thefollowing two expressions(i)4(7.10)(li) 2 + 2

Suppose the result of (i) is <t 1 , 4> for some time t 1, and the result of (ii) is <t 2 , 4> forsome time t 2 . It can be seen from the semantics that t1 and t2 will be different: t1 willbe the first time value in the semantic clock used to evaluate the expression whereas t2
will be read from the ath sub-clock of that clock and must therefore be bigger than t 1.
Under a non real-time semantics (i) and (ii) would be considered equivalent since the155data value part of their result is all that is considered: the classical notion of referential
transparency abstracts from the real-time aspect. Paraphrasing [Stoy 77] we can better
express classical referential transparency as follows.

The only thing that matters about an expression are its data value and its semantic

timestamp value, and any expression can be replaced by any other with equal data
value.

The addition of the consideration of time to the definition of classical referential
transparency has made explicit what was previously implicit : that for mostcomputational purposes two expressions are equivalent if they compute the same data
value, regardless of when they compute it. We shall refer to this interpretation ofclassical referential transparency as data referential transparency (DRT).
A more "hard-line" interpretation of referential transparency is what we shall callreal-time referential transparency (RRT) which is defined as follows.

The only thing that matters about an expression are its data value and its semantic

timestamp value, and any can expression can be replaced by any other with equal
data value and semantic timestamp value.

Under RRT only totally identical expressions whose evaluations are carried out at thesame time can be considered to be equivalent. Consequently RRT is not a useful basis
for program transformation since one of the major reasons for transforming programs is
to make them execute faster: to change the values of the semantic timestamps. DRT, on
the other hand, is the basis for many transformation systems on non-real time languages;
for a survey see [Partsch & Steinbruggen 83].

Some transformation systems (e.g. [Sherlis 80]) guarantee the preservation of total
correctness: if evaluation of expression E terminates with the result v then evaluation of
the transformed version of E, E T, will also terminate with the result v. Other systems(e.g. [Darlington 82]) guarantee to preserve only partial correctness: if evaluation of156

expression E tenninates with the result v then if evaluation of the transformed version ofT

E, E , also tenninates it will do so with the result v.

In a real-time semantics total correctness preservation is expressed as data total
correctness (DTC) preservation, and partial correctness preservation is expressed asdata partial correctness (DPC) preservation.
Definition: Data total correctness preservation.

(7.11)Let E be a Ruth Expression and let ET be E transformed by sometransfonnation T.
If ~ [ E ] P c = <t,v> and ~ [ ET ] P c = <tT,vT>

Then the transfonnation T preserves DTC iff v = v T
Definition: Data partial correctness preservation.
Let E be a Ruth Expression and let ET be E transformed by sometransfonnation T.
If ~ [ E ] P c = <t,v> and ~ [ ET ] P c = <tT,v T>

Then the transformation T preserves DPC iff v !;;;; v T or v T !;;;; vThe question is, can DTC or DPC preservation be used as a basis for programtransfonnation in real-time systems? Let ch be an output channel from a Ruth process p
and let chT the corresponding output channel from the transformed process pT. If thetransfonnation from p to p T preserves DPC then either ch is a prefix of ch T, or ch T is aprefix of ch. If the transfonnation from p to pT preserves DTC then ch is identical to
ChT.

The problem with DPC preservation is the same problem as was encountered in thelast section on fonnal reasoning: Ready's ability to detect the timing out of a message
due to a non-tenninating, or simply too slow, computation. By transforming a process
or a channel construction it is possible to introduce, or to remove, time outs and thus
potentially change the data value part of the result of a Ready test.
Once again, if the Ready test is removed from Ruth then DPC preservmg
transfonnation becomes possible. Indeed, a transformation technique which preservesclassical partial correctness would also preserve DPC when used with Ruth programs.
However removing the Ready test would remove most of Ruth's power as a real-time157

language. Furthennore DPC preservation is not acceptable in real-time systems because
it allows for timeouts to be introduced by transfonnations. In non real-time situations atardy computation can be aborted and another attempt made. Real-time systems do notallow second attempts.

The same problem exists for DTC as for DPC : the introduction and/or removal of
timeouts must be avoided. The situation is more serious than for DPC. Even if the
Ready test were removed from Ruth DTC preserving transfonnation is difficult since atransfonnation which preserves classical total correctness may not preserve DTC.
Although the transfonned expression will terminate provided the original terminated it
may take a different amount of time to do so. Thus timeouts may be introduced or
removed and thus DTC will not be preserved.

Simply being able to predict the occurrence of timeouts would solve these problems
since transfonnations which introduced or removed timeouts could be identified and thus
DTC preservation could be guaranteed. Because channel message timestamps are part ofthe data that would be preserved, we would thus gain the ability to transfonn programs
and still preserve their real-time behaviour.

7.4.3 Conclusions

The biggest problem with fonnal reasoning and transfonnation of Ruth programs isthe combination of clock-driven semantics and channel message timeouts. Clock-driven
semantics allows abstraction away from low-level detail but this abstraction makes it
impossible to reason about the values of semantic timestamps save in the most generaltenns. In particular, it is impossible to predict when timeouts will occur at channel
construction or process boundaries.

Ruth's time expressibility is based upon user-defined timestamps to identify when
events will, or did, occur, and upon a detenninate Ready test for detecting the158

occurrence or non-occurrence of an event. Thus, in the absence of timeouts, thereal-time behaviour of a Ruth program is totally defined by, and can therefore be proved
from, the program's text. Also, DTC preserving transformation is sufficient to preserve
the real-time behaviour of a Ruth program.

Most other real-time languages use implicit don't care/don't know timestamping to
identify when events should/did occur, and implicit time determinate operators to detect
the non-occurrence of events. By don't care timestamping we mean that an event will
occur as soon as possible, and by don't know times tamping we mean that the systemdoes not know when an event occurred save that it occurred before the current time. The
real-time behaviour of a program written in such a language is totally defined by the
speed at which it is executed. The way this would be modelled semantically depends
upon whether a clock- or delay-driven semantics is used. Using a clock-driven
semantics timestamps would depend on the (unknown) values in the semantic clock.
U sing a delay-driven semantics timestamps would depend upon the 8 values specified
for the operations required to compute data values.
If a delay-driven semantics is specified then it is possible to prove the real-time
behaviour of a language using don't care/don't know timestamping, though performing
such a proof ,is probably impractical for all but the most trivial programs. If aclock-driven semantics is given proof of real-time behaviour is impossible. This isslightly worse than with Ruth for which, even using a clock-driven semantics, it ispossible to prove a program's real-time behaviour assuming the absence of timeouts.
For either a delay-driven or clock-driven semantics DTC preserving transformation
will not, in general, preserve the real-time behaviour of a language using don'tcare/don't know timestamping. In this context DTC preserving transformation will only
guarantee to preserve the data values computed, not the times at which they arecomputed. This is much worse than with Ruth for which DTC preserving
transformation will preserve real-time behaviour.

Thus, Ruth offers certain advantages for formal reasoning and transformation over a
traditional real-time language with time expressibility based on don't care/don't know
159

timestamping. To a large extent, however, these advantages require that timeouts be
detectable from the text of a Ruth program. In the absence of timeouts the real-time
behaviour of a Ruth program is totally determined by its text, and this behaviour will not
be changed by a DTC preserving transformation since such a transformation will neither
introduce, nor remove, timeouts. The remaining problem is then to detect timeouts
within Ruth programs. If a Ruth program can be proved timeout free then its real-time
behaviour is guaranteed. If both the source and result expressions of a classical total
correctness preserving transformation can be proved timeout free then the transformation
has preserved DTC.

A possible approach to this problem is simply to assume that timeouts do not occur.
The real-time behaviour specified by programs can be proven modulo this assumption.
Classical total correctness preserving transformations can be applied to programs since,in the absence of timeouts, they will preserve DTC, and thus real-time behaviour. The
transformations used will be go-Jaster transformations : transformations which produce
an expression which computes the same result as the original expression but with alower semantic timestamp value (i.e. the transformed expression produces a result
faster). By applying go-faster transformation the hope is that the potential for theoccurrence of timeouts will be removed.
Of course, this is a totally heuristic method since, under a clock-driven semantics,
there is no way in which go-faster transformations can be identified. Equally, there is nocertainty that the program which results from transformation is timeout free anyway.

The situation can be improved by giving a delay-driven semantics for Ruth. To
avoid problems caused by the possible variability in duration of language operations the
O-values chosen will be the maximum that the relevant operation can take. Consequently,
this approach is called defensive delay-driven timing. Any putative implementation of
Ruth which did not guarantee to exactly conform to these 8-values would not be a valid

implementation of the language.
The advantage of a defensive delay-driven semantics is that timeouts can always be
predicted and thus DTC preserving, go-faster transformations identified. A disadvantage
160

of a defensive delay-driven timing semantics is the difficulty of choosing the correct
a-values. If these values are too small the language may be difficult to implement; toolarge and the language may be too slow to be useful. A further disadvantage is that adefensive delay-driven semantics must specify evaluation strategy in some detail. For
example, if a lazy evaluation mechanism is used then the exact way in which recipes are
updated with their values must be specified in the high level semantics. Also, to prevent
a-values becoming too large an incremental garbage collection mechanism must be used
and multi-programming cannot be allowed.

The next section outlines a compromise in which as few as possible of the constructsof a language need be given a defensive delay-driven semantics in order to guarantee
real-time behaviour. By restricting the set of constructs chosen to those for which a
fixed, and small, a-value can be guaranteed it is hoped that the problems mentioned
above will be minimised.

161

7.5 A Language Based On Explicit Timeouts
7.5.1 Introduction

As was seen in the Minesweep program, real-time software often has the following
structure:loop(7 .12)

Get inputs ;Compute outputs ;Send outputs ;endloopthat is, an infinite sequence of I/O interactions and computation steps. The Minesweep
program contained output supervisors to provide the following, defensive, behaviour :start algorithm ;(7 . 13)

if algorithm produces result within tl of starting
then okelse interrupt algorithm and return default value

If t 1 time units have passed and the algorithm has not yet produced a result then it ispre-emptively interrupted and a default constant is returned instead.

The underlying concept here is that the programmer expects that each interaction step
will take a fixed, and known, amount of time, whereas each computation step may takean indefinite amount of time, depending upon the parameters of the computation and thecurrent state of the machine. Consequently, to ensure that time deadlines are met a meansof preempting a computation step and taking recovery action is required.

In this section we introduce a programming language which allows real-time
programs to be written in the style outlined above. The language is called STRuth,
which stands for "Sequential, Timeout Ruth" since it provides explicitly sequential
constructs and a facility for preemptive timeouts, and is an attempt to put into practice the162lessons learned from Ruth.

7.5.2 The language STRuth

In the same way as real-time programs can be divided into interactions andcomputations STRuth is divided into a behavioural and a computational language. As
noted above even a functional program tends to interact with its environment in asequential manner and it therefore seems sensible to provide sequential primitives toallow this. The notation we shall use here, whilst appearing very similar to traditional
imperative language notation, is in fact no more than a syntactic transformation of purely
functional combinators such as those used in [Thompson 86] and [Jones & Sinclair 89].
The most important feature of the behavioural language is that each of its constructs
takes a fixed amount of time to execute.Thus a defensive delay-driven timing semantics
can be given for the behavioural language and formal reasoning and transformation ispossible with it.

All interaction with the environment, and the times at which it occurs, is expressed in
the behavioural language. Thus the computational language need have no notion of time
expressibility; in particular, the Ready test and channel primitives are not required. A
traditional functional language, such as Haskell [Hudak et. al. 89], is thus perfectly
adequate for the task. Operations in the computational language are not expected to take afixed amount of time to execute; instead the behavioural language provides facilities fortardy computations to be timed out. Since fixed 8-values need not be specified, aclock-driven timing semantics is appropriate for the computational language.

The simple, and somewhat contrived, program overleaf repeatedly reads an integer
from the input channel inl, a boolean from the input channel in2, and the current timefrom the pre-defined input channel time. If the input boolean is true then the integer
and the time are output on output channel outl, otherwise they are output on output
channelout2.
163

chan input in1, in2 ; output out1, out2 ;(7.14)

var x,y : integer; b : bool ;behaviourl.oop true do

in1 ? x ; in2 ? btime ? Y ;if b then

out1

I

y

;

out1

x

y

;

out2

x

el.se

out2
endif

endl.oop
endprog

The example contains all of the behavioural constructs allowed in STRuth apartfrom assignment: identifier reference, loop, if-then-else, input and output. Since a fixed
duration is guaranteed for identifier reference, input, output and assignment, a fixed
duration can be guaranteed for any loop or if-then-else, and thus for any complete
STRuth program.

A STRuth assignment is of the formv:=

"computational language expression"(7.15)

Obviously, once the computational language expression has produced a value it takes afixed, and specifiable, time to bind that value to v. However, there is no way ofdetermining how long a computational language expression may take to evaluate.To
ensure that deadlines are not missed the programmer is allowed to specify the completiontime for any assignment. If the assignment is not completed by that time then an interrupt
occurs and recovery action can be taken.
(7 . 16)x .- E timeout 800 ;An attempt is made to evaluate the computational language expression E. If thisevaluation is not completed and its result successfully bound to x within 800 time units164

of the start of the assignment then an interrupt occurs and execution of the assignment
terminates with the value bound to x unchanged (i.e. the same as before the assignment
started).
If timeout

800 were omitted then as much time as required would be taken for E,

and the result would be bound to x with no possibility of timeout. In this case there is no
way of determining when the assignment takes place.

A similar approach can be taken to the problem of guaranteeing that input/output
interactions terminate within a fIxed time.
in ? x timeout 800 ;(7.17)

If a message is not available on channel in within 800 time units of the start of executionof the input then an interrupt occurs and execution of the input terminates with the value
bound to x unchanged.

7.5.3. Formal semantics

The meaning of a STRuth program is defined via the evaluation function tp which
has the following signature.
PROG ~ ENV ~ NOM ~ @~~ ~ ENV(7.18)

Here PROG is the syntactic domain of STRuth programs. A STRuth program is amapping from an initial environment, the current time represented as a positive integer
and a clock, to a final environment. The clock argument is not used by tp but is passed
to the meaning function tv which defines the semantics of a computational language
expression.
(7.19)Exp is the syntactic domain of computational language expressions. A computational165

language expression is a mapping from an environment and a clock to an expressible
value.

The semantics of a simple assignment are as follows

t; [ x := El ; P ] p t c=(7.20)~ <tl,V l > : ~ [ El ] p clockafter(co,t)

~

e

p [

p

]

(P &

[x

~ <tl,V l >])(t l + 0assign)

Cl»>
P, the remainder of the program, is executed with an environment in which x is bound tothe value obtained by evaluating the computational expression E l . Evaluation of El does
not begin until after t; there is no guarantee of when evaluation of El terminates. 0assign
is the time taken after El has been evaluated to bind its result to x; execution of p does
not begin until tl + Oassign'

To give the semantics of an assignment which may be timed out requires the use of~§'lS@ll:21 ••. ~A'lSl:21 •••notation rather than the more secure ~ ...

IDsince timeout

behaviour must be specified (c.f. the definition of Ready in Chapter 5).

t; [ x := El t~out 800 ; p ] p t c(7.21)(~'lS@ll:21 <t l , VI> ~A'lSl:21<tl,..l> ~

((t l
~

+ 0assign)~(t+ 800)<tl'..l>,t; [ p ] P (t + 800) cl<tl'Vl> ~((t l + 0assign) ~ (t + 800)~t; [ p ] (P & [x ~ <tl'v l >])t; [ P ] P (t + 800) cl(t + 800)

cl '

where

<tl,v l > = ~ [ El ] p clockafter(co,t)Note that here we have been a little simplistic in that we have assumed that the timeout
time is the fixed constant, 800, rather than a value computed during execution of the166

program. The general principle holds good however: if the value of E I can be computedin time for its result to be bound to x by absolute time t + 800 then this is done.
Otherwise an interrupt will occur and the binding for x will be left unchanged. In eithercase execution of P, the rest of the program, will not begin until t + 800. STRuth
takes a defensive view: since there is no way to predict when evaluation of EI will
tenninate, all that can be guaranteed is that the assignment will terminate by the interrupt
time, t + 800. Even if evaluation of EI terminates quickly enough for the assignment tobe completed before t + 800 the program must still wait until t + 800 before starting
P. This may seem excessively severe but is the only way to guarantee the real-time

behaviour of a timed out assignment.

The semantics for an input are similar.

t; [ in ? x timeout 800 ; p ] p t C(~'G@~ <t l<t' ,1..> ~+ BId'(7.22)

vI> ~~'G~«t' + Bassign) ~ (t + 800)~

<t' ,1..>,t; [ p ] p (t + 800) cI< t', [a, rest] >~«t' + Bassign) ~ (t + 800)~t;[p] (p& [x~<t',a>]) (t+800) clf
t; [ p ] P (t + 800) cI

where
lookup(in,p)There is no identification timestamp associated with the channel bound to the identifier
in. Identification timestamps were required for Ruth channels because a channel could

be the result of an arbitrarily lengthy computation. In STRuth the only way to referencea channel is via an identifier reference as above. Identifier reference has a fixed overhead(BId above) so no identification timestamp is required.

167

7.5.4 Conclusion

The principles behind STRuth are that to give a delay-driven semantics for acomplete real-time programming language is difficult, and that such a semantics isprobably impractical to work with at present. Instead, a clock-driven semantics is used
for most of STRuth and the use of defensive delay-driven semantics is restricted to asmall subset. Programs written in STRuth guarantee either to interact with theirenvironments at the correct times, or with the correct data values. In the absence of acomplete delay-driven semantics it is impossible for a language to guarantee both.
STRuth accepts that fact and provides programmers with the ability to decide whichaspect of correctness is the more important. If correct data values are more important,then a combination of inputs, simple assignments and outputs suffices. If deadlines must
be met, then STRuth provides an explicit timeout construct to prevent computations
from overrunning. An alternative may be substituted for the timed out computation andthe deadline still met.

The work presented here is of a very preliminary nature. Nonetheless, it seems likelythat this approach will prove valuable in the production of reliable real-time software,and represents the most promising route for further research. For further information
about STRuth the reader is referred to [Harrison & Nelson 89].

168

7.6 Conclusion

This thesis has explored the application of functional programming techniques toreal-time programming via the design of the real-time functional programming language
Ruth. Many existing real-time languages have poor facilities for time expressibility andprogrammers often rely upon their intuitive knowledge of how a von Neumann
processor works to ensure that things happen at the right times. Moreover, implicit time
determinate operators are usually used to allow for non-blocking tests for input. Neitherof these approaches is possible within a functional language and we were forced to
evolve new methods. Time expressibility was provided via timestamps and real-timeclock streams, and non-blocking test for input via the Ready test which is a determinate
test on user-defined message timestamps.

The major part of this work is the semantic definition of Ruth using herring-bone
domains and clock-driven timing. An exploration of a framework within which thereal-time characteristics of computer programming languages could be expressed was
not the original intention but, in retrospect, has probably proven the most interesting
result of this work, and probably the most useful.

Ruth is by no means a perfect real-time programming language and, as we haveseen, certain difficulties exist in formal reasoning and transformation of Ruth programs.
These difficulties are a direct consequence of working within the real-time domain: since
when values are computed is a part of the result of a real-time program is comes as no
surprise that this information must be supplied by giving a defensive delay-driven
semantics to the language. Unfortunately giving a defensive delay-driven semantics for alanguage is a difficult task. The explicit message timestamps used in Ruth programs
limit these problems but do not totally solve them. STRuth extends the explicit
specification of timing requirements in programs to a limited set of language operations.
It is hoped that a compromise can be reached in which the real-time behaviour ofprograms can be guaranteed without the need to specify a defensive delay-drive
semantics for all language constructs.
169

Appendix 1 : Formal Presentation Of The Semantic
Domains

AI.I The Foundations

In this section we define the primitive domains and orderings, domain constructors

the orderings they impose, and constructors and selectors for the constructed domains.
Firstly the primitive domains

Definition: Primitive Domains(AI. 1)

INT

Integers: {..i, ... , -2, -1, 0, 1, 2, ... }NUMIntegers ~ 0 : {..i,BOOL

Booleans : {..i, true, false}

STRING

Symbolic strings: {..i, a, ab, abc, ... }NIL

End of list marker: {..i,

UNDEF

Identifier not defmed indicator: {..i, Undef}

NUM

Set of integers ~ 0 : {O, 1, 2, ... }0, 1, 2,

... }

Nil}

All primitive domains except NUM have the following orderingx !; y <=> (x =..i) v (x = y)and thus are pointed flat cpos. NUM is a set with no..i element and thus has the orderingx!;y<=>x=y

Before proceeding we shall define the syntax of the boolean choice primitive to be used.

Definition:

Choice Primitive(AI. 2)For any domain D

~

,

)

(BOOL x D x D)

~Dsuch that(..i~dl , d2)

..i

(true

~

dl , d2)dl(false~dl , d2)

d2

The definitions of the domain constructors to be used, he orderings the constructors

impose on the constructed domains, and constructors and selectors for elements of theconstructed domains are given below.

Definition:

Lifted Domain(AI. 3)For any domain A

Elements:

A..i

Ordering:

x b..i Y ¢:::}{lift(a)

I a

E

.i)

v

(x

A}

U

{.1}

(x

Constructor :

.1
lift

~

A..i

By pattern matching on lift (a) elements

Selector:

Definition:

A(Al . 4)

Sum Domain
For any two domains A and B{inA(a)Elements:

A

Ordering:

x bA+B Y ¢:::}

+ B

I a

E

A} U

{inB(b)

I b

E

B} U

{.1}

(x = .i) v(x=inA(a x ) A y=inA(a y ) A ax bA a y ) v(x=inB(b x ) A y=inB(b y ) A b x bB by)Constructors:

Selectors:
such that

~

.1

A+B

inA

A ~ A+B

inB

B ~ A+B(Cases x of isA(a) ~ elf isB(b) ~ e2)(Cases inA(a) of isA(x) ~ elf isB(y) ~ e2)= (ldx) .el)(a)(Cases inB(b) of isA(x) ~ elf isB(y) ~ e2)=(I..(y) .e2)(b)(Cases .1 of isA (x) ~ elf isB (y) ~ e2)

= .1

171

and also(Cases x of isA(a)such that(Cases inA (a)

=

~ elf

~ e

of isA(x)(Jdx) .e l )else ~ e 2 )l,else ~ e )2,else ~ e )2(a)(Cases inB(b)~ eof isA(x)l= e2(Cases .i of isA (x)=Definition :

~ elf

~ e

isB (y)2).iProduct Domain(AI. 5)For any two domains A and B

Elements:

A x B

Ordering:[ a , b ] !; AxB [a', b ']Constructor: [ , ]Selectors:

Definition:{ [a, b]

I a

A, b

E

B}

E

<=> [ a !; A a']A[b!; B b']AxB~AxB

By pattern matching on [a, b] elements

Coalesced Sum Domain(AI. 6)

For any two domains A and B

Elements:

A Ef> B{inA(a)a{inB(b)b E B, b :f. .i} u

A,

E

a

:f.

.i} u

{.i }

Ordering:

Constructors :x !;AEeB y.i<=> (x = .i) v(x=inA (ax)A

y=inA (a y )A

ax !;A a y ) v(x=inB (b x )A

y=inB (by)A

b x !;B by)~

A Ef> B

inA

A~

A Ef> B

where inA (.iA)

.i

inB

: B

~

A Ef> B

where inB (.iB )

.i

172

Selectors:
such that~(Cases x of isA(a)(Cases inA(a) of isA(x)(A(X) .el)=(A(y) .e2)

such thatel' isB(y)

~

e2)

~

el' isB(y)

~

e2)

(b)
~

e l , isB(y)~(Cases x of isA(a)~e l , else ~ e 2 )

e2)

~

=

and also~

of isA(x)(Cases

~

e2 )

(a)

(Cases inB(b) of isA(x)=~e l , isB (b)(Cases inA (a) of isA(x)(A(x) .el)=~el' else ~ e 2 )~el' else ~ e 2 )(a)(Cases inB(b) of isA(x)e2=(Cases~~of isA (x)elf else ~ e 2 )= ~Definition:

Coalesced Product Domain(AI. 7)

For any two domains A and B

Elements:

A

Ordering:

x !;A®B Y ¢::>{[a,b]® B

I a E A, a :t ~, b E B, b :t ~}(x = ~) v(x=[a,b] A

y=[a',b'] A

a !;A a'b!;B b')Constructor :

A

~A®B

,

[

A x

B ~ A

® B

where

[~A,b]

where [a, ~B]

Selectors:
Definition:~

By pattern matching on [a,b] elements
Function Space(AI. 8)For any two domains A and B

Elements:

A~B

Ordering:fConstructor:

Ax.e E

Selector:

U

{f

I a

¢::>

VaEA, f (a) !;B g (a)!;A~B g

(

)

E

A,

f(a)

A ~ B

(A

~

B)

x A

173

~

B

E

B,

f

continuous}{~}

A1.2 Herring-Bone Domains

This section concerns the construction of herring-bone domains. Firstly, theisomorphism between §@@~, the herring-bone domain of booleans and ~§@@~, thedomain constructed using domain lifting is proven. The rule for constructing aherring-bone domain from any arbitrary domain is then given.

The herring-bone domain of booleans is defined as follows :-Definition:

Herring-bone domain of booleans
For the domain of booleans, BOOL, the corresponding
herring-bone domain is §@@~.

Elements:
Ordering:{<t,b>'If tl't2

I t

E

NUM, b E BOOL} U{<~,~>}

NUM, bl' b 2 E BOOL

E

<t 1 , b 1 >~<t 2 , b 1 > ¢=>(t 1

Constructors :
<,

>

<~,

~>

NUM x BOOL

~ §@@~~§@@~

Selectors:(~'\S@~ <t, v> ~~'\S~ <t', ~> ~ e 1 ,<t', b ,> ~ e 2 )such that(~'\S@~ <t, ~> ~~'\S~ <t', ~> ~ elf=(A(t') .el)(t)(~'\S@~ <t, b> ~~'\S~ <t', ~> ~ e 1 ,=<t', b' > ~ e2)(A(t',b') .e2)(t,b)<t', b' > ~ e2)

where b :1= ~174(Al. 9)Proposition:(Al.IO)The domain ~@@~ is isomorphic to the domain ~~ defined by~@@~= BOOL <11 ~~@@~.l as follows

V t

NUM, b E BOOL, b

E

:I;

.i :

<t,b> = (A(X) .in~~@@~.l(lift(x»)t(inBOOL (b»<t,.i> = (A(X) .in~@@~.l(lift(x»)t(.i)<oo,.i> =U{ (A (x). in~~@@~.l (lift (x) ) ) t(.i)

I t ~ O}

where, for any function f
fO(x)

=

f t + 1 (x)x= f (ft (x) )The proof is in two parts. Firstly, fixed-point induction is used to prove the isomorphism
for the finite elements of ~@@~ and ~~@@~. The second part of the proof concerns theinfinite elements of the two domains. The only infinite element of ~§@@~ is the least
upper bound of the chain of spine elements of ~@~,

U{ (A(x). in~~@@~.l(lift (x»)t (.i)

I t ~ O} ~@@~, <oo,.i>,

It is proved that the only infinite element of ~@@~, <oo,.i>, is the least upper bound of thechain of spine elements of §@@~,

U{ <t,.i> I t E NUM}.
This completes the proof of isomorphism.

We first define two functions, enlift and delift as follows.

Definition: Projection functions enlift and delift.
enliftenliftA (b) .
(~'l5@~ b ~A'l5~<t,.i>~ (t0 ~.i,

in~~@@~.l (lift (enlift «t-I, .i» ) )<t,torf>~(t = 0~ inBOOL(torf),

in~@@~.l(lift(enlift«t-I,torf»»

175(AI. II)

delift
deliftA(lb) .
(lb = 1.
-7

<0,1.>,(Cases lb ofis§@@~

-7

(b)

<O,b>

is~@@~.1 (lift (lb ' ) )-7 <t+l, lb">

where<t,lb">

delift (lb ' )enlift must be proven to be monotonic as it uses ~1S@~.

Proposition:

enlift is monotonic.

(Al.12)

Proof
Base case:'V b 1 , b 2 E BOOL
enlift«0,b 1»<0, b 1> !;; <0, b 1> ¢::> b 1 !;; b 1
inBOOL(b 1 )enlift«0,b 2»

inBOOL(b 2 )::::) 'V bl'b 2 E BOOL <0,b 1> !;; <0,b 1> ¢::>
enlift«0,b 1»!;; enlift«0,b 2»

Induction step : Assume that for <t 1 ,b 1>,<t 2 ,b 2> E
<t1,b 1> !;; <t 2 ,b 2> ::::) enlift«t1,b 1»§@@~,!;; enlift«t 2 ,b 2»<t1+l,b 1> !;; <t 2+1,b 2>
enlift«t1+l,b 1»

in~§@@~.l(lift(enlift«tl,bl»))enlift«t 2+1,b 2»

in~§@@~.l(lift(enlift«t2,b2»))

enlift «t 1 +1,b 1»!;; enlift «t 2+1,b 2»'V <tl' b 1>, <t 2 , b 2 > E

by induction hypothesis§@@~,<t1,b 1> !;; <t 2 ,b 2> ::::) enlift«t1,b 1»
enlift is monotonic

176!;; enlift«t 2 ,b 2 »For the fmite elements of §@X9)~ and ~~ to be isomorphic we require that
V lb E ~@@~, lb :;:U{ (I\, (x). in~@@~1. (lift (x» ) t

enlift(delift(lb»I t ~ O}

<-l)

= lb

and
V

b

E

m@@~, b :;: <00,1..>delift(enlift(b»Proposition:b

V lb E ~§@@~,
lb :;:(A1.13)

U{ (A(x). in~§@@~1.(lift (x»)t (1..)

I t ~ OJ,

= lb

enlift(delift(lb»ProofBase cases:
delift(1..)=<0,1..>

enlift«O,1..»= 1..

enlift(delift( inBOOL(true)»

inBOOL(true)

enlift(delift( inBOOL(false)»

inBOOL(false)~~, enlift (delift (lb) )Induction step: Assume that for lb E
enlift(delift(in~§@@~1.(lift(lb»enlift«t"+l,lb"»»delift(lb)where <t",lb">in~§@@~1. (lift (enlift «t", lb"»))

where <t",lb"> = delift(lb)in~§@@~1.(

lift(enlift(delift(lb»in~§@@~1.( lift (lb)~ V)

by induction hypothesislb E~m@@~,lb:;:

U{ (A(X). in~§@@~1.(lift(x»)t (1..)

enlift(delift(lb»

)

= lb

177

I t ~ OJ,lb

Proposition:<t,b> E );l@@~, <t,b> ::1= <00,1..>,\;f(A1.14)delift(enlift«t,v») = <t,v>

Proof
Base cases:
enlift«O,1..»delift(1..)

=

= 1..

<0,1..>

delift(enlift«O,b»)delift( inBOOL(b)<O,b>Induction step: Assume that for <t,b> E );l@@~, <t,b> ::1= <00,1..>,delift(enlift«t,b») = <t,b>delift(enlift«t+l,b»)delift(in~);l@@~~(lift(enlift«t,b»)))<t'+l,b'> where <t',b'> = delift(enlift«t,b»)<t, b> by induction hypothesis~ \;f<t, b> E);l@@~,<t, b> ::1= <00,1..>,delift(enlift«t,b») = <t,b>~

The finite elements of );l@@~ and );l@@~ are isomorphic.

The only infinite element of );l@@~ is <00,1..>. The only infinite element of ~);l@@~ isU{ (},,(x). in~@~~(lift(x)))t (1..)

I t ~ o}.Theinfiniteelementof~§@@~isthe least upper bound of the set of spine elements (i.e. those elements of ~);l@@~ formed
by applying the lifting operator to 1.. some finite number of times).

From the ordering on );l@@~ we see that <00,1..> is an upper bound of the set of spine
elements in );l@@~ since\;ft E NUM, <t,1..> C <00,1..>178

Moreover, it must be the least upper bound, as shown by the following

Proposition :<00, .1>(Al. 15)

Proof
Assume ::3 <t',.1> E ~@@~, such that
V <t,.1> E ~@@~ <t,.1> ~ <t',.1> and <t',.1> ~ <00,.1>

Either1.

t'ENUM=>t'+l E NUM=> <t ' +1,.1> E ~@@~=> <t ' ,.1> ~<t' +1,.1> from the ordering on BOOL.

or:

2.

t'

=

00

=> <t' ,.1><00,.1>=> <00,.1> is the least upper bound of the spine elements of ~@@~.

Since the finite elements of ~@@~ and ~~@@~ are isomorphic, and since the infinite
element of ~@@~ corresponds to the infinite element of ~~@@~, ~@@~ and ~~@@~ areisomorphic.

The herring-bone domain construction can be generalised to an arbitrary domain as
follows:

Definition:(A1.16)
General Herring-Bone Domains
Given a domain definition D = F (D), where F (D) is a domain

expression which mayor may not refer to D, let the corresponding
herring-bone domain be rID = F (rID) EEl rID1-

Constructors :<_,>:<00, .1> :NUM x F (rID)

~

rID

~ rID

179

Selectors:(~'lS@~<t,v> ~~'lS~ <t',~> ~ e l , <oo,~> ~ e2' <t',fd'> ~ e 3 )such that(~'lS@~ <t,~> ~~'lS~ <t',~> ~ elf=(I,,(t') .el)<oo,~> ~ e2'<t',fd'> ~ e3)<oo,~> ~ e 2 ,<t',fd'> ~ e 3 )e2(~'lS@~=<t',fd'> ~ e3)(t)(~'lS@~ <oo,~> ~~'lS~ <t',~> ~ elf=<oo,~> ~ e2'<t,fd> ~~'lS~ <t',~> ~ el'(A,(t',d') .e 3 )where fd 1:- ~(t,fd)

and:~<t ' , fd ,> ~ e

<t,v>

~

such that~<t, v> : <t', fd ,> ~ e(~'lS@~~<t, v> ~~'lS~<t' ,~>~<t' ,~>,<t',fd'>~(~'lS@~(A,(t',fd') .e)<t" , ~>~

<max (t ' , t") , ~> ,<t",v">~<max(t',t"),v">

and also:~<t,V> ~ e~such that~<t,v> ~ e=~~<t, v> : <t, v>~(t',fd')

e

~

180

) ~~'lS~Al.3 Non-Primitive Domain Definitions

This section contains the definition of the non-primitive domains used in thesemantics of Ruth. Note that unless the ordering, constructor(s) and selector(s) are
explicitly given for a domain the standard ordering, constructor(s) and selector(s)implied its defining equation are assumed.
Definition:

Environments
Let Id be the syntactic domain of identifiers.

ENV = Id ~(UNDEF EJj W~)(Al.17)

Constructors :
~ENV

(0

&

Selector:such that

Id x W~~ENV

ENV x ENV

~ENV[

ENV x Id ~ UNDEF EJj W~](0 [I]= inUNDEF (Undef)
[I

~

v]

[II]

= (I = II(pI&~ inW~(v),)p2) [I](Cases P2[I]Definition:

inUNDEF(Undef)ofisUNDEF (Undef)

~

else

~ P2 [I]Pl [I](AI.18)Atoms

ATOM = BOOL EJj INT EJj STRING

Definition:(Al.19)Clocked Functions

FUNC@~ ~ FFW~ ~(F EJj W~)

181

Definition:
TUPLE =

Tuples(AI. 20)(~~1. ® TUPLE)~IT!J~ = ©~ $$NIL

§IT!J~1.

Constructors :{}{, ... ,

~

TUPLE

~

TUPLE

such that{ } = inNIL (Nil){ell' e1 2 , ... , elm}in§IT!J~1.®IOTUPLE ( [lift (ell) , {e1 2 , ••• , elm} ] )Selector:

Using pattern matching on {ell' e 1 2 , ••• , elm} structures

Definition:

Input/Output Tuples

IOTUPLE(©~1. ®

=IOTUPLE)(AI.21)$

NIL

Constructors :
{{

}}

{{

, ... ,~(©m~ x

}}

...

x ©~)

IOTUPLE~ IOTUPLE

such that{{}} = inNIL (Nil){ {ch 1 , ch 2 , ••• , ch m} }=in©~1.®IOTUPLE([lift(ch1)' {{ch 2 , . . . ,ch m}}])Selector: Using pattern matching on {{ ch 1 , ch 2 , ••• , ch m}} structures

Definition:

S-expressions

S-EXP

NIL $

PAIR

(§=§~

x

S-EXP $§=~~ 1-

Definition:

ATOM $(AI.22)

PAIR§=~~)1.

Clocks(AI. 23)182

Definition:

Channels(ATOM ® ~.L)

Definition:
W~ =(Al.24)EEl @rnRm.L

Expressible values(A1.25)( S- EXP EEl FUNC EEl TUPLE EEl @~gs EEl ~) EEl WlM1.L

183

Appendix 2 : Formal Presentation Of The
Semantics of Ruth

A2.1 Syntactic Domains
Definition: The Syntactic Domains(A2 . 1)

Pr

E

Prog

C

E ConfProcess ConfigurationsP

E ProcProcesses

Programs

PA E Pr-App

Process Applications

B

E

Bool

Booleans

N

E

Int

Integers

Y

E

StringSymbolic Strings

I

E

Id

Identifiers

E

E

Exp

Syntactic Expressions

D

E Dec

Declarations

A2.2 Abstract Syntax
Definition: Abstract Syntax(A2.2)Pr .. = P ... P C

C.. = Configuration I Output 1 . . . 1
Is PA

P

Input 1 . . . 1... PA.. = Process I Input 1 ... 1 Clock I
Is E

PA .. = 1. .. 1EI

(1. .. 1): := Y I B I N I I

E + E

E - E

E * E

E / E

E \ E IE I E i= E

E ~ E

E ~ E

E < E

E > E

Atom (E)E

isNil (E)Cons (E E)

I Head (E)Tail (E)

ConsCh (E E E)

I HeadCh (E)Time (E)I TailCh (E)

Nil

I E

E

Ready (E E)

I {E ... E}

TailClk(E)I E And E I E Or E!

HeadClk (E)Not E II

I
I

If E Then E Else E I E where D endwhere I
E whererec D endwhererec I lambda (I ... I) E I E (E ... E)

D

::= I

E D I

A2.3 Semantic Domains
Definition: The Semantic Domains(A2 .3)

i,n

E

INT

As defined by (A1. 1)

t,n

E

NUM

As defined by (A1. 1)

b

E

BOOL

As defined by (A1.1)

Y

E

STRINGAs defined by (A1. 1)

NIL

As defined by (A1. 1)

UNDEF

As defined by (A1. 1)

NUM

As defined by (A1. 1)

P

E

ENV

As defined by (A1. 17)

a

E

ATOM

As defined by (A1.18)

f

E

FUNC

As defined by (A1.19)

tp

E

TUPLE

As defined by (A1. 20)

IOTUPLEAs defined by (A1.21)

s

E

S-EXP

As defined by (A1. 22)

s

E

§=ml~

As defined by (A1. 22)

c

E

@~gs

As defined by (A1.23)

ch

E

@~

As defined by (A1. 24)

W~

As defined by (A1. 25)<t,v> E

185

A2.4 Semantic Functions
Definition : The Meaning Functions

epr
ec
ep
epA
tv
eD
e
eB
y

~

(A2 .4)

Prog

~

@~~

~

IOTUPLE~IOTUPLE

Conf

~

ENV

~

@~

~

IOTUPLE

Proe

~

ENV

Pr-App ~ ENV

~

@~~

~ENV

Exp

~

ENV

~

@~~

~W~

Dec

~

ENV

~

@~~

~ENV

Symbol~STRING

Bool

~

BOOL

Int

~

INT

~

IOTUPLEIn defining these functions we will find the following functions useful.

Definition: Environment lookup function(A2 .5)

Id x ENV ~ W~

lookuplookupA(I,P) .
(Cases P[I] of
isUNDEF (Undef)~ <oo,~>

isW~(lift«t,v»

~

<t,v>

Definition: Clock Extraction Function(A2 . 6)

extract
extract
A(e,n) .
~e<t, [1, r] >~(n ~ 0 ~ from(l,t), extraet(from(r,t),n-l»

from

@~~

x NUM ~ @~~fromA(e,n). ~ e : <t c ' [lc,r c ]> ~ <tc+ n + 1 , [lc,r c ]> ID

186)

The following convention is used with extract:v C E @~, n E NUM, C n denotes extract (c,n)

Definition: Ageing Functions(A2 .7)

after
after
c).

A(V,
~

c

: <t e , [Ie' re] >~~v: <t,d>~(t e > t~clockafter@~ x

clockafterA(c,n). from(c,n)<te,v>, after«t,d>,from(le,t e )NUM ~ @~gs

Definition: f il ter Function(A2 .8)filter@illlM1 x NUM x @~gs ~ @ffiRm

filterA(ch,n,c) .<t-n,v>

where
<t,v>

~

c

: <t e , [Ie' re] >~«< ch : <t, [a, lift (rest) ] >~(t e::;; t~<t+ n+ n, [a,lift(rest')]>,

<~,~>

where
rest'

filter (rest,t+n+l,from(le,t e ) )»>In Appendix 1 we defined Cases

...

of

...

selectors for sum domains. In

certain situations we would prefer to be able to test if an element is in a particular
sub-domain and project from that sub-domain directly, without using the cases notation.
The functions defined overleaf allow this.
187

Definition : W~ sub-domain accessing functions out X and(A2. 9)checkX.

v X E{S-EXP, FUNC, TUPLE, @~, ~}outX

S-EXP EEl FUNC EEl TUPLE EEl @~ EEl @rnRm ~checkXS-EXP EEl FUNC EEl TUPLE EEl @~~ EEl @rnRm ~ BOOL

x

outX

A (v) •=(v

= 1.. ~ .i,(Cases v ofisX(x)

~ x

else

~

1..

checkX

A (v) .
(v

= .i ~ .i,(Cases v ofisX (x)

~

true

else

~

false

Definition: S-EXP sub-domain accessing functions outX andcheckX.

v X E {NIL, ATOM, PAIR}
outX

S-EXP

checkXS-EXP EEl FUNC EEl TUPLE EEl @~~ EEl @rnRm ~ BOOL

~

X

outX

A (s) •(s =1.. ~ .i,

(Cases s ofisX(x)

~

else

~.i

x

188

(A2 . 9)

checkX

A(v) .
= 1.- ~ 1.-,(v

(Cases v of
isS-EXP(s)

~

else

v X E

{ INT,(Cases s ofisX (x)

~

true

else

~

false

~ falseBOOL,

STRING}

outX

S-EXP

checkXS-EXP E9 FUNC E9 TUPLE E9 @~~ E9 @rnRm ~ BOOL

~

X

outX

A (v) .
(v =.1 ~ .1,(Cases v of
isATOM(a)

~

else

~

(Cases a ofisX (x)

~

x

else

~.1

.1

checkX

A (v) •(v

= .1 ~ .1,(Cases v of
isS-EXP(s)~(Cases s ofisATOM (a)

~

else

else

~

~

false

189

(Cases a ofisX(x)

~

x

else

~

false

false

Definition: F EB W~ sub-domain accessing functions out X and(A2.10)checkX.

v X E{F, W~}outX

FEBW~~x

checkXF EB W~ ~ BOOL

out X

A (v) .
(v

= 1.. ~ 1..,(Cases v ofisx(x)

~

x

else

~

1..

checkX

A(v) .
(v= 1.. ~ 1..,(Cases v ofisX (x)~ true

else

~

false

Definition: Maximum functionmax

INT x INT~

(A2 .11)

INT

Note that max generalises to any number of arguments as below.
max (il' max (i 2 ,190... , max (i m- 1 ,

i m)

•••

))

For completeness we also include the definition of the Least Fixed Point operator fix.

Definition: The Fixed Point operator fix(A2.12)For any domain 0 the least fixed point of the continuous functional
F

:

fix

0

~ 0

exists and is defined to be fix (F) where(0 ~ 0)~(0 ~ 0)

fix

where

= x

FO (x)

Fn+1 (x)=F (Fn (x) )A2.5 Semantic Equations

The usual convention is followed :

co

c'Pr

[ p l ' •. P k C]
ee[C] p c

C

{{ ch

{{chl'

1,(A2.13).,. ch n }}.. , ch n }}whereee [ Configuration I Output 11 . . . Im Input 1 1 " .I n
Is Pa1 ... Pak ] p c {{ch 1 ,{{ch1,(A2.14)... , chn }}... , chm}}

where
ch j

=

~ lookup(Ij,pc)~: <t,v>(check@rnRm(v)~ out~(v),<oo,~»

~

Pc
pI

fix

(Ap".p I&

epA[pa O]

p"

Co

&

•• ,

&

p & [1 1 ~ <0,in@~(ch1»] &... &[In ~ <0, in@rnRm(ch n ) >]191

ePA[pak] P" ck

Cp[

Process I Input 1 1 ... I n Clock[I ~ <O,f>]Ic Is E ](A2.1S)

where
f

=

inFUNC(AOsc.inF(AO o . . . . inF(AO pc .

inW~(tv[E]([1 1 ~ 01]&&[In ~ On]&

[Ic ~ 0pc]) 0sc ) ) ... »(A2 .16)[1 1 ~<0, in@mmIi(ch 1 »] & ••• & [1 m ~ <O,in@mmIi(ch m»]

where
chj = ~ <tj,ch j >~filter(out@mmIi(chj),O,clockafter(cj,max(t',t j »)<t', inTUPLE ({<t 1 , ch 1>,~

lookup(I,P)~... , <t m , chm>}) >: <t,v>(checkFUNC (v)~ outW~(outF( ...

<t, {<oo,.1>,

outF( f i1 ) ... in ) pc ),... , <oo,.1>} >where
i k = lookup(Ik,p)f = outFUNC(v 1 ) extract (co'O)
pc = in@~~«O,extract(co,l»)tv [ Y ] P c(A2.17)= after«O,inS-EXP(inATOM(inSTRING(Cy[Y]»», c)

tv [

B ]

(A2.18)P c= after«O,inS-EXP(inATOM(inBOOL(CB[B]»», c)(A2 .19)

tv [ N ] P c= after«O,inS-Exp(inATOM(inINT(~[N]»», c)(A2.20)tv[I]pC= after(lookup(I,P), c)192

~ [ El + E2 ] P c(A2 .21)

after (~

<t1,v 1
~ ~<t 2 ,v 2>~(checkINT(v 1 ) A checkINT(V2)~<max(tl,t2),inS-EXP(inATOM(inINT(res))»,<00,1..>

~,

co)

where
res

=

outINT(outATOM(outS-EXP(v 1 ))) +outINT(outATOM(outS-EXP(v2)))

The definitions of - (A2 .22) , * (A2. 23) , / (A2. 24) and \ (A2. 25) can be obtained bysubstituting the relevant operator for + in the definition of res in (A2. 21) •~ [ El = E2 ]Pc

(A2 .26)

after (~

<t 1 , vl>~ ~<t 2 ,v 2>~(checkATOM(v 1 ) A checkATOM(v 2 )~<max(tl,t2),inS-EXP(inATOM(inBOOL(res))»,<00,1..>

~,

co)

where
outATOM(outS-EXP(V2)))

res = outATOM(outS-EXP(v 1 ))The definition of 1= (A2 . 27) can be obtained by substituting 1= for = in the definition of
res in (A2. 26) •193

~ [ El $ E2 ] P c(A2.28)after (~

<t 1 , v 1 ><t 2 ,v 2 >~ ~(checkINT(v 1 )~AcheckINT(v 2 )~<max(tl,t2),inS-EXP(inATOM(inBOOL(res»»,<oo,-L>~,res = outINT(outATOM(outS-EXP(v 1 »)outINT(outATOM(outS-EXP(v 2»)$

The definitions of~ (A2 .29), < (A2. 30) and> (A2. 31) can be obtained by substituting
the relevant operator for $ in the definition of re s in (A2. 28) •~ [ ATOM (E 1 ) ]Pc(A2.32)after (~

<t 1 , v 1 >~(checkS-EXP (vl)~<t1,inS-EXP(inATOM(inBOOL(checkATOM(v1 »»>,
<oo,-L>~,The definition of IsNil (A2 .33) can be obtained by substituting checkNil forcheckAtom in (A2. 32) •~ [ Nil ] P c=(A2.34)after«O,inS-EXP(inNIL(Nil»>, c)194

~ [ Cons (E 1 E 2 ) ] P c(A2 .35)

after«O,inS-EXP(inPAIR(lift([sl,s2]»»'c o)where

sl = «< <t1,vl>~

S2(checkS-EXP(v 1 )~<t 1 ,outS-EXP(v1 »,

<~,~»

~

<t 2 ,outS-EXP(v 2 »,<~,~»«< <t 2 ,v2>~

(checkS-EXP(v2)>}>~ [ Head (E 1 ) ]Pc(A2 .36)

after («< <tl'v1>~(checkS-EXP (v 1 )~(Cases outS-EXP(v 1 ) of
isPAIR(lift([<tH,sH>,<tT,sT>]»~ <max(t 1 ,t H),inS-EXP(sH»else)~ <~,~>

,

<~,~>

~,

(A2 • 37)

~ [ Tail (E 1 ) ] P cafter (~

<t 1 ,v1>~(checkS-EXP (v1)~

(Cases outS-EXP(vl) of
isPAIR(lift([<tH,sH>,<tT,sT>]»else~ <~,~>

) ,
<~,~>

~,

195

~ [ ConsCh(E 1 , E 2 , E 3 ) ]Pc(A2.38)after (~

<t 1 , v 1>
~ ~<t 2 , v 2 >~(checkATOM(v 1 ) A checkINT(V2)
~

(i2

~

~

t

<00,-1>, <t,ch», <00,-1>

~,

co)
where

al

outATOM(outS-EXP(v 1 »)i2outINT(outATOM(outS-EXP(v 2 »)<t,ch> = after«max(tl,t2),in@~«i2' [al,lift(rest)]»>,co)
rest<t"-(i 2+1),v"»
where«< <t 3 ,v3><t",v">~(check@~(v3)~ ~out@~(v3)~ (t' ~t 3~

: <t', [a',lift(ch')]>At' > i 2<t', [a',lift(ch')]>,<oo,-1>~,»>~ [ HeadCh (E 1 ) ](A2.39)Pc

after («< <t 1 , vl>~(check@~(vl)~(~out~(vl)~: <t, [a,lift(ch)]><max(t1,t),inS-EXP(inATOM(a»>),<00,-1>~,196

~ [ Time (E 1 ) ]=Pc(A2 .40)

after (~

<t 1 , v 1 >~(check@~ (vl)~(~out@~(vl)~: <t, [a,lift(ch)]><max(t1,t),inS-EXP(inATOM(inINT(t»»~),<00,.1>~,~ [ TailCh (E 1 ) ]Pc(A2 . 41)

after (~

<tl'v 1 >~(check@~(vl)~ ~ out@~ (v 1 )~: <t, [a, lift (ch) ] ><max(t1,t),

in@~«t'+t+1,v'»>

where<t'V'>~

ch : <t r , Ear' lift (ch r ) ] >~~,<00,.1>~,

197<t r , Ear' lift (ch r ) ] >(A2 0 42)

after
~

<t 1 , V 1 >~ ~<t 2 , V 2 >~(check@~(vl)AcheckINT(v 2 )~ (~'iS@~ out~(Vl)~~'iS~<t,-1>
~

> i2

(t

~

<max(t 1 ,t 2 , i 2 ) ,ff>,<max (t 1 ' t 2 ' t) ,-1><t, [a, lift (ch) ] >
~

> i2

(t

~

<max(t 1 ,t 2 , i 2 ) ,ff>,<max(t 1 ,t 2 ,t),tt>

),
)

,

<00,-1>~,i2 = outINT (outATOM(outS-EXP (v 2 ) ))t t = inS-EXP (inATOM(inBOOL (true)) )ff = inS-EXP (inATOM(inBOOL (false) ))~ [{E1o 00 En}]

Pc(A2043)after«O,inTUPLE({<t1,ch 1 >,~0 0 0' <tn,ch n >}»,

cO)

<tk,vk> :<t,v>~(check@~(v)198~ <t,out@~(v»,<oo,-1»

~ [ ElPc! E2 ](A2 . 44)

after (~

<t 1 , v 1 >~~<t 2 ,v 2> : <t 2 ,i>~(checkTUPLE(v 1 ) A checkINT(v 2 )~(1 ~ i ~ m~<max(tl,t2,ti),chi>,<=,~»,
<=,~>

where
{<tl, chl>,... , <tffi, chffi >}

v1

):»
~,

~ [ HeadClk (E 1 ) ]Pc(A2 .45)

after (~

<t 1 , v 1 >~(check@~gs (v

~

~

1)

out@~gs(vl)~: <t, [1, r] ><max(t1,t),inS-EXP(inATOM(inINT(t»»~,~ [ TailClk (E 1 ) ]

after
~

P c

(A2 • 46)(

<tl'vl>~(check@~gs(vl)~~ out@~gs (vl)~

: <t e , [le' re] ><max(t1,t e ), from(l e ,t e »

~,

~,

199

~ [ El And E2 ] P c(A2 .47)

after (~

<t 1 , v 1 >~ ~<t 2 ,v 2 >~(checkBOOL(v 1 ) A checkBOOL(v 2 )~<max(tl,t2),inS-EXP(inATOM(inBOOL(res»»,<00,.1>~,

res = outBOOL(outATOM(outS-EXP(Vl»)

A

outBOOL(outATOM(outS-EXP(V2»)

The definition of Or (A2 . 48) can be obtained by substituting v for A in the definition ofre S in (A2. 47 ) .

~ [ Not El ]Pc

(A2 .49)

after (~

<t 1 , vl>~(checkS-EXP (v 1 )~<tl'inS-EXP(inATOM(inBOOL(res»

~,

co)

where

res = ~ outBOOL(outATOM(outS-EXP(v1 »)200», <00,.1>

tv [ If El Then E2 Else E3 ] P c~(A2.50)<t l , v l >~(checkBOOL (v l )~(b~ tv [E 2 ] p clockafter(c 2 ,t l ),tv [E 3 ] p clockafter(c 3 ,t l )

),

)

,

~,

where
after (tv [E l ]b

P cl '

co)outBOOL(outATOM(outS-EXP(v l )))tv [ E where D endwhere ] p c(A2.51)

tv[E] (Bn[D] p c l ) Co

tv [ E whererec D endwhererec ] p c(A2.52)

tv[E] pI Co
where

pI

fix (AP" . P & Bn[D] P" Cl)=

tv [ lambda (10".I n ) E ]Pc(A2.53)after«O,f>, c)
where
f = inFUNC (AO c . inF (Aa o . . . . inF(Aa n .

inW~(tv[E] (P
)

&

[10

~ 00]

&

•••

&

[In ~ On]) 0c )... ) )

(A2 . 54)~<t l , vl>~(checkFUNC (vl)~outW~(outF( ...

outF( f <t 2 ,v2> ) ... ) <tn,v n »,

~,

where
<tl,vl>f=

after (tv [E l ] P c lf co)outFUNC(v l ) clockafter(co,t l )201

CD [ I = ED] P C=[I ~ ~[E](A2.55)

P CO] & ~[D] P cl

(A2 .56)202

Appendix 3 . The Syntax of Ruth

A3.1 Introduction

This appendix gives the syntax of Ruth in Extended Backus-Naur Formalism(EBNF). The syntactic rules are of the following form
Non Terminal .. = Syntactic_Expression" I " is used to seperate alternatives in Syntactic Expressions, "[" and"] " enclose an

optional term and "{" and"} " enclose a term which may be repeated any number oftimes (including none). Terminal symbols will be enclosed by " and".

A3.2 Syntactic Equations
Program::= Process Definition,n.n

Process Definition

n_ ..

,

} Configuration

Process Definition.. = "Process" Process Name
"Input" Chan_List"Clock" Ident"Is" Process_Expression
Configuration"Configuration" Ident"Output" Chan_List"Input" Chan_List"Is" Process_Application"end. ",

n.n

Process_Application " ,. "Process_Application::= Chan_List "=" Process Name [ "(" Chan List ")" ]Process_Expression: : = Expression
Expression.. = Lambda _ Exp I Function_Application I If_Exp I Tuple_Exp
Expression "where" Definition_List "endwhere" I
Expression "whererec" Definition List "endwhererec" I
Simple_Exp

Lambda_Exp: : = "lambda" "(" Ident List ") " " " Expression
Function_Application- Predefined Function_Application I
User_Defined_Function Application
If_Exp.. ="If" Expression "Then" Expression "Else" Expression

Tuple_Exp::= "{nSimple_Exp::= Basic_Exp
Definition List::= Definition " ,. "Definition List " ,. "Definition: : = Ident "=" Expression
Predefined_Function_Application.. ="Atom"" (n Expression ")""isNil" "(" Expression ")""Cons" "(n Expression "," Expression ")" I"Head" "(n Expression ")" I"Tail" "(" Expression ")" I"ConsCh" "(" Expression ",n Expression " , " Expression ")" I"HeadCh" "(" Expression ")n I"Time" "(" Expression ")" I"TailCh" "(" Expression ")""Ready" "(n Expression "," Expression ")" I"HeadClk" "(" Expression ")" I"TailClk" "(" Expression ")"User Defined_Function_Application.. = Function Name" (" Exp_List n)"
Basic_Exp· . = [ " +" I " - "] term { Add_ Op term }term::= factor
factorAtom I "(" Expression ")"I "Not" factor I "Nil"Atom· .= Number I Boolean I " , " Symbol " , "Number::= Digit {Digit}
Boolean: : = true I false
Symbol::= Character {Character}
Chan List· .= Chan Name"," Chan Name

204

EXP_List: : = Expression" , " Expression }Ident List
- Ident" , " Ident }Ident- AlphaAlpha_Numeric" "Chan Name::= Ident
Process Name::= Ident
Function Name.. = Ident
Alpha
.. =

"a" ... "z" I"A" ... "Z"

Digit"0" ... "9"CharacterAny printable ASCII Character
Alpha_Numeric: := Alpha I Digit
Rel_Op
::=

"<"

"~"

Add_Op::= "+" I "-". -= n*"I "I"I ">" I

"~,,

"=" I

":;t:"I "Or"I "\""'" I "And"205

Appendix 4· The Minesweep Program

Process Validate Process
Input keyboard
Clock cIs { Time Check (output, c) }whererecoutputValidate (keyboard, start-pos, first_move)

start-posc omp_de lay

1 ; first move
5 ; intervalo;200Time Check
lambda (output, c).
If out time ~ soonest
Then ConsCh (out_data, out_time,
Time_Check (Tail (output) , TailClk(c»)
Else ConsCh (out_data, soonest,
Time_Check (Tail(output), TailClk(c»)
whererecout time
Tail(Head(output»;out data
Head(Head(output»;
soonestHeadClk (c) + check_delay ;check_delay
1 ;endwhererec
Time Check
Validate
lambda (kb, pos, next_move).
If new-pos = pos
Then Validate (TailCh(kb), pos, move_time + interval)
Else Cons (Cons(new-pos, move_time),
Validate(TailCh(kb),new-pos,move_time+interval»
whererecCheck_and_Move (move, pos) ;new-pos
HeadCh ( kb) ;move
If Time (kb) + comp_delay < next move
move time
Then next move
Else Time (kb) + comp_delay
Validate
endwhererec
Check and Movelambda (m, pos).
If m = 'u' And y > 1
Then ((y-2) * array_width) + x
Else If move'd' And Y < array_height
Then (y * array_width) + x
Else If m = '1' And x > 1
Then ((y-1) * array_width) + x-1
Else If m = 'r' And x < array_width
Then ((y-1) * array_width) + x+1
Else pos
whererec((pos-1) \ array_width) + 1;x((pos-1) I array_width) + 1;y2;
array_width2;
array_height
Check and Move
endwhererec
endwhererec

Validate ProcessProcess Cell Process
Input rnd
Clock cIs { Time_Check (output, c)
whererecoutput = Cell (rnd, 0, init_state, init_danger, init~eriod);
Time Check
lambda (output, c).
If out time ~ soonest
Then ConsCh (out_data, out_time,
Time_Check (Tail(output), TailClk(c)))
Else Time_Check (Tail(output), TailClk(c))
whererecout time
Tail(Head(output)) ;out data
Head(Head(output))soonestHeadClk (c) + check_delay
check_delay
250 ;endwhererec ; -- Time Checkin it state=

init_danger

50
20000;

init~eriod

null = -1;

null ;
limit_danger

400;
2500;

limit~eriod

inc danger

5 ;dec~eriod

250

mine = -2 ;Celllambda (rnd, last_out, state, danger, period).
If new state = state
Then Cell (TailCh(TailCh(rnd)), out_time, state, new_danger,
new~eriod)

Else Cons (Cons (new_state, out_time),
Cell (TailCh(TailCh(rnd)), out_time, new_state,
new_danger, new~eriod))whererecout time
last_out + period +((HeadCh(rnd) - 500) * period) / 1000 ;new stateCalculate_State(HeadCh(TailCh(rnd)),danger)
new_period
If (period - dec~eriod) ~ limit~eriod
Then limit~eriod
Else period - dec~eriod ;new_danger
If (danger + inc_danger) ~ limit_danger
Then limit_danger
Else danger + inc_danger ;endwhererec ; -- Cell
Calculate State
lambda (n,danger).
If n > 500
Then n \ 10Else If n < danger
Then mine
Else null ;endwhererec ; -- Cell Process207

,~--~~Process Monitor Process
Input f_cell_l, f_ce 1 1_2 , f_cell_3,
Clock cIs { Time Check (output, c)
whererecf_cell_4, f val

output = Monitor (inputs, init_state, init-player-pos, init_score)o ; init-player-pos = 1 ;init scoreinit statenull= ConS(null,Cons(null,Cons(null,ConS(null,Nil))))=-1 ; mine = -2 ;Time Check
lambda (output, c).
If out time ~ soonest
Then ConsCh (out_data, out time,
Time_Check (Tail(output), TaiIClk(c)))
Else ConsCh (-1, soonest, stop)whererecout time
Tail (Head (output) ;out data
Head (Head (output) ;soonestHeadClk (c) + check_delay ;stop= ConsCh (-1, 0, stop)
check_delay
10 ;endwhererec ;Time Check

inputsScan and Sort (f_cell_l, f_cell_2, f_cell_3, f_cell_4,
f_val, init_scan)
whererecin it scan
200 ;scan interval
200;
Scan- and- Sort
lambda (f_cell_l, f_cell 2, f cell 3, f_cel1_4, f_val,
scan_time) .
Append (Quicksort (event_list, Nil),
Scan and Sort (new_f_cell_l, new_f_cell_2,
new_f_cell_3, new_f_cell_4,
new_f_val,
scan time + scan_interval)
whererecevent list
Get Events ({f_cell_l, f_cell_2, f_cell_3,
f_cell_4, f_val}, 5, scan_time))
new f cell- 1
new f cell 2
new f cell- 3
new f cell 4
new f val
endwhererec ;New Chan (f_cell 1,
New Chan (f- cell_2,
New Chan (f- cell- 3,
New Chan (f- cell- 4,
New Chan (f_val,-- Scan and Sort

check time)check_time)check_time)check time)
scan_time);;

Append = lambda (11, 12)
If 11 = Nil
Then 12Else Cons (Head(ll) , Append (Tail(ll), 12))208

Quicksort= lambda (evll, ev12).
If isNil (evll)
Then ev12
Else Quicksort (sooner,Cons(Head(evll),Quicksort (later,evl2»
whererecsoonerSooner(Tail(Tail(Head(evll»), Tail(evll»
later
Later (Tail(Tail(Head(evll»), Tail(evll»
Soonerlambda (time, evl).
If isNil(evl)Then Nil
Else If time < Tail(Tail(Head(evl»)
Then Sooner(time, Tail(evl»Else Cons (Head(evl) ,Sooner(time,Tail(evl»);Later
lambda (time, evl).
If isNil(evl)Then Nil
Else If time ~ Tail(Tail(Head(evl»)
Then Later(time, Tail(evl»Else Cons(Head(evl),Later(time,Tail(evl»);
endwhererec; -- Quicksort
Get Events
lambda (chs, n, t).
If n < 1
Then Nil
Else If Ready(chs!n, t)
Then Cons(Cons(n, event),
Get_Events (chs, n-l, t) )Else Get Events (chs, n-l, t) ;where
event = Cons (HeadCh(chs!n), T~(chs!n)endwhere ; -- Get Events
New Chanendwhererec

lambda (ch, t ) .
If Ready(ch, t)
Then TailCh(ch)Else ch ;inputs209

Monitorlambda (inputs, state, player-pos, score)score out
whererecevent
Head(inputs) ;event_type
Head (event) ;event data
Head(Tail(event)) ;event time
Tail(Tail(event)) ;out time
event time + comp_delay
comp_delay = 50 ;score out

If Lookup (new_state, new-player_pos)mineThen Cons (Cons (-1, out_time), Nil)
Else If new score # score
Then Cons (Cons (new_score, out_time) , rest)
Else rest ; -- score out

rest = Monitor (Tail (inputs) ,new_state,new_player-pos, new_score ) ;new scoreIf event_type = 5
Then If cell value > 0
Then score + cell value
Else score
Else score
where
cell value = Lookup (state, event data)
new score
endwhere ;new-player-pos = If event_type = 5
Then event data
Else player-pos ;new state

LookupIf event_type ~ 4Then Update (state, event_type, event data)
Else state
whererecUpdate = lambda (st, n, d).
If n ~ 1
Then Cons (d,Tail (st))
Else Cons (Head(st),Update (Tail(st), n-1, d))endwhererec ; -- new statelambda (table, n).
If n ~ 1
Then Head(table)
Else Lookup (Tail(table), n-1)

endwhererec ; -- Monitor
endwhererec ; -- Monitor Process210;Configuration Minesweep
Output score, f_cell_l, f_cell_2, f_cell_3, f_cell_4, f val
Input keyboard, rnd_l, rnd_2, rnd_3, rnd_4
Isscore = Monitor Process (f cell 1,f cell 2,f_cell_3,f_cell_4,f_val);f cell 1
f - cell- 2
f cell 3
f cell 4
f - valend.

Cell Process (rnd_l) ;Cell Process (rnd_2)
Cell Process (rnd_3) ;Cell Process (rnd_4) ;Validate Process (keyboard)211;

References[Abramsky & Sykes 85]

A virtual machine for applicative multiprogramming
S. Abramsky and R. Sykes
Functional Programming Languages and Computer Architectures
Springer-Verlag LNCS 201, 1985
[Apt & Plotkin 81]

A cook's tour of countable non determinism
K.R. Apt and G. Plotkin
8 th International Colloquium on Automata, Languages and Programming
Springer-Verlag LNCS 115.
[Apt & Olderog 83]

Proof rules and Transformations dealing with fairness
K.R. Apt and E-R. Olderog
Science o/Computer Programming No.3, pp 65-100.1983[Ashcroft & Wadge 76]

LUCID - A Formal System for Writing and proving programs
E.A. Ashcroft and W.W. Wadge
SIAM Journal o/Computing Vol. 5, No.3. Sept 1976
[Ashcroft & Wadge 77]

LUCID, a NonProcedural Language with Iteration
E.A. Ashcroft and W.W. Wadge
Communications o/the ACM Vol. 20, No.7. July 1977
[Ashcroft & Wadge 80]

Some common misconceptions about Lucid
E.A. Ashcroft and W.W. Wadge
ACM SIGPLAN Notices Vol. 15, No. 10. Oct 1980
[Backus 78]

Can Programming be Liberated from the von Neumann style? Afunctional style and its Algebra of Programs
J. Backus
Communications o/the ACM Vol. 21, No.8. August 1978

[Baker 78]

List Processing in Real Time on a Serial Computer
H.G. Baker
Communications of the ACM Vol. 21 No.4 April 1978
[Bergerand et. al. 85]

Outline of a Real-Time Data Flow Language
J.L. Bergarand, P. Caspi, D. Pilaud, N. Halbwachs and E. Pilaud

Proceedings IEEE Real-Time Systems Symposium
San Diego, California December 1985.
[Bergerand et. al. 86]

Automatic Control Systems Programming using a Real Time
Declarative Language
J.L. Bergarand, P. Caspi, N. Halbwachs and J.A. Plaice

IFACIIFIP Symposium on Software for Computer Control {SOCOCO 86}
Graz (Austria) May 1986
[Berry & Cosserat 84]

The ESTEREL Synchronous Programming Language and its
Mathematical Semantics
G. Berry and L. Cosserat

Proceedings Seminar on Concurrency, Carnegie-Mellon University
Pittsburg 1984.
Springer-Verlag LNCS 197[Berry et. al. 86]

Synchronous Programming of Reactive Systems
G. Berry, P. Couronne and G.Gonthier

Proceedings France-Japan Artificial Intelligence and Computer Science
Symposium
Institute for New Generation Computer Technology, October 1986
[Berry et. al. 87a]

Synchronous Programming of Reactive Systems: An Inroduction to
ESTEREL
G. Berry, P. Couronne and G.Gonthier
INRIA Rapports de Recherche No. 647. March 1987

213

[Berry et. al. 87b]

The ESTEREL v2.2 System Manuals
G. Berry, P. Couronne and G.GonthierRapports Technique ENSPMP /INRIA May 1987
[Bird & Wadler 88]

Introduction to Functional Programming
R. Bird and P. Wadler
Prentice-Hall International 1988
[Bjorner & Oest 80]

Towards a Formal Description of Ada
Eds : D. Bjorner and O.N. Oest
Springer-Verlag LNCS 98[Broy 82]

A Fixed point approach to Applicative Multiprogramming
M. Broy
Theoretical Foundations of Programming M ethodolo gy

Eds. M. Broy and G. Schmidt
D. Reidel Publishing Company 1982
[Broy 83]

Applicative Real-Time Programming
M. Broy
Proceedings IFIP 1983

North-Holland Information Processing 1983.
[Burstall & Darlington 77]

A Transformation System for Developing Recursive Programs
R.M. Burstall and J. Darlington
Journal of the ACM Vol. 24, No.1. January 1977

[B urstall et. al. 80]

HOPE: An Experimental Applicative Language
R.M. Burstall, D.B. MacQueen and D.T. Sane1la
Report CRS-62-80 May 1980
Dept. of Computer Science, University of Edinburgh.

214

[Burton 88]

Nondeterminism with referential transparency in Functional
Programming Languages
F.W. Burton

The Computer Journal Vol. 31, No.3. 1988
[Cartwright & Donahue 82]

The Semantics of Lazy {and Industrious} Evaluation
R. Cartwright and J. Donahue

Proceedings 1982 Symposium on Lisp and Functional Programming
Pittsburg 1982
[Caspi et. al. 87]

LUSTRE: A Declarative Language for Programming Synchronous
Systems
P. Caspi, D. Pilaud, N. Halbwachs and J.A. Plaice

Conference Record o/the 14th Annual ACM Symposium on Principles ofProgramming Languages
January 1987
[Darlington & Reeve 81]

Alice, a multiprocessor reduction machine for the parallel evaluationof applicative languages
J. Darlington and M. Reeve
Internal Report, Dept of Computing Science, Imperial College 1981.
[Darlington 82]

Program Transformation
J. Darlington

Functional Programming and its Applications
Eds. J. Darlington, P. Henderson and D.A. TurnerCambridge University Press 1982
[Faustini & Lewis 85]

A Declarative Language for the Specification of Real Time Systems
A.A. Faustini and E.B. Lewis

Proceedings IEEE Real-Time Systems Symposium
San Diego, California. December 1985.

215

[Faustini & Lewis 86]
Toward a Real-Time Dataflow Language
A.A. Faustini and E.B. Lewis
IEEE Software January 1986

[Friedman & Wise 76]
Cons should not evaluate its arguments
D.P. Friedman and D.S. Wise
Automata Languages and Programming Third International Colloquium
Eds. S. Michaelson and R. Milner

Edinburgh University Press 1976
[Harrison 87]
RUTH: A Functional Language for Real-Time Programming
D. Harrison
Proceedings Parallel Architectures and Languages Europe

Eindhoven, June 1987
Springer-Verlag LNCS 259[Harrison & Nelson 89]
A Real-Time Language Based on Explicit Timeouts
D. Harrison an S . Nelson
University of Stirling, Department of Computing Science
Technical Report 1989
[Henderson & Morris 76]
A Lazy Evaluator
P. Henderson and J.H. Morris
Conference Record of the 3 rd Annual ACM symposium on Principles ofProgramming Languages

January 1976
[Henderson 80]
Functional Programming: Application and Implementation
P. Henderson
Prentice-Hall Internationa11980

216

[Henderson 82]

Purely Functional Operating Systems
P. Henderson

Functional Programming and its Applications
Eds. J. Darlington, P. Henderson and D.A. TurnerCambridge University Press 1982
[Henderson et. al. 83]

The LispKit Manual
P. Henderson, G.A. Jones and S.B. Jones
Oxford University Computing Laboratory
Programming Research Group Monograph 32[Holmstrom 83]

PFL : A Functonal Language for Parallel Programming
S. Holmstrom

Proceedings Declarative Programming Workshop
University College London II-13th April 1983
[Hudak et.al. 89]

Report on the Functional Programming Language Haskell
P. Hudak (Editor), P. Wadler, Arvind, B. Boutel, J. Fairbairn, J. Fasel, J. Hughes,
T. Johnsson, D. Kieburtz, S. Peyton Jones, R. Nikhil, M. Reeve, D. Wise andJ. Young
University of Glasgow, Department of Computing Science,
Research Report CSC/89/R5 March 1989
[Ida & Tanaka 83]

Functional Programming with Streams
T. Ida and J. Tanaka

Proceedings IFIP 1983
North-Holland Information Processing 1983
[Ida & Tanaka 84]

Functional Programming with Streams - Part IT
T. Ida and J. Tanaka
New Generation Computing 2, pp 261-275.1984[!NMOS 84]

OCCAM Programming Manual
Inmos Ltd.
Prentice-Hall International Series in Computer Science 1984
217

[INMOS 87]

Preliminary Data: IMS T414 Transputer
Inmos Ltd. 1987
[Jones 84a]

Abstract Machine Support for Purely Functional Operating Systems
S.B. Jones
University of Stirling, Department of Computing Science
Technical Report T.R.15. September 1984
[Jones 84b]

A Range of Operating Systems Written In A Purely Functional Style
S.B. Jones
University of Stirling, Department of Computing Science
Technical Report T.R.16. September 1984
[Jones & Sinclair 89]

Functional Programming and Operating Systems
S.B. Jones and A.F. Sinclair
The Computer Journal Vol. 32, No.2. Feb. 1989
[Lamport 78]

Time, Clocks and the Ordering of Events in a Distributed System
L. Lamport
Communications o/the ACMVol. 21, No.7. July 1978
[Landin 64]

The Mechanical evaluation of Expressions
P.J. Landin
The Computer Journal Vol. 6 pp308-320. 1964
[Le Guernic et. al. 85]
SIGNAL: A Data Flow Oriented Language for Signal Processing
P. Le Guernic, A. Benveniste, P. Bournai and T. Gautier
IRISA Internal publication 246. January 1985
[Le Guernic et. al. 86]
SIGNAL - A Data Flow-Oriented Language for Signal Processing
P. Le Guernic, A. Benveniste, P. Bournai and T. GautierIEEE Transactions on Acoustics, Speech and Signal Processing Vol. ASSP-34,
No.2. April 1986

218

[Le Guernic & Benveniste 87]

Real-Time, Synchronous, Data-Flow Programming: The Language
SIGNAL and its Mathematical Semantics
P. Le Guemic and A. Benveniste
INRIA Rapports de Recherche No. 620. February 1987
[Le Lann 83]

On Real-Time Distributed Computing
G. LeLann

Proceedings IFIP 1983
North-Holland Information Processing 83.
[Liebermann & Hewitt 83]

A Real-Time Garbage Collector Based on the Lifetimes of Objects
H. Liebermann and C. Hewitt

Communications of the ACM Vol. 26 No.6. June 1983
[MoD 70]

Official Definition of Coral-66
Ministry of Defence 1970
[McCarthy 60]

Recursive Functions of Symbolic Expressions and Their Computationby Machine, Part I
J. McCarthy

Communications of the ACM Vol. 3, No.4. April 1960
[McCarthy 63]

A basis for a mathematical theory of computation
J. McCarthy
Studies in logic: Computer programming andformal systems
Eds. Braffort and Hirschberg
North Holland 1963.
[Partsch & Steinbruggen 83]

Program Transformation Systems
H. Partsch and R. Steinbruggen
ACM Computing Surveys Vol. 15, No.3. September 1983

219

[Peyton Jones 85]

GRIP - a parallel graph reduction machine
S.L. Peyton Jones
University College London Internal note 1665. January 1985
[Peyton Jones 87]

The Implementation of Functional Programming Languages
S.L. Peyton Jones
Prentice-Hall Internationa11987[Sannella 81]

HOPE Update
D. Sannella
University of Edinburgh, Dept. of Computer Science. February 1981
[Schmidt 86]

Denotational Semantics, A Methodology For Language Development
D .A. Schmidt
Allyn and Bacon 1986
[Sherlis 80]

Expression Procedures and Program Derivation
W.L. Sherlis
Ph.D. Thesis
Dept. Of Computer Science, Stanford University
Report No. STAN-CS-80-818. August 1980
[Shin 87]

Introduction to special issue on Real-Time systems
K.G. ShinIEEE Transactions on Computers Vol. c-36, No.8. August 1987
[Stoy 77]

Denotational Semantics: The Scott-Strachey Approach toProgramming Language Theory
J. Stoy
The MIT Press 1977
[Stoye 86]

Message-Based Functional Operating Systems
W. Stoye
Science of Computer Pro gramming No.6, pp 291-311. 1986
220

[Thompson 86]

Writing Interactive Programs in Miranda
S. Thompson
UKC Computer Lab. Report No. 40. University of Kent, August 1986
[Turner 85]

Miranda: A non-strict functional language with polymorphic types
D.A. Turner

Proceedings, Functional Programming Languages and Computer Architecture
Nancy, France. Sept 1985
Springer-Verlag LNCS 201[Turner 87]

Functional programming and communicating processes
D.A. Turner

Proceedings Parallel Architectures and Languages Europe
Eindhoven. June 1987
Springer-Verlag LNCS 259[USDOD 83]

Programming Language Ada: Reference Manual
U.S. Dept. of Defence 1983
Springer-Verlag LNCS 155[Wadge & Ashcroft 85]

Lucid, the Dataflow Programming Language
W.W.Wadge and E.A.Ashcroft
Academic Press, London 1985
[Wirth 83]

Programming in Modula-2
N. Wirth
Springer-Verlag 1983
[Young 82]

Real Time Languages design and development
S.J. Young
Ellis-Harwood Publishers 1982.

221