convert from svn repository: remove tags directory

[lttv.git] / trunk / verif / Spin / Doc / Book.answers

Answers to selected exercises from
'Design and Validation of Computer Protocols'
=============================================

1.1
Assuming that torches in the two groups would be
raised and lowered simultaneously,
the code for the first character in the first group
could have clashed with the pre-defined start of text code.

If torches are not raised simultaneously it is conceivable
that group numbers could be paired with the wrong character numbers.

A well-trained transmitter might also overestimate the receiver's
ability to translate the codes on the fly.
as is still true today: receiving is a more time consuming task
than transmitting.

1.2
Assuming that a torch code is displayed for a minimum of 30 seconds,
the torch telegraph transmits a choice of 1 out of 25 (between 4
and 5 bits of information), giving a speed of roughly 0.15 bits/sec.
Chappe's telegraph transmitted a choice of 1 out of 128 every 15 to 20
seconds, giving a transmission speed of roughly 0.5 bits/sec.
On Polybius' telegraph the 15 characters of the message
``protocol failure'' would take 15x30 seconds or 7.5 minutes to transmit...
(Note that a code for the space was not available.)
On Chappe's system the 16 characters (space included) would be
transmitted in 4 minutes, assuming that no predefined code
was assigned to either the word `protocol' or the word `failure.'
(As far as we know, there wasn't.)

1.3
Removing the redundancy in messages increases the chance that a
single transmission error would make a large part of a message
inrecognizable.  It could cause a lot of extra traffic from receiver
back to sender, asking for retransmissions, and additional transmissions
of messages.  The same tradeoff is still valid on today's communication
channels (see Chapter 3).

1.4
The signalman at A had to make sure that not one but two
trains would leave the tunnel, before he admitted the third.
The two trains could reach signalman B in approximately 2 minutes.
At 25 symbols per minute, that would allow the two signalmen
to exchange roughly 50 characters of text.
A could have signaled: "two trains now in tunnel - how many left?"
for a total of 42 characters.
Assuming that B would have answered eventually "one train left,"
that would still leave A puzzling if B had really understood his
message, and if so, where the second train could possibly be.
Considering also that signalman A had been on duty for almost
18 hours when the accident occured, it is not entirely certain
that he could have succesfully resolved the protocol problem.
Note that he still would have had to `invent' part of the protocol
for resolving the problem in real-time.

1.5
Replace the message `train in tunnel' with `increment the number of
trains in the tunnel by one.'  Similarly, replace the message `tunnel
is clear' by `decrement the number of trains in the tunnel by one.'
The message `is tunnel clear' becomes `how many trains are in the
tunnel?' with the possible responses spelled out with numerals 0 to 9.
Either signalman can increment or decrement the number.
The rule of the tunnel is invariantly that the number of trains in
the tunnel is either zero or one, and only one signalman may transmit
at a time. (To resolve conflicts on access to the transmission line,
one could simply give one of the signalmen a fixed priority.)

1.6
A livelock would result.  Assuming that the semaphore operators would
quickly enough recognize the livelock, it is still an open question
what they would (should) do to recover properly from such an occurence.

1.7
One possible scenario, observed by Jon Bentley in real life, is that
two connections are made, and both parties are charged for the call.
Clearly, a dream come true for the telephone companies.

2.1
Service - the simplex transfer of arbitrary messages from a designated
sender to a designated receiver.

Assumptions about the environment - sufficient visibility and small enough
distance to make and accurate detection (and counting) of torches possible
for both sender and receiver.  There seems to be an implicit assumption of
an error-free channel.  There is also the implicit assumption that the
receiver will always be able to keep up with the sender and will not get
out of sync with the symbols that have to be decoded.

Vocabulary - 24 characters from the Greek alphabet, plus two control messages
(the start of text message and its acknowledgement).

Encoding - each character, and each control message, is encoded into two
numbers, both between 1 and 5.
Since there are 26 distinct messages and only 5x5=25 distinct codes, some
ambiguity is unavoidable.

Procedure rules - minimal.  Apparently there was only a single handshake
at the start of the transmission.  All other interactions (end of transmission,
error recovery, flow control) were undefined and would have had to be
improvised in the field.  There is also no resolution of a potential conflict
at the start of transmission (assuming that both parties could decide to
start sending at the same time).

2.2
The procedure rules can include a poll message once per
complete page - interrogating the printer about it's status
(confirming that it is online and confirming that it
is not out of paper - both conditions that can change from
one page to the next).  Note that the procedure rules must
also guarantee that no more than one user can use the printer
at a time.

2.3
Service - establishing a voice connection between two subscribers
of a phone system. (Let's conveniently ignore multi-party connections,
or faxes and modems.)

Assumptions about environment - the phone system is infinitely
available and error-free (sic).

Vocabulary - off-hook, on-hook, dial 0 ... dial 9 (ignore star and sharp).
Dial-tone, busy-tone, ring-tone.  All messages listed here are control
messages - the `data' of the protocol is encoded in the voice message.
(For completeness then we could list `voice' as a separate message in the
vocabulary, without attempting to formalize it's `encoding.')

