Re: Safety-critical development in Ada and Eiffel

[leew@micrologic.com (Lee Webber)]

On Tue, 19 Aug 1997 02:18:04 GMT, donh@syd.csa.com.au (Don Harrison)
wrote:

>Ken Garlington wrote:
>
>:Don Harrison wrote:

>That *is* how blocking works under SCOOP. The operation of the supplier object 
>contains the precondition, so the supplier determines the (synchronisation) 
>contract.

It's not clear to me that we're getting at the truth here on either
side.  Let me throw in an example and we can go from there.
(Caveat: I'm not a guru, but I have just finished studying chapter 30
of OOSC2 very closely.)

Assume:

   two objects X and Y on which we want to synchronize.
   a client C that wants exclusive access to them.

We will assume that when X and Y were instantiated, they were attached
to 'separate' entities x and y.  This is not necessary for
exclusivity, but most interesting cases happen this way as far as I
can see.

Now to get exclusive access to X and Y, C has to define a feature as
follows:

feature access_xy (separate xx, yy) is
require
   conditions_on_x	-- if these are not met, access_xy blocks
   conditions_on_y
do
     -- at this point, C has exclusive access to X and Y
    operations_on_x
    operations_on_y    -- possibly interleaved
end
     -- at this point, C has given up X and Y

Now my point.  It is likely that operations_on_x and operations_on_y
have preconditions.  However, it is not those preconditions that are
used for blocking, but the preconditions on access_xy.  Hopefully,
the latter subsume the former to the extent they do not ensure them
directly, but it's not enforced.  SCOOP requires you to duplicate the
preconditions if you want to block on them.

So DH's statement above is only true if C is considered the supplier!
Now normally that would be the case -- i.e., a wrapper class is
written that performs the synchronization functions and is then called
by the real client -- but it must be made clear that the class(es) to
be synchronized on do not directly specify the blocking preconditions.


See OOSC2 p. 996.

>
>:In order for the
>:threads that use this object to decide the outcome of their "duel", don't
>:they have to know the internal operation of the object -- an object contract
>:violation?
>
>No, only the object has to know (and how to restore its invariant - ie. how 
>to return to a consistent state).

On the other hand, DH is correct here. The exception occurs in the
object being contended for (the one that is executing a routine at the
time -- there can be at most one such).  (Question for guru'ier
people: what happens if the challenge occurs when access_to_xy is
calling a non-separate object?  Who gets the exception?)