Re: D.10

[Matthew Heaney <matthew_heaney@acm.org>]

Robert Dewar <robert_dewar@my-dejanews.com> writes:

> In article <m3lnfxtan3.fsf@mheaney.ni.net>,
>   Matthew Heaney <matthew_heaney@acm.org> wrote:
> > The RM is ambiguous.  It doesn't say specifically that
> > the suspension object can be shared this way (ie that
> > Suspend_Until_True is atomic wrt other calls to
> > Suspend_Until_True), but it doesn't say it can't be.
> 
> I must say I don't see any ambiguity in the RM here, but
> I have trouble with your question because the terminology
> is vague ("A is atomic wrt B" does not have a clear meaning
> in this context).


I was trying to phrase my question using the same terms as the RM, but
perhaps I goofed.

RM95 D.10 (7) reads "The operations Set_True and Set_False are atomic
with respect to each other and with respect to Suspend_Until_True..."

My question is, why doesn't the RM also say "The operation
Suspend_Until_True is atomic with respect to Suspend_Until_True"?


> > I would like to know the specific intent of the language
> > designers, and whether or not the algorithm in B&W is in
> > fact legal.
> 
> You are using legal again in some peculiar sense (in Ada
> it means that something satisfies static semantic and
> syntax requirements).

Agreed; I used the term "legal" incorrectly.

 
> I think you will get a clearer answer to your question if
> you produce a small example, and ask a question about it
> at the proper level of semantic description. 

I included an example in my original post.

Here is the text from Concurrency In Ada (by Burns and Wellings),
section 12.3.1:

(start of excerpt)
Using a Suspension_Object, it is possible to program mutual exclusion
between two tasks by simply encapsulating their critical sections with
the following:

   Mutex : Suspension_Object;

   ...

   Set_True (Mutex);

   ...

   Suspend_Until_True (Mutex);
     -- critical section
   Set_True (Mutex);

Suspension objects can also be used inside protected objects to
implement condition synchronization. (end of excerpt)


My question is, Is this is a correct program, or isn't it?

Does this program have a defined meaning, or doesn't it?

Is the statement "it is possible to program mutual exclusion between two
tasks by simply encapsulating their critical sections with the
following..." true, or isn't it?



> If I write X, then is Y true, where Y is stated in terms with which we
> are familiar, preferably those in the RM!

The phrase "atomic with respect to" came out of the RM, which I why I
used it.  Incorrectly, I guess.