|
CO538 Anonymous Questions and Answers Keyword Index |
This page provides a keyword index to questions and answers. Clicking on a keyword will take you to a page containing all questions and answers for that keyword, grouped by year.
To submit a question, use the anonymous questions page. You may find the keyword index and/or top-level index useful for locating past questions and answers.
Keyword reference for formal-semantics
2012 |
Submission reference: IN2167
In the last lecture (Friday, 19 Oct), someone asked about the position of the replace gadget in the integrate process with a reset line ("Choice" slide 52): could it have been placed on either of the other two internal channels instead? Could you go over that again please?
I don't think I answered that question very well, changing my mind to say: "yes, it doesn't really matter where the replace is placed in the circuit". That's true ... but only if we take a fairly relaxed view of the semantics of the device. If we take a strict view, there are low-level differences in the behaviours possible from the device, depending where that replace is placed – see below. However, for real-time control applications, such as the inertial navigation component described in "Choice" slides 53-56 (and in the "occam Approach to Transputer Engineering" paper), we can take the relaxed view – see the end of this answer.
A simpler system to consider first is the numbers.reset circuit in slide 49. If no resets are sent, this just generates: 0, 1, 2, 3, 4, 5, etc. Suppose we send the number 42 down the reset line just once. The output sequence depends, of course, on when that reset happens. Possible output sequences are:
42, 43, 44, 45, 46, 47, ...
0, 42, 43, 44, 45, 46, ...
0, 1, 42, 43, 44, 45, ...
0, 1, 2, 42, 43, 44, ...
0, 1, 2, 3, 42, 43, ...
0, 1, 2, 3, 4, 42, ...
etc.
However, if the replace gadget were spliced into the d channel (between succ and prefix), there is no way the 42 could ever get in quick enough to prevent the first 0 from coming out – i.e. the first output sequence line above would not be possible.
If replace were spliced into the c channel (between delta and succ), not only could the first 0 not be replaced but the reset sequence could only start from 43. Possible output sequences are:
0, 43, 44, 45, 46, 47, ...
0, 1, 43, 44, 45, 46, ...
0, 1, 2, 43, 44, 45, ...
0, 1, 2, 3, 43, 44, ...
0, 1, 2, 3, 4, 43, ...
etc.
So, the actual reset number, 42, would not come out.
Compare the above with what the numbers.reset serial implementation (slide 50) can do with the same scenario (a single reset of 42). If the reset happens early enough, the 42 will overwrite the variable n on the first loop and will come out first – the 0 will not be seen. I hope it is clear that the possible output sequences are the same as the first set above – i.e. the same as those produced by the parallel implementation (slide 49), with the replace gadget between prefix and delta. So, for this scenario anyway (and actually for all), the two implementations of numbers.reset (slides 49 and 50) give rise to the same component – at least, if we are only considering the possible output sequences they produce. If the position of replace in slide 49 is changed, we have noted differences in the possible output sequences, which may or may not be significant (depending on the application in which it is used).
The "at least" qualification two sentences back needs explaining. The full semantics of a device is more than just the outputs it makes for given inputs and the timings of those inputs. We need also to know about the patterns of all events (i.e. input and output communications and, later, barrier synchronisations) in which it can engage. For instance, how may the inputs events interleave with output events? In many circumstances, we need this information to avoid deadlock.
When we consider possible interleavings for the numbers.reset implementations of slides 49 and 50, some differences do emerge. In the serial implementation (slide 50), here is the sequence of events when a single reset event occurs:
...
out ! x
out ! x + 1
out ! x + 2
reset ? y
out ! y
out ! y + 1
out ! y + 2
...
where time is flowing downwards and x and y represent generic values. Note that the output of the reset value is the next event following the reset input. No other interleavings of input and output events are possible.
Now, consider the parallel implementation (slide 49). The above sequence is certainly a possibility but so, also, is the following:
...
out ! x
out ! x + 1
out ! x + 2
reset ? y
out ! x + 3
out ! y
out ! y + 1
out ! y + 2
...
It all depends on where the previously cycling number is in the feedback circuit when the reset is taken by replace. If it is in succ or prefix, we will get the first pattern. If it is in delta, we will get the second.
So the parallel and serial implementations of number.reset are different. The serial form is more constrained in the way it syncrhonises with its environment (i.e. the other processes in the network in which it is embedded). Everything it does can also be done by the parallel version, but the parallel version may choose to do things differently.
Note: when considering the semantics of a process, it is only its impact on its environment that is relevant. That is why, when thinking about the patterns of events in which a process can engage, it is only those that interact with its environment (e.g. external input and output channels) that are important. Hence, in the above sequence (and the ones that follow), we only include events involving the channels from the parameter list – not the internal ones.
Now, let's get back to the integrate process, first comparing the serial and parallel versions of the original process – the one without any reset channel. Consider the serial version (slide 57). Its synchronisation pattern is tightly constrained: a strictly alternating sequence of inputs and outputs:
...
out ! r -- running total, so far
in ? x
out ! r + x -- running total, so far
in ? y
out ! r + x + y -- running total, so far
in ? z
out ! r + x + y + z -- running total, so far
...
This serial version "buffers" one item of the flow of numbers from its input channel to its output (i.e. in any state, the number of inputs it has taken is either the same as its number of outputs or one more).
As noted in "Basics" slide 94, the parallel version "buffers" two items of the flow of numbers from its input to output (i.e. in any state, the number of inputs it has taken is either the same as its number of outputs or one more or two more). This allows it greater flexibility in the way it synchronises. The above pattern can certainly happen, but so can:
...
out ! r -- #in? = #out!
in ? x -- #in? = #out! + 1
in ? y -- #in? = #out! + 2
out ! r + x -- #in? = #out! + 1
in ? z -- #in? = #out! + 2
out ! r + x + y -- #in? = #out! + 1
out ! r + x + y + z -- #in? = #out!
...
where "#in?" means the number of inputs so far and "#out!" means the number of outputs so far. Other patterns may occur, so long as:
0 <= (#in? - #out!) <= 2
Note that, viewed separately, the output sequence for any given input sequence is the same for both the serial and parallel versions. However, the difference in buffering capacities may be significant for deadlock analysis. The more constrained pattern of synchronisation forced by the serial version increases the potential for deadlock in a poorly designed application that uses it.
Now consider the serial and parallel versions of integrate.reset ("Choice" slides 51 and 52). The serial version still buffers only one running total (either the most recently computed value or one that's just been reset). Its synchronisation pattern is also tightly constrained: a strictly alternating sequence of either an input or reset event, followed by an output event. For example:
...
out ! r -- running total, so far
in ? x
out ! r + x -- running total, so far
in ? y
out ! r + x + y -- running total, so far
reset ? a
out ! a -- the reset running total
in ? z
out ! a + z -- running total, so far
...
The parallel version (slide 52) can buffer up to three running totals: one in plus (the most recent), one in replace (either the second most recent or a reset value) and one in delta (the oldest). This gives much greater flexibility to the patterns of synchronisation possible. Again, the above pattern is possible. But also:
...
out ! r -- running total, so far
in ? x -- 'r+x' moves through 'replace' to 'delta'
in ? y -- 'y' only gets into 'plus' (which needs its other input)
reset ? a -- 'a' gets into 'replace'
out ! r + x -- running total, so far
-- 'r+x' fed back through 'prefix' to 'plus'
-- 'r+x+y' computed, moves to 'replace' and is discarded
-- 'a' moves into 'delta'
out ! a -- the reset running total
in ? z
out ! a + z -- running total, so far
...
and many others. Notice that in the above sequence, one of the running sums of input values (r+x+y) never emerged. Whether missing this value is significant depends on the application.
Now, consider what happens if the replace gadget in the parallel implementation (slide 52) were positioned elsewhere. For one thing, the buffering capacity between the in and out channels drops back to two. If replace were spliced into the channel between prefix and plus, the reset value would never emerge as itself – it would always first have been added to the next input value. For example:
...
out ! r -- running total, so far
in ? x -- 'r+x' moves to 'delta'
in ? y -- 'y' only gets into 'plus' (which needs its other input)
reset ? a -- 'a' gets into 'replace' and moves on to 'plus'
-- 'a+y' computed in 'plus', cannot move on yet
out ! r + x -- running total, so far
-- 'r+x' fed back through 'prefix' to 'replace', which discards it.
-- 'a+y' moves to 'delta'
out ! a + y -- the reset running total (with added 'y')
in ? z
out ! a + y + z -- running total, so far
...
In the previous example, the contribution of 'y' was never seen in the running sum outputs. This time it is, but added to the reset value (which is not seen directly).
If replace were spliced into the channel between delta and prefix, the reset value would never emerge as itself – it would always first have been added to the next input value (as for the previous version). The difference is at start-up – there is no way a reset could happen fast enough to prevent the first output from always being the first input added to the initial 0 from prefix (i.e. the first output is always the first input).
A sequence of events (channel communications and, later, barrier synchronisations) in which a process can engage is called a trace.
The last 7 sequences above show extracts from traces of the processes being considered. For clarity, we've listed them in two columns: one for input and one for output. For traces, consider them listed in one column, keeping the ordering.
CSP (Communicating Sequential Processes), the formal algebra that underlies occam-pi, defines three semantic models with increasing capabilities: traces, failures and divergences. The simplest is the traces model, which enables verification of safety properties (e.g. that a process will not do something bad). The other two concern liveness properties (e.g. that a process will actually do something): failures enable deadlock analysis and divergences address livelock.
In the traces model, the semantics of a process is just defined by: the set of all its possible traces. Two processes are equivalent if their traces are the same set. A process, P, is a refinement of a process, Q, if the traces of P are a subset of the traces of Q. This is where safety analysis comes in: if a process Q is known to have safe behaviour and we implement a process P and prove that it refines Q, then we know that P also must be safe (because every trace that P can do, Q can do and Q only does safe things). In such a scenario, Q is usually described as a specification for P.
The position of the replace component in the parallel circuits of numbers.reset (slide 49) and integrate.reset (slide 52) does impact on their formal semantics.
The serial numbers.reset (slide 50) is a traces refinement of the parallel implementation in slide 49. The serial integrate.reset (slide 51) is a traces refinement of the parallel implementation in slide 52.
If, however, the replace component is repositioned somewhere else in the circuits, there is no formal relationship between the serial and those parallel versions. Whether the differences (see earlier) matter depends on the applications to which they are put.
For the inertial navigation component (slides 53-56), they don't matter. All the versions of integrate.reset (serial or any of the three parallel implementations considered above) deliver running sums and allow resets at any time. The precise interleaving of inputs, resets and outputs doesn't matter – the important matter is the accuracy of the input sample values and the accuracy of their sampling times (which must be evenly spaced). If some running sum is discarded when a reset happens, it doesn't matter: that value was suspect anyway, which is why integrate.reset was being reset. If the reset value does not get output itself, it doesn't matter: the value that comes out is the reset value plus the latest input, which is more up-to-date than the reset value alone. Finally, if we can't reset before the first number appears after integrate.reset is switched on, who cares?
Keywords: q4 , csp , formal-semantics , reset
|
This work is licensed under a Creative Commons Attribution-Share Alike 3.0 Unported License. |
