Sequential Control
Goals for this lecture :
- To introduce guarded commands.
- To introduce the alternive guarded command.
- To introduce the repetitive guarded command.
- To introduce weakest precondition semantics.
Click here ,
here , and
here for these notes in postscript
In a concurrent programming language such as SR there are
three kinds of control mechanism not often found in determinisitic sequential
languages ( Slide 1 ) such as Java.
- Parallel Execution : in SR this is
interleaving expressed in terms of synchronous and
asynchronous invocation, e.g. processes.
- Synchronisation : in SR we have
semaphores and rendezvous primitives.
- Sequential Control : in SR we have
Dijkstra's guarded commands for non determinisitic
control.
Today we will be studying the last of these, sequential control.
In determinisitic sequential languages we make conditional choices to
decide which statement should be executed next
( Slide 2 ).
In this example a symmetric function has to be coded up in
a very non symmetric manner.
To code such a function symmetrically we need a non deterministic
choice construct.
Such facilities for non deterministic choice are not often to be
found in determinisitic sequential languages.
However, in concurrency where non detrerminism is so pervasive we
make extensive use of programming conditional choices from which
the computer will choose any option passing its condition.
What we are looking for (and we find in SR) is a language
notation for expressing such non determinisitic choices.
After introducing parallel compounds in 1968 we find that it was
Dijkstra who later gave us such a notation.
Today's lecture refers to Dijkstra's seminal
paper [ Di75 ] on
Guarded Commands, Nondeterminacy and Formal Derivation of
Programs
( Slide 3 ).
Guarded commands are used extensively in SR to programme
Sequential Control are required reading for the course.
non deterministic sequential control, and so it is well worth
reading Dijkstra's paper to see how they came about.
Dijkstra's motivation for guarded commands is not concurrency
but rather to assist with the formal reasoning of Algol-like
(i.e. Pascal-ish) programs.
See the page
[ Di71 ]
for some more insight as to his motivation.
By including deterministic code in a program to make choices
which could be left to the computer we are unnecessarily
complicating the program, and so making it equally unnecessarily
harder to reason about its correctness.
Why make programming harder than it has to be?
A Gaurded Command,
is a statement `pre-fixed' by a boolean expression termed
a guard
( Slide 4 ).
To execute a guarded command we first evaluate the guard, then
execute the statement if the guard is true, otherwise do nothing.
On its own a single guarded command does not amount to much,
it is only when we combine them together non deterministically
that we get a choice.
A Guarded Command Set,
is a set of guarded commands
( Slide 4 ).
Note that it is a `set', that is, the order of the guarded
commands is not important.
The exact execution of a guarded command set will depend upon
the implementation, we just need to describe what has to be done.
To execute a guarded command set we choose a guarded command
whose guard evaluates to true (if it exists!) and then execute its command.
If there is no such guard then there is nothing to do.
In contrast to an if-then-elseif-then-... construction
in deterministic sequential programming there is no programming
of the order in which guards are evaluated.
On a single processor machine we would probably evaluate the
guards from left to right until (if ever!) we find a guard that evaluates
to true
( Slide 5 ).
On a parallel architecure (or a parallel simulation like SR)
it would make sense to evaluate all guards at once and choose
that command whose guard first (if ever!) evaluates to true.
The important point is that we as programmers don't need to know
how the guards are evaluated.
All we need to understand is that non deterministic choices can be
expressed (but not implemented!) using guarded commands.
For example to non deterministically choose either a 0 or
1 for a variable x we write
(using SR notation),
true -> x := 0 [] true -> x := 1
There are two kinds of construct built from a guarded command set
which we now discuss.
The first construct is the non deterministic counterpart
to the deterministic if-then-else statement.
The Alternative Construct
( Slide 6 )
is a guarded command set surrounded by the if-fi
brackets.
SR has no if-then-else, but that is simply
because we can build an equivalent expression in terms of
Dijktra's alternative construction
( Slide 6 ).
In Slide 7
we produce a symmetric implementation for the function
min disccussed in
Slide 2.
A guarded command is not an atomic action, and so must not
be put at risk from possible interference
( Slide 8 ).
Our example shows a possible pathological interleaving whose
affect is to prevent inc
incrementing x
which it should otherwise be able to do according to the
Law of the Excluded Middle
[ Le65 ],
that is, one guard must always be true.
The logic of an alternative can thus be made totally absurd if
interference is allowed to take place.
Preferably guarded commands should only be used with variables not
subject to change elsewhere.
If there is a risk then some sychronisation must be used to preserve
the guarded command's integrity.
Now try Exercise 1.
At this point we should mention the semantics for guarded commands
given in Dijkstra's paper.
Dijkstra uses the weakest precondition to define the
affect a guarded command has on changing states.
His semantics was not in the context of concurrent programming,
but for the formal reasoning of sequential programs.
Thus Dijkstra's semantics holds for concurrent programming as
long as there is no interference.
This is the only way we can reasonably use guarded commands in
a language such as SR.
Guarded command sets are usually simplest when the degree of non
determinisitic choice is high.
However, it may be the case that the choice has to be uniquely
determined according to, what would be called elsewhere, a
case analysis
( Slide 9 ).
We begin by looking for all possible mutually exclusive cases.
In our example with two cases for each of a and b
we first deduce that there are 2*2 = 4 cases for
x to find.
A common experience is that after finding all the possible
cases we can combine some together.
It is best to look for the most exhaustive partition first and subsequently
refine it.
Don't try to pluck it out of thin air straight away.
This is Dijkstra's non deterministic generalisation for Pascal's
while-do and repeat-until loops
( Slide 10 ).
It is a guarded command set surrounded by the
do-od brackets.
The guarded command set is repeatedly executed until (if ever!)
all the guards evaluate to false.
Also in Slide 10 an example of using a one arm
repetitive construct for computing integer division by 2.
Now we consider the use of else in Dijkstra's constructs
( Slide 11 )
firstly in an alternative, and then in a repetitive one.
else is intended to be the negation of the disjunction
of all the guards, that is, a default when all the `real' guards
evaluate to false.
our first example is an application to
HTML codes.
In the second example of an alarm clock we need to insert a
stop command to terminate the program after the alarm
has gone off.
Having an else in a reptitive construct means that the
loop will never terminate unless forced to by something such as
stop.
Now try Exercise 2 and
Exercise 3.
SR has a for all loop much as in Pascal
( Slide 12 ).
However, its notation is more in keeping with that of
Dijkstra's constructs.
Sadly we don't have time to study the semantics of an
SR-like language
( Slide 13 ).
What we can do however is study the semantics of
Dijkstra's constructs using the weakest precondition
he suggests in his paper.
I am not going to lecture on the weakest precondition for the
following reason.
I want students to be exposed to at least one classic research
paper in concurrency.
This paper is as short and as straightforward as any, so this
will be your `research' experience.
Given that non determinism is such a tricky subject it is worth
asking whether or not SR implements guarded commands correctly
( Slide 14 ,
exp.sr ).
The unfairness usually found in the handling of guarded commands
should not be misinterpreted as an incorrect implemetation of
Dijkstra's constructs
( Slide 15 ).
java is a deterministic sequential programming langauge, and as such despite all its
other undoubtee strengths does not empower us to make non deterministic choices.
We could simulate guarded commands by setting up a thread to evaluate each of a set
of guards; the first thread to return true would determine which statement would be
executed.
We can thus employ guarded commands as a design tool for writing concurrent Java programs,
even though they are not supported by the language itself.
I suspect that for reasons of efficiency and portability Java would find non deterministic
choice too higher leve concept to include.
Sequential Control - Exercise 1
In Exercise 3
of the busy waiting lecture you were asked to use the bakery algorithm
to decide which process should get the next turn.
If you've already attempted this question look at my answer, otherwise have a go
at it.
Does my procedure serving have any problems with
interference? Discuss this.
My answer
Sequential Control - Exercise 2
In Dijkstra's paper read about Euclid's Algorithm
for finding the greatest common divisor of two positive
numbers.
I can furnish anyone interested with a copy of this paper.
Test your understanding of this by writing an SR program
to compute a gcd of two integers given at run time.
Your program should have error handling in case one or
both of the integers input is mistakenly non positive.
My answer
Sequential Control - Exercise 3
Improve the HTML code program in
Slide 11
to distinguish between those codes which are unused, and those
which are used but not letters.
My answer