Encoding - lifting the receiver, lowering the receiver,
pushing one of 10 labeled buttons.

Informal procedure rules -  Go off-hook, if no dial-tone is returned
go on-hook and repeat a random amount of time later.
If there is a dial-tone, push the sequence of buttons that identify the
required destination to the phone system.
If a busy-tone is returned in this interval, go on-hook, wait a random
amount of time, and repeat from the start.
If a ring-tone is returned - the call has been established - wait a
random amount of time, go on-hook.

Note that the random wait period after a busy signal makes it less likely
that a `Lovers' Paradox' can be created (cf. Exercise 1.7).
To be complete, the phone systems behavior should also be listed.
Be warned that the latter is not a trivial exercise....

2.4
The revised version is the famous alternating bit protocol, see Chapter 4.

2.5
The receiver can then determine where a message (should) end by
counting the number of bytes it receives, following the header.
It does not have to scan for a pre-defined message terminator.

2.6
For isntance, a character stuffed protocol always transmits an integral
number of bytes.  A bit stuffed protocol carries slightly less overhead.

2.7
See Bertsekas and Gallager, [1987, p. 78-79].

2.8
More detailed sample assignments for software projects such as
this one are available from the author (email to gerard@research.att.com).

3.1
The code rate is 0.2.  Protection against bursts is limited
to errors affecting maximally 2 out of the 5 bytes.
At 56 Kbits/sec that means bursts smaller than 0.28 msec.

3.3
Does the crc need to be protected by a crc?

3.4
In many cases English sentences are redundant enough that
forward error correction is possible.  Any real conversation,
though, contains many examples of feedback error correction
to resolve ambiguities.
To stick with the example - if the sentence ``the dog run'' is
received, the original version (i.e., one or more dogs) cannot be
determined without feedback error control.

3.5
(a) - the checksum is 6 bits wide.
(b) - the original data is equal to the first n-6 bits of the code word
(6 bits in this case).
(c) - there were no transmission errors other than possible multiples
of the generator polynomial itself.

3.6
The standard example is that of the voyager space craft near
the planet Jupiter receiving a course adjustment from earth.
A retransmission of the message would mean hours delay and invalidate
the original commands.
If the return channel has a high probability of error (e.g., a low
power transmitter on board the spacecraft, sending out a very weak
signal back to earth), the chances that a retransmission request would
reach the earth intact may also be unacceptably low.

3.8
It is impossible to reduce a non-zero error rate to zero.
The probability of error can be brought arbitrarily close to zero,
at the expense of transmission speed, but it cannot reach zero.
The scheme suggested would violate this principle and therefore
should be placed in the same category as perpetuum mobiles and time-travel.

3.9
Fletcher's algorithm can be classified as a systematic block code.

4.2
The alternating bit protocol does not protect against
duplication errors or reordering errors.
Duplication errors persist (duplicate messages do not dissapear
but generate duplicate acks etc, for the duration of the session.)
Reordering can cause erroneous data to be accepted.

4.5
Too short a timeout creates duplicate messages.
The duplicates lower the throughput for the remainder of the session.
Too long a timeout increases idle-time and lowers the
throughput.

4.6
Ignore duplicate acks.

4.8
See Bertsekas and Gallager [1987, pp. 28-29].

4.9
In at least one case (when the receiver is one full window of
messages behind the sender) there is a confusion case where
the receiver cannot tell if an incoming message is a repeat
from W messages back, or a new message.

4.10
Store the data in buffer[n%W] where W is window size.

4.11
Use time-stamps and restrict the maximum life time of
a message.  Note however that time-stamps are just another
flavor of sequence numbers and they would have to be selected
from a sufficiently large window.
For 32 bit sequence numbers one message transmission
per micro-second would recycle the number in 71 minutes.
For 64 bit sequence numbers, the number recycles
at the same transmission speed in 500,000 years.

4.12
Alpha controls the rate of adaption to changes in
network performance.
Beta controls the allowed variance in response time.
(It estimates the load variance of the remote host.)

4.13
Most importantly, all assumptions about the environment,
specifically of the tranmission channel used, are missing completely.

4.14
The message could be received again and cause a duplicate acceptance.

5.1
An assignment is always executable.  The variable b would be set
to the value 0.

5.2
If the receive is executable on the first attempt to execute
the statement, the message would be received, and the condition
would be false (since the `executability' value of the receive is
non-zero).  The statement would block, and would be repeated.
If the receive is (finally) non-executable, the receive fails,
but the condition becomes true and executable.
For all clarity: this is not valid Promela syntax.  In Promela
the rule is that the evaluation of a condition must always be
completely side-effect free.

