Subject: TR: TR: Timer active expression
From: VINCENT Daniel FTRD/DTL/LAN (daniel.vincent#rd.francetelecom.fr)
Date: Thu Apr 26 2001 - 12:14:17 GMT
-----Message d'origine-----
De : Susanne Graf [mailto:Susanne.Graf#imag.fr]
Envoyé : jeudi 26 avril 2001 14:14
À : VINCENT Daniel FTRD/DTL/LAN
Cc : 'laurent.mounier#imag.fr'; 'marius.bozga#imag.fr';
'iulian.ober#telelogic.com'; rickreed#tseng.co.uk
Objet : Re: TR: Timer active expression
Dear Rick,
There are two questions. I will try to respond and will add a third one:
1. A (less interesting one) about who said what, but let's answer it too: I
am not aware
of the fact that we (the Interval project) said that there is a change in
the semantics of
the active predicate in SDL. The automaton representing a timer in the paper
submitted to
the SDL forum allows a timer to be active and expired.
2. A second question about what has changed and what has not changed about
timers between
SDL'96 and SDL 2000?
a) the active predicate has not changed. On page 36 (of my version) of the
ASM semantices
the activity of a timer is very clearly defined by:
Active(Pid,t) = (t.arrival > now) or (t in Pid.inport.queue)
which is as in SDL'96
b) what HAS changed is the expiration of a timer: a timer "expires" (meaning
that a
timeout signal is put into the queue of the owner process) "exactly" at
expiration time";
that means that the (implicit) timeout expiration has become an "eager"
transition see our
proposal), which we requested unnecessarily as a change in the above
mentioned paper.
3. A third question arises about what should be the right definitions:
a) should a timer become inactive as soon it has expired?
to some extent it is a matter of taste, but it is dangerous to make such
subtle changes
(which would by the way complicate the reset operation, relying on the
active predicate,
when a timer has expired but the signal hasn't been consumed);
We propose to add a (very useful) function "time-to-expiration" which
subsumes the "has
expired predicate" you are prosing, as it can be used to know if the timer
has already
expired or not: time-to-expiration<=0 and active meaning that the
timeout-signal is still
in the queue waiting to be consumed.
Under some assumption the "time-to-expiry" function can be coded in today
SDL, by
remebering "now"" "right after setting the timer" (supposing however that
these two
actions can be made "atomic"), but it is much cleaner to have a well-defined
abstract data
type timer with abstract operations set, reset, active, time-to-expiration.
In this
context "active and expired" can be defined as a derived, rather than as a
primitive
predicate.
b) should the timeout expiration be eager?
definitively yes. If one wants to be able to assume some flexibility in the
expiration of
a timer, it is better to allow "flexible timeouts" where one can make
assumption about an
interval in which the timer will expire. Moreover, even with an eager
expiration, there is
still a lot of flexibility, as there is by default no constraint on the time
that passes
between expiration and consumption; the control of this time using the
attributes eager,
delayable or lazy is the purpose of our flexible definition of time
progress.
Susanne
VINCENT Daniel FTRD/DTL/LAN wrote:
> -----Message d'origine-----
> De: Rick Reed TSE [mailto:rickreed#tseng.co.uk]
> Date: vendredi 20 avril 2001 22:57
> À: meeting
> Objet: Timer active expression
>
> The work of under Q.7/10 and the Interval project has stated (in papers to
> the SDL Forum) that the semantics of the timer active expression has
changed
> between a previous version of SDL and SDL-2000.
>
> I thought that this was the case myself and that in SDL-96 a timer was
> inactive if the timer had expired and a signal had been posted in the
input
> queue. However, I checked and found that this was incorrect and the same
> text for "timer" and "active" appears in the main body of Z.100 in the
Blue
> Book Z.100 (SDL-88), Z.100(03/93) SDL-92, and Z.100(11/99) SDL-2000.
>
> I then checked the formal definition for SDL-92 and this has the same
> semantics: a timer remains active until the corresponding timer signal is
> consumed. I have not checked the current formal definition, but I assume
it
> also follows the Z.100 definition (which has not changed since 1988).
>
> However, there seems to be a (common?) understanding that there was at one
> time a Z.100 definition that a timer was active until it "expired" and the
> signal was put into the input queue - at which time it becomes "inactive".
> The only document in which I can find this interpretation is in
"Engineering
> Real Time Systems" by Rolv Braek and Oystein Haugen. It is correct in the
> Sarma/Hogrefe books and in the Olsen et al. book.
>
> Though the Braek/Haugen meaning is not correct according to Z.100 (or SDT
-
> I have not checked GEODE or Cinderella), it is easy to see why there
should
> be a misunderstanding. The current active expression is not particularly
> useful as the value does not change unless the signal has been consumed,
> whereas an expression that is evaluated as Braek/Haugen suggest (let's
call
> this "unexpired") would be more accurate than "active". This would make it
> easy to do something which otherwise requires the value used in the "set"
> statement to be stored. If the timer T was set with:
>
> SET(time_t, T);
>
> then "unexpired(T)" would have the value of the Boolean expression:
>
> NOW < time_t
>
> assuming that the value of "time_t" had not been changed. As this
expression
> can be written in SDL in any case, such an active expression does not
> require any new underlying semantics in SDL.
>
> By examining now in enabling conditions or continuous signals either
> explicitly or by the application of "unexpired" - it is possible to leave
a
> state as soon as a timer expires: it is not necessary to wait for the
signal
> to be consumed.
>
> The possible states of a timer are:
>
> - inactive: timer never set or set and the signal consumed;
>
> - active unexpired: timer set but time not reached and no signal
generated;
>
> - active expired: timer expired, signal in input queue.
>
> I suggest therefore to add a additional active operator "expired" to SDL.
>
> --
> Rick Reed - rickreed#tseng.co.uk
> Tel:+44 1455 55 96 55 Fax:+44 1455 55 96 58 Mob.:+44 7970 50 96 50
-- ------------------------------------------------------------------------ Susanne Graf | tel : (+33) (0)4 76 63 48 52 VERIMAG | fax : (+33) (0)4 76 63 48 50 2, avenue de la Vignate | http://www-verimag.imag.fr/~graf/ F - 38610 Gieres | e-mail: Susanne.Graf#imag.fr ------------------------------------------------------------------------
This archive was generated by hypermail 2a23 : Mon May 05 2008 - 20:30:55 GMT