5.3

/***** Factorial - without channels *****/

int par[16];
int done[16];
int depth;

proctype fact()
{	int r, n, m;

	m = depth;
	n = par[m];
	if
	:: (n <= 1) -> r = 1
	:: (n >= 2) ->
		depth = m + 1;
			par[m+1] = n-1;
			run fact();
			done[m+1];
			r = par[m+1];
		depth = m;
		r = r*n
	fi;
	par[m] = r;
	printf("Value: %d\n", par[m]);
	done[m] = 1
}

init
{	depth = 0;
	par[0] = 12;
	run fact();
	done[0];
	printf("value: %d\n", par[0])
	/* factorial of 12: 12*11*10....*2*1 = 479001600 */
}

/***** Ackermann's function *****/

short  ans[100];
short done[100];	/* synchronization */

proctype ack(short a, b, c)
{
	if
	:: (a == 0) ->
		ans[c] = b+1
	:: (a != 0) ->
		done[c+1] = 0;
		if
		:: (b == 0) ->
			run ack(a-1, 1, c+1)
		:: (b != 0) ->
			run ack(a, b-1, c+1);
			done[c+1];	/* wait */
			done[c+1] = 0;
			run ack(a-1, ans[c+1], c+1)
		fi;
		done[c+1];	/* wait */
		ans[c] = ans[c+1]
	fi;
	done[c] = 1
}
init
{
	run ack(3, 3, 0);
	done[0];	/* wait */
	printf("ack(3,3) = %d\n", ans[0])
}

5.10

Here, as an inspiration, is another sort program, performing
a tree-sort.

/**** Tree sorter ****/

mtype = { data, eof };

proctype seed(chan in)
{	byte num, nr;

	do
	:: (num < 250) -> num = num + 5
	:: (num >   3) -> num = num - 3
	:: in!data,num
	:: (num > 200) -> in!eof,0 -> break
	od
}

init {
	chan in[1] of { byte, byte };
	chan rgt [1] of { byte, byte };
	byte n;

	run seed(in);
	in?data,n;
	run node(n, rgt, in);
	do
	:: rgt?eof,0 -> printf("\n"); break
	:: rgt?data,n -> printf("%d, ", n)
	od
	
}

proctype node(byte hold; chan up, down)
{	chan lft [1] of { byte, byte };
	chan rgt [1] of { byte, byte };
	chan ret [1] of { byte, byte };
	byte n; bit havergt, havelft;

	do
	:: down?data,n ->
		if
		:: (n >  hold) ->
			if
			:: ( havelft) -> lft!data,n
			:: (!havelft) -> havelft=1;
				run node(n, ret, lft)
			fi
		:: (n <= hold) ->
			if
			:: ( havergt) -> rgt!data,n
			:: (!havergt) -> havergt=1;
				run node(n, ret, rgt)
			fi
		fi
	:: down?eof,0 -> break
	od;
	if
	:: (!havergt) -> skip
	:: ( havergt) -> rgt!eof,0;
		do
		:: ret?data,n -> up!data,n
		:: ret?eof,0 -> break
		od
	fi;
	up!data,hold;
	if
	:: (!havelft) -> skip
	:: ( havelft) -> lft!eof,0;
		do
		:: ret?data,n -> up!data,n
		:: ret?eof,0 -> break
		od
	fi;
	up!eof,0
}

5.13
Promela is a validation modeling language, not an implementation language.
Why does a civil engineer not use steel beams in wooden bridge models?

6.1
The assertion can be placed inside the critical section.
The simplest way is as follows (rewritten with some features
from the more recent versions of Spin):

	mtype = { p, v }
	
	chan sema[0] of { mtype };
	byte cnt;
	
	active proctype dijkstra()	/* 1 semaphore process */
	{       do
	        :: sema!p -> sema?v
	        od
	}
	active [3] proctype user()	/* 3 user processes */
	{
		sema?p;
		cnt++;
		assert (cnt == 0 || cnt == 1);  /* critical section */
		cnt--;
		sem!v
		skip   /* non-critical section */
	}

6.2
To check the truth of the invariant
for every reachable state, one can write simply:

	never { do :: assert(invariant) od }

Or to match an invalid behavior by reaching the
end of the never claim, without assertions:

	never
	{	do
		::  (invariant)	/* things are fine, the invariant holds */
		:: !(invariant) -> break	/* invariant fails - match */
		od
	}

Note that semi-colons (or arrows) in never claims match system transitions,
(i.e., each transition in the system must be matched by a move in the
never claim;  the claim does not move independently).

6.5
Using accept labels, for instance:

	proctype A()
	{	do
		:: x = true;
			t = Bturn;
			(y == false || t == Aturn);
			ain = true;
	CS:		skip;	/* the critical section */
			ain = false;
			x = false
		od
	}
	... and simularly for proctype B()

	never {
		do
		:: skip		/* allow arbitrary initial execution */
		:: !A[1]@CS -> goto accept1
		:: !B[2]@CS -> goto accept2
		od;
	accept1:
		do :: !A[1]@CS od	/* process 1 denied access forever */
	accept2:
		do :: !B[2]@CS od	/* process 2 denied access forever */
	}


6.6.a
	never {
		do
		:: skip	/* after an arbitrary number of steps */
		:: p -> break
		od;
	accept:
		do
		:: p	/* can only match if p remains true forever */
		od
	}

6.6.b
For instance:
	never {
		do
		:: assert(q || p)	/* "!q implies p" */
		od
	}

6.6.c
	never {    /* <> (p U q) */
	        do
	        :: skip	/* after an arbitrary number of steps */
	        :: p -> break	/* eventually */
	        od;
	        do
	        :: p		/* p remains true */
	        :: q -> break	/* at least until q becomes true */
	        od
		/* invalid behavior is matched if we get here */
	}

The translation has been automated, and is standard in Spin version 2.7
and later (Spin option -f).

6.7
A research problem -- there are no easy answers.

6.8
	assert(0)
is an immediate violation in both finite or infinite execution sequences,
and is a safety property.

	accept: do :: skip od

is only a violation for an infinite execution sequence, and is a liveness
property (i.e., requires a nested depth-first search for acceptance
cycles). The safety property can be proven more effieciently.
Other than this, the two properties are equivalent;

7.1
Layers 3 to 5 and layer 7.

7.2
At the sender: first checksumming, then byte stuffing and framing.
At the receiver: first unstuffing and de-framing, then checksum
verification.

7.3
Rate control is placed at the layer that handles the units it
refers too (for bit rates, it is the physical layer - for packets
it would be the layer that produces packets, etc.).
Dynamic flow control belongs in the flow control module.

7.13
The one-bit solution will no longer work.

8.1
The dash is used as a don't care symbol - any valid symbol
could replace it without changing the validity of the specification.
The epsilon is a null-element, i.e. it represents the absence
of a symbol (the empty set).

8.7
No, the run and chan operators are defined to be unexecutable
when an (implementation dependent) bound is reached.

9.2
No.

9.5
More states, up to a predefined bound only.  Fewer states, yes.

9.6
No, the IUT could be arbitrarily large.

9.8
It can no longer detect transfer errors.

10.2
The computational complexity will make an interactive
solution impossible for all but the simplest
applications.

11.3
Missing from the program text is that variable j is
initialized to 1 minus the value of i.

12.1
Note that the number of states to be searched by a validator on
such a protocol would multiply by the range of the time count...

13.1
If done right, the changes will be minimal (say 10 to 20 lines
of source).
The memory requirements will very quickly make validations
effectively impossible.