comp.lang.ada
 help / color / mirror / Atom feed
* Help with Atomic_Components and whole array assignment
@ 2001-01-22 11:22 r_c_chapman
  2001-01-22 12:51 ` Stuart Palin
  2001-01-22 16:21 ` Robert Dewar
  0 siblings, 2 replies; 31+ messages in thread
From: r_c_chapman @ 2001-01-22 11:22 UTC (permalink / raw)


Having a slight confusion over the use of array aggregate assignments
with Atomic_Components.

We have a device which _has_ to be accessed use byte-wide load
and store instructions only (it's an autostore NOVRAM...), so we
have an array of bytes declared, thus:

  type Byte is range 0 .. 255;
  for Byte'Size use 8;
  for Byte'Alignment use 1;
  type Index is range 0 .. 4; -- for argument's sake!
  type Byte_Array is array (Index) of Byte;
  pragma Volatile (Byte_Array);
  pragma Atomic_Components (Byte_Array);

  A : Byte_Array;
  for A'Address use ...

all fine so far.  When we initialise this array, thus:

  A := Byte_Array'(others => 0);

compiler A generates 1 Word-sized store and 1 Byte-sized store.
(Target is PowerPC by the way.)
Compiler B (or should that be "G" :-) ) generates similar code on IA32.

Can anyone confirm this is indeed acceptable behaviour?

PS...Yes I know the Byte should probably be modular, but this is SPARK,
and we haven't got them implemented (yet... :-) )
 Thanks,
  Rod




Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 11:22 Help with Atomic_Components and whole array assignment r_c_chapman
@ 2001-01-22 12:51 ` Stuart Palin
  2001-01-22 14:16   ` mark_lundquist
  2001-01-22 16:21 ` Robert Dewar
  1 sibling, 1 reply; 31+ messages in thread
From: Stuart Palin @ 2001-01-22 12:51 UTC (permalink / raw)


r_c_chapman@my-deja.com wrote:

Hi Rod!

> Having a slight confusion over the use of array aggregate assignments
> with Atomic_Components.
> 
> We have a device which _has_ to be accessed use byte-wide load
> and store instructions only (it's an autostore NOVRAM...), so we
> have an array of bytes declared, thus:
> 
>   type Byte is range 0 .. 255;
>   for Byte'Size use 8;
>   for Byte'Alignment use 1;
>   type Index is range 0 .. 4; -- for argument's sake!
>   type Byte_Array is array (Index) of Byte;
>   pragma Volatile (Byte_Array);
>   pragma Atomic_Components (Byte_Array);
> 
>   A : Byte_Array;
>   for A'Address use ...
> 
> all fine so far.  When we initialise this array, thus:
> 
>   A := Byte_Array'(others => 0);
> 
> compiler A generates 1 Word-sized store and 1 Byte-sized store.
> (Target is PowerPC by the way.)
> Compiler B (or should that be "G" :-) ) generates similar code on IA32.
> 
> Can anyone confirm this is indeed acceptable behaviour?

Yes it is (from a language specification point of view) - a deja news
search should throw up several discussions on the topic.

The pragma volatile has been observed, because the operation is on
object (not some locally cached version of it).

The pragma atomic_components has been observed because each component is
indivisibly updated (within the bounds of an architecture assumption
that the word write is not divisible).

--# hide;
Ultimate answer seems to be package MACHINE_CODE is the way to go if the
there is a specific way memory has to be accessed.

  The "portability" argument is that since this access mechanism is
specific to your
  architecture it should be re-examined if you change the hardware
anyway, so using
  MACHINE_CODE conveniently highlights the areas of software you should
look at.

Personally; this seems to be a recurrent embedded systems problem (that
is either
agonized over or [in]conveniently swept under the carpet).  It would be
nice if it were addressed at the next language revision.


--
Stuart Palin
Principal Software Engineer
BAE SYSTEMS Avionics Ltd, Rochester
G-NET 791 3364    mailto:stuart.palin@baesystems.com



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 12:51 ` Stuart Palin
@ 2001-01-22 14:16   ` mark_lundquist
  2001-01-22 16:09     ` Pat Rogers
  2001-01-22 16:29     ` Robert Dewar
  0 siblings, 2 replies; 31+ messages in thread
From: mark_lundquist @ 2001-01-22 14:16 UTC (permalink / raw)


In article <3A6C2CDD.67FD79DC@baesystems.com>,
  Stuart Palin <stuart.palin@baesystems.com> wrote:
> r_c_chapman@my-deja.com wrote:
>
> > [...]
> > all fine so far.  When we initialise this array, thus:
> >
> >   A := Byte_Array'(others => 0);
> >
> > compiler A generates 1 Word-sized store and 1 Byte-sized store.
> > (Target is PowerPC by the way.)
> > Compiler B (or should that be "G" :-) ) generates similar code on
IA32.
> >
> > Can anyone confirm this is indeed acceptable behaviour?
>
> Yes it is (from a language specification point of view) - a deja news
> search should throw up several discussions on the topic.
>
> The pragma volatile has been observed, because the operation is on
> object (not some locally cached version of it).
>
> The pragma atomic_components has been observed because each component
is
> indivisibly updated (within the bounds of an architecture assumption
> that the word write is not divisible).
>
> --# hide;
> Ultimate answer seems to be package MACHINE_CODE is the way to go if
the
> there is a specific way memory has to be accessed.

Or, just access the array one element at a time (no whole array or
slices).  If instead of

   A := Byte_Array'(others => 0);

you write

   for I in A'range loop
      A (I) := 0;
   end loop;

you'll get 1-byte writes, guaranteed.  It's hard to imagine a compiler
wanting to generate anything but simply a 1-byte write for each
element, but if it did want to, RM C.6(20) would not allow it
(violation of sharing properties of the other components).

> [...]
> Personally; this seems to be a recurrent embedded systems problem
(that
> is either
> agonized over or [in]conveniently swept under the carpet).  It would
be
> nice if it were addressed at the next language revision.

I agree, it would be very nice not to have to work around this.

Here's another embedded systems issue I'd like to see taken up: I'd
like to see bit order fixed, i.e. the ability to write endian-
independent record representation clauses.

---------------
Mark Lundquist
Rational Software



Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 14:16   ` mark_lundquist
@ 2001-01-22 16:09     ` Pat Rogers
  2001-01-22 16:29     ` Robert Dewar
  1 sibling, 0 replies; 31+ messages in thread
From: Pat Rogers @ 2001-01-22 16:09 UTC (permalink / raw)


<mark_lundquist@my-deja.com> wrote in message
news:94hfaq$h3n$1@nnrp1.deja.com...

<snip>

> Here's another embedded systems issue I'd like to see taken up: I'd
> like to see bit order fixed, i.e. the ability to write endian-
> independent record representation clauses.

There's an AI for it; I forget which one off the top of my head.  At any
rate we can now compile the following (i.e., Norm Cohen's nice example),
because Default_Bit_Order is now static:


with System;
use  System;

package Endianess is

  Byte_MSB        : constant := 0 + (Boolean'Pos(Default_Bit_Order =
Low_Order_First) * 7);
  Halfword_MSB    : constant := 0 + (Boolean'Pos(Default_Bit_Order =
Low_Order_First) * 15);
  Word_MSB        : constant := 0 + (Boolean'Pos(Default_Bit_Order =
Low_Order_First) * 31);
  DoubleWord_MSB  : constant := 0 + (Boolean'Pos(Default_Bit_Order =
Low_Order_First) * 63);

  NextBit         : constant := 1 - (2 * Boolean'Pos(Default_Bit_Order =
Low_Order_First));

end Endianess;







^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 11:22 Help with Atomic_Components and whole array assignment r_c_chapman
  2001-01-22 12:51 ` Stuart Palin
@ 2001-01-22 16:21 ` Robert Dewar
  2001-01-22 16:39   ` r_c_chapman
  1 sibling, 1 reply; 31+ messages in thread
From: Robert Dewar @ 2001-01-22 16:21 UTC (permalink / raw)


In article <94h55t$9a1$1@nnrp1.deja.com>,
  r_c_chapman@my-deja.com wrote:
> Can anyone confirm this is indeed acceptable behaviour?

Yes, of course this is acceptable behavior, can you point to
anything in the RM that would even HINT that it is not?

No, you can't (to save you the trouble :-)

There is NO legitimate way to ensure that the compiler
generates specific instructions other than using machine
language inserts, since the compiler is always free to
substitute different instructions which have the same effect
*as defined by the semantics in the RM* and the RM knows
nothing about byte stores etc.

pragma Atomic merely says that two tasks cannot intefere with
one another, and that the semantics is as though writes are
done for every write. But there is nothing to stop the compiler
from combining four writes into a word write (in fact this is
a very nice optimization -- all compilers should do it :-)



Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 14:16   ` mark_lundquist
  2001-01-22 16:09     ` Pat Rogers
@ 2001-01-22 16:29     ` Robert Dewar
  2001-01-22 19:52       ` Mark Lundquist
  2001-01-30 15:54       ` Tucker Taft
  1 sibling, 2 replies; 31+ messages in thread
From: Robert Dewar @ 2001-01-22 16:29 UTC (permalink / raw)


In article <94hfaq$h3n$1@nnrp1.deja.com>,
  mark_lundquist@my-deja.com wrote:
>    for I in A'range loop
>       A (I) := 0;
>    end loop;
>
> you'll get 1-byte writes, guaranteed.

That is not correct.

> It's hard to imagine a compiler wanting to generate anything
> but simply a 1-byte write for each element

It's not hard at all. Converting this loop to a more efficient
form is a quite reasonable optimization (the Microsoft C
compiler does this for example, since it is a big win on
earlier implementations of the ia32 architecture.

> but if it did want to, RM C.6(20) would not allow it
> (violation of sharing properties of the other components).

No, it is a perfectly legitimate optimization, and does not
violate the quoted section, which talks about generating extra
stores, not about combining store operations.

> > Personally; this seems to be a recurrent embedded systems
> > proble (that
> > is either agonized over or [in]conveniently swept under the
> > carpet).

No, it is not swept under the carpet, it is clear from the
RM (as has been explained in many threads on the subject), that
if your application requires specific sequences of instructions
to be generated, then the ONLY legitimate way of doing this is
with machine language insertions. To think otherwise is a
recipe for mysterious and ill-documented implementation
dependencies (the GNU/Linux kernel suffered from these problems
early on).

> > It would be nice if it were addressed at the next language
> > revision.

At most addressing this would involve adding a note that points
out that the only way to ensure specific sequences of machine
instructions being generated is to write the specific sequence
that you want as a machine language insert.

I suppose we could add

   pragma Full_Memory_Access (type);

but at most we could only have implementation advice that this
meant that every read or write must be done with a single
instruction that affects those bits and nothing else (this
basically would be a stronger and weaker condition than atomic,
stronger, because it forbids, e.g., combing writes, or reading
more than is needed, weaker, because at the bus level, there is
no requirement for invidisibility.

But we could only make this implementation advice, since there
is really no clear way at the semantic level to talk about
generated instructions (consider for example that such a rule
is completely meaningless when you are running in a JVM
environment).


>
> I agree, it would be very nice not to have to work around
this.
>
> Here's another embedded systems issue I'd like to see taken
up: I'd
> like to see bit order fixed, i.e. the ability to write
endian-
> independent record representation clauses.
>
> ---------------
> Mark Lundquist
> Rational Software
>
> Sent via Deja.com
> http://www.deja.com/
>


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 16:21 ` Robert Dewar
@ 2001-01-22 16:39   ` r_c_chapman
  2001-01-30 15:57     ` Tucker Taft
  0 siblings, 1 reply; 31+ messages in thread
From: r_c_chapman @ 2001-01-22 16:39 UTC (permalink / raw)


In article <94hml1$o64$1@nnrp1.deja.com>,
  Robert Dewar <robert_dewar@my-deja.com> wrote:
> pragma Atomic merely says that two tasks cannot intefere with
> one another...

Ah..got it..of course, from the point of view of another Ada task,
the writes can be combined.  This means I've mis-understood Atomic
for at least the last 4 years... :-(

Package Machine_Code here we come...
 - Rod


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 16:29     ` Robert Dewar
@ 2001-01-22 19:52       ` Mark Lundquist
  2001-01-30 15:54       ` Tucker Taft
  1 sibling, 0 replies; 31+ messages in thread
From: Mark Lundquist @ 2001-01-22 19:52 UTC (permalink / raw)



Robert Dewar <robert_dewar@my-deja.com> wrote in message
news:94hn5p$on4$1@nnrp1.deja.com...
> In article <94hfaq$h3n$1@nnrp1.deja.com>,
>   mark_lundquist@my-deja.com wrote:
> >    for I in A'range loop
> >       A (I) := 0;
> >    end loop;
> >
> > you'll get 1-byte writes, guaranteed.
>
> That is not correct.
>
> > It's hard to imagine a compiler wanting to generate anything
> > but simply a 1-byte write for each element
>
> It's not hard at all. Converting this loop to a more efficient
> form is a quite reasonable optimization (the Microsoft C
> compiler does this for example, since it is a big win on
> earlier implementations of the ia32 architecture.

Ah, I didn't mean for the loop... but unfortunately, it's the loop that's
relevant :-(.  What I just meant for the assignment statement itself.  That
is, you'd expect a byte-addressable machine to generate a byte-wide access
for an assignment of a byte-wide type, not, for instance, a 32-bit read,
mask, logical or, then 32-bit write -- and I was saying that although you
can't otherwise assume that behavior, the atomicity rules would enforce it
(which you shot down in flames below :-).  But anyway, I missed the forest
for the trees at that point -- of course the compiler *can* say, "oh, he's
initializing this array... I know a better way".

Now then... if you pull out the byte write into its own procedure, then as
long as you know the compiler doesn't do any automatic inlining before it
tries to optimize the loop(and it doesn't do global optimization)...

Hah!  I just said that to get to you... and it worked, didn't it?  Eh?...
:-) :-)

Yeah, I know, if I have to say "as long as you know the compiler X" then
it's wrong.

Reminds me of the old Benny Hill episode... "Never ASSUME!  It makes an ASS
out of U and ME!"

>
> > but if it did want to, RM C.6(20) would not allow it
> > (violation of sharing properties of the other components).
>
> No, it is a perfectly legitimate optimization, and does not
> violate the quoted section, which talks about generating extra
> stores, not about combining store operations.

Phooey... you're right.

>
> > > Personally; this seems to be a recurrent embedded systems
> > > proble (that
> > > is either agonized over or [in]conveniently swept under the
> > > carpet).
>

[note,  someone else said this -- it was just part of the post I was
replying to...]

> No, it is not swept under the carpet, it is clear from the
> RM (as has been explained in many threads on the subject), that
> if your application requires specific sequences of instructions
> to be generated, then the ONLY legitimate way of doing this is
> with machine language insertions. To think otherwise is a
> recipe for mysterious and ill-documented implementation
> dependencies (the GNU/Linux kernel suffered from these problems
> early on).
>
> > > It would be nice if it were addressed at the next language
> > > revision.
>
> [...]
> I suppose we could add
>
>    pragma Full_Memory_Access (type);
>
> but at most we could only have implementation advice that this
> meant that every read or write must be done with a single
> instruction that affects those bits and nothing else (this
> basically would be a stronger and weaker condition than atomic,
> stronger, because it forbids, e.g., combing writes, or reading
> more than is needed, weaker, because at the bus level, there is
> no requirement for invidisibility.

Well, yeah, I think that is the idea! :-)

>
> But we could only make this implementation advice, since there
> is really no clear way at the semantic level to talk about
> generated instructions

Don't volatility/atomicity kind of suffer from this in general?  And why
couldn't you go stronger than implementation advice, and say the
implementation is required to do X on platforms where X is meaningful?

>  (consider for example that such a rule
> is completely meaningless when you are running in a JVM
> environment).

Sorry, I don't really know anything about the JVM so this example doesn't
mean anything to me...  So if you feel like elaborating, I'm interested,
otherwise no need...

Best,
-- mark







^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 16:29     ` Robert Dewar
  2001-01-22 19:52       ` Mark Lundquist
@ 2001-01-30 15:54       ` Tucker Taft
  2001-01-30 18:20         ` Robert Dewar
  1 sibling, 1 reply; 31+ messages in thread
From: Tucker Taft @ 2001-01-30 15:54 UTC (permalink / raw)


Robert Dewar wrote:
> 
> In article <94hfaq$h3n$1@nnrp1.deja.com>,
>   mark_lundquist@my-deja.com wrote:
> >    for I in A'range loop
> >       A (I) := 0;
> >    end loop;
> >
> > you'll get 1-byte writes, guaranteed.
> 
> That is not correct.

It seems correct if pragma atomic_components applies to A,
since in that case, each component of A is an atomic object,
and each update to an atomic object has a separate external
effect, per C.6(20).

> > It's hard to imagine a compiler wanting to generate anything
> > but simply a 1-byte write for each element
> 
> It's not hard at all. Converting this loop to a more efficient
> form is a quite reasonable optimization (the Microsoft C
> compiler does this for example, since it is a big win on
> earlier implementations of the ia32 architecture.

True, but such a transformation is not permitted if Atomic_Components
applies.

> > but if it did want to, RM C.6(20) would not allow it
> > (violation of sharing properties of the other components).
> 
> No, it is a perfectly legitimate optimization, and does not
> violate the quoted section, which talks about generating extra
> stores, not about combining store operations.

I don't agree with Robert's reading of this.  It seems very clear
that you cannot combine multiple updates of separate atomic
objects into a single write.  One of the whole points of atomic
is to make each write separate and indivisible.  It was designed
specifically to address issues relating to "active" memory, where
breaking the write down into multiple writes, or combining
multiple writes into a single write, would confuse the device.

> ...
> No, it is not swept under the carpet, it is clear from the
> RM (as has been explained in many threads on the subject), that
> if your application requires specific sequences of instructions
> to be generated, then the ONLY legitimate way of doing this is
> with machine language insertions. To think otherwise is a
> recipe for mysterious and ill-documented implementation
> dependencies (the GNU/Linux kernel suffered from these problems
> early on).

Well, I don't agree completely with these "many comp.lang.ada threads."
Atomic is designed to provide additional control over what
code the compiler generates.  It doesn't specify exactly what
instructions will be used, but it does require that each read/update
be its own indivisible operation, however that is accomplished.
In general, that means each read/update is a separate instruction.
Which particular instruction is not specified, though of course
in most cases it will be a load or a store.  I don't agree with
the advice of slipping into machine code to accomplish all of these
kinds of things, if atomic can do the job.  

I would agree that with the original code, which used an aggregate
assignment, there is no requirement to perform that as separate
byte assignments.  However, if the code is written as a sequence
(or a loop) of separate assignments, and the objects are atomic,
it is a bug (in my view) if the compiler combines these assignments 
into a single assignment.  Similarly, reordering such assignments
would be a bug, since it would change the external effect of the
program in an impermissible way.

> > ---------------
> > Mark Lundquist
> > Rational Software

-- 
-Tucker Taft   stt@avercom.net   http://www.averstar.com/~stt/
Chief Technology Officer, AverCom, Inc. (A Titan Company) Burlington, MA  USA
(AverCom was formed 1/1/01 from the Commercial Division of AverStar)
(http://www.averstar.com/services/ebusiness_applications.html)



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-22 16:39   ` r_c_chapman
@ 2001-01-30 15:57     ` Tucker Taft
  2001-01-30 18:26       ` Robert Dewar
  2001-01-31 10:09       ` Rod Chapman
  0 siblings, 2 replies; 31+ messages in thread
From: Tucker Taft @ 2001-01-30 15:57 UTC (permalink / raw)


r_c_chapman@my-deja.com wrote:
> 
> In article <94hml1$o64$1@nnrp1.deja.com>,
>   Robert Dewar <robert_dewar@my-deja.com> wrote:
> > pragma Atomic merely says that two tasks cannot intefere with
> > one another...
> 
> Ah..got it..of course, from the point of view of another Ada task,
> the writes can be combined.  This means I've mis-understood Atomic
> for at least the last 4 years... :-(

I don't agree with Robert on this.  Have you tried writing it
as a loop rather than an aggregate assignment.  I suspect that
all Ada compilers would use separate assignments, including GNAT.
In any case, I believe they should use separate assignments.

> 
> Package Machine_Code here we come...

This is not necessarily the right conclusion in my view.
Most device drivers are written without dropping into machine
code these days.  Ada of all languages should not change that.

>  - Rod

-- 
-Tucker Taft   stt@avercom.net   http://www.averstar.com/~stt/
Chief Technology Officer, AverCom, Inc. (A Titan Company) Burlington, MA  USA
(AverCom was formed 1/1/01 from the Commercial Division of AverStar)
(http://www.averstar.com/services/ebusiness_applications.html)



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 15:54       ` Tucker Taft
@ 2001-01-30 18:20         ` Robert Dewar
  2001-01-31  5:08           ` DuckE
  0 siblings, 1 reply; 31+ messages in thread
From: Robert Dewar @ 2001-01-30 18:20 UTC (permalink / raw)


In article <3A76E3B9.BD806841@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:
> I don't agree with Robert's reading of this.  It seems very
> clear that you cannot combine multiple updates of separate
> atomic objects into a single write.

I disagree with Tuck. Please provide a test program where it
would be theoretically possible to determine that combining
writes had a semantic effect.

> One of the whole points of atomic
> is to make each write separate and indivisible.

Indivisible, yes. Separate no. You may have intended to say
this, and you may have thought it, but I don't see that the
RM says, or even implies this.

> It was designed specifically to address issues relating to
> "active" memory, where breaking the write down into multiple
> writes, or combining multiple writes into a single write,
> would confuse the device.

This is a total surprise to me, and certainly there is nothing
in the RM that would reveal this hidden design intent. For
example, an implementation which locks the bus and then does
a whole sequence of writes for an atomic variable, and then
unlocks the bus, CLEARLY meets the semantics of the RM.

This is a case of the designer reading more into what's there
than what was written. My own view is that it is almost
impossible to achieve the design goal that Tuck quotes, except
on an implementation advice basis. I had no idea that the
design team had this view of pragma Atomic (because nothing
they ever wrote in the RM implied this viewpoint).

Note that the detailed list in AARM C.6(20) of disallowed
transformations has no hint at all of the "separate" part of
Tuck's claim, and conspicuously does not list combining writes
as an improper transformation.

Tuck, having something in your mind is not good enough if you
do not write it down :-)

> In general, that means each read/update is a separate
> instruction.

No, there is absolutely NO implication of this

> Which particular instruction is not specified, though of
> course in most cases it will be a load or a store.

> I don't agree with the advice of slipping into machine code
> to accomplish all of these kinds of things, if atomic can do
> the job.

But it can't! In particular, suppose you have four atomic
byte variables next to one another. It is perfectly fine to
do a word load followed by a shift and mask, but likely this
would play havoc with memory mapped I/O.


> I would agree that with the original code, which used an
> aggregate assignment, there is no requirement to perform that
> as separate byte assignments.  However, if the code is
> written as a sequence (or a loop) of separate assignments,
> and the objects are atomic, it is a bug (in my view) if the
> compiler combines these assignments  into a single
> assignment.

You repeat this, but the RM does not support this view point.

> Similarly, reordering such assignments
> would be a bug, since it would change the external effect of
> the program in an impermissible way.

No, this is not similar at all. Everyone agrees that reordering
is not permitted, because you can see external effects not
corresponding to the canonical order. The RM is quite explicit
in this case, and indeed AARM C.6(20.c) gives an explicit
example of this not being allowed, but the AARM does not list
combining.

Too bad you did not list the combining case in the AARM Tuck,
then we would at least have known what was in your mind, and
could have discussed the point that the RM wording does not
happen to capture this intent (and as I say, I think it would
be almost impossible to capture this intent).

For all the examples in AARM C.6(20), you can devise simple
pure Ada tests that can conceptually malfunction because of
a task switch at a bad point (it may be tricky to actually
do the run that fails, since it depends on very precise
timing). But for the combining case, you cannot devise a
pure Ada test that even conceptually fails.

The idea that pragma Atomic solves this problem is an old
confusion, going way back to Ada 83 days, I thought we had
put that to rest in Ada 95, because we never discussed the
idea that Atomic *did* solve this problem. I am somewhat
amazed to see the claim that it was addressed :-)



Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 15:57     ` Tucker Taft
@ 2001-01-30 18:26       ` Robert Dewar
  2001-01-30 21:30         ` Simon Wright
  2001-02-06  0:32         ` Richard Kenner
  2001-01-31 10:09       ` Rod Chapman
  1 sibling, 2 replies; 31+ messages in thread
From: Robert Dewar @ 2001-01-30 18:26 UTC (permalink / raw)


In article <3A76E455.AABF2490@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:
> I don't agree with Robert on this.  Have you tried writing it
> as a loop rather than an aggregate assignment.  I suspect
> that all Ada compilers would use separate assignments,
> including GNAT.

True enough

> In any case, I believe they should use separate assignments.

Yes, this article of faith has been discussed in a previous
message but I see nothing in the RM to justify this statement.

> > Package Machine_Code here we come...
>
> This is not necessarily the right conclusion in my view.
> Most device drivers are written without dropping into machine
> code these days.  Ada of all languages should not change
> that.

If specific instructions are required (as is often the case
with device drivers), then there is nothing in the C, or
Ada (or any other) standard that guarantees that a particular
instruction will be generated. If you are counting on this,
and it just happens that your compiler let's you get away
with it, you are writing implementation dependendent bogus
code, and I think this should be avoided.

The GNU/Linux kernel had endless problems from assumptions
of this kind, and finally they have all been replaced by
machine language insertions, to avoid the problems. What
happened in this case is that new improved and correct gcc
compilers blew the kernel out of the water by breaking these
undocumented assumptions.

The same can happen to you if you follow Tuck's advice. Note
that even from what Tuck claims, he specifically notes that
nothing in the RM requires a particular instruction to be
used. So for example, if you have a word variable, and
you read it and copy it somewhere else, there is nothing
to stop the compiler from using a floating-point instruction
for the purpose, even if what you want and need is an integer
load.



Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 18:26       ` Robert Dewar
@ 2001-01-30 21:30         ` Simon Wright
  2001-02-01  6:11           ` Robert Dewar
  2001-02-06  0:32         ` Richard Kenner
  1 sibling, 1 reply; 31+ messages in thread
From: Simon Wright @ 2001-01-30 21:30 UTC (permalink / raw)


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

> In article <3A76E455.AABF2490@averstar.com>,
>   Tucker Taft <stt@averstar.com> wrote:
> > I don't agree with Robert on this.  Have you tried writing it
> > as a loop rather than an aggregate assignment.  I suspect
> > that all Ada compilers would use separate assignments,
> > including GNAT.
> 
> True enough
> 
> > In any case, I believe they should use separate assignments.
> 
> Yes, this article of faith has been discussed in a previous
> message but I see nothing in the RM to justify this statement.
> 
> > > Package Machine_Code here we come...
> >
> > This is not necessarily the right conclusion in my view.
> > Most device drivers are written without dropping into machine
> > code these days.  Ada of all languages should not change
> > that.
> 
> If specific instructions are required (as is often the case
> with device drivers), then there is nothing in the C, or
> Ada (or any other) standard that guarantees that a particular
> instruction will be generated. If you are counting on this,
> and it just happens that your compiler let's you get away
> with it, you are writing implementation dependendent bogus
> code, and I think this should be avoided.

If it were another compiler provider, I would be tempted to read this
whole discussion as "it would cost us a bundle to implement this, so
let's dig our heels in". I don't for one moment believe that that's
the case here.

If the intent is to ensure that the RM be modified (advised) so that
Ada will be at least as useful as C for writing device drivers, great!

I'm very very far from the expert on memory-mapped device management
(I know only one, a VME device), but it seems hard to conceive of
devices where you *must* do other than read or write a byte/a short/a
word at once??? can't we come up with an interpretation that does at
least that? then someone who needs to do (say) bit accesses can be
sure they're out on a limb ..

-- 
Simon Wright                       Work Email: simon.j.wright@amsjv.com
Alenia Marconi Systems                        Voice: +44(0)23-9270-1778
Integrated Systems Division                     FAX: +44(0)23-9270-1800



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 18:20         ` Robert Dewar
@ 2001-01-31  5:08           ` DuckE
  2001-01-31  5:57             ` Robert Dewar
  0 siblings, 1 reply; 31+ messages in thread
From: DuckE @ 2001-01-31  5:08 UTC (permalink / raw)


> Note that the detailed list in AARM C.6(20) of disallowed
> transformations has no hint at all of the "separate" part of
> Tuck's claim, and conspicuously does not list combining writes
> as an improper transformation.
>
> Tuck, having something in your mind is not good enough if you
> do not write it down :-)
>
> > In general, that means each read/update is a separate
> > instruction.
>
> No, there is absolutely NO implication of this
>

I find the difference in interpretation of AARM C.6(20) interesting.

This clause states:

  "... The implementation shall not generate any memory reads or updates of
atomic or volatile objects other than those specified by the program."

My interpretation of this statement is: if my program contains two separate
assigments to two distinct variables for which pragma atomic applies, these
assignments will be performed as two distinct operations.  Since the two
assignments appear as separate assignments in the code, if the performed
these assignments are combined as single operation, an update is being
performed that my program did not specify.

Since there is obviously some confusion over this issue perhaps the AARM
should be revised?

BTW: When I first started reading about Ada I didn't realize that there was
any confusion on this issue.  It is actually one of the specific features of
the language that made me think Ada is superior for interfacing with
hardware.

SteveD








^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31  5:08           ` DuckE
@ 2001-01-31  5:57             ` Robert Dewar
  2001-02-01  3:31               ` DuckE
  2001-02-02 21:38               ` Mark Lundquist
  0 siblings, 2 replies; 31+ messages in thread
From: Robert Dewar @ 2001-01-31  5:57 UTC (permalink / raw)


In article
<95Nd6.343422$U46.10481049@news1.sttls1.wa.home.com>,
  "DuckE" <nospam_steved94@home.com> wrote:
> I find the difference in interpretation of AARM C.6(20)
> interesting.

Remember that the AARM is not an official document, and not
part of the official standard, so you can use it to try to
understand the motivation behind the standard, but it never
adds anything.


> My interpretation of this statement is: if my program
> contains two separate assigments to two distinct variables
> for which pragma atomic applies, these assignments will be
> performed as two distinct operations.  Since the two
> assignments appear as separate assignments in the code, if
> the performed these assignments are combined as single
> operation, an update is being performed that my program did
> not specify.

First, this statement is not part of the standard, so you
cannot use it in interpreting what conformance means.

But just for the moment, suppose this statement *were* part
of the standard.

Any *semantic* rule in the standard is always an "as-if" rule.
This is fundamental to the nature of semantic specification.
This means that if two possible translations have the same
semantic effect, then they are equivalent.

So I ask you the same question I asked Tuck, namely please
provide the program that will (at least conceptually) show
that the translation you claim is incorrect is semantically
non-equivalent to separate stores.

The trouble is that the semantic domain of the RM is not
at the right level of abstraction to talk about machine
instructions.

THat's why it is often better and more precise to make
requirements of this kind into implementation advice.

In this particular case, the issue of whether to make
this a requirement or IA did not arise, since it is not
stated as a requirement in any case, and (at least speaking
for myself as a reviewier) I had no idea that the design
team intended this requirement. I thought of pragma Atomic
basically as a renaming of the (confusingly named) pragma
Shared in Ada 83, and it was certainly presented this way.

> Since there is obviously some confusion over this issue
> perhaps the AARM should be revised?

That's irrelevant, since the AARM is not an official document.
The only way to resolve confusion on this issue is to send a
comment following the RM procedures, and have the ARG address
the issue.

I would think that the appropriate approach would be to
introduce implementation advice, something to the effect

Implementation Advice
---------------------

A load or store of an atomic object should, where possible,
be implemented by a single load or store instruction which
accesses exactly the bits of the object and no others. The
implementation should document those instances in which
it is not possible to follow this advice.

-----------
The reason this should be IA is that in IA, we are allowed
to talk about things like load and store instructions, and
we can intepret a statement like this in a helpful pragmatic
manner, whereas if it appeared as a formal requirement, it
would be meaningless (since it contains many undefined terms,
and would be susecptible to the as-if semanitc interpretation
which we specifically do NOT want in this case).

I think it is quite reasonable to consider adding some
IA of this kind. I suspect that most implementations can
follow this easily enough -- what is missing is documentation
of when it is not possible.


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 15:57     ` Tucker Taft
  2001-01-30 18:26       ` Robert Dewar
@ 2001-01-31 10:09       ` Rod Chapman
  2001-01-31 21:41         ` Tucker Taft
  1 sibling, 1 reply; 31+ messages in thread
From: Rod Chapman @ 2001-01-31 10:09 UTC (permalink / raw)


In article <3A76E455.AABF2490@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:

> I don't agree with Robert on this.  Have you tried writing it
> as a loop rather than an aggregate assignment.

Of course, but that would usually be considered bad style in
SPARK.  The assignment
  A := A_Type'(others => 0);
has information flow "derives A from ;" (i.e. the final value of
A is derived from "nothing" - a constant - which is probably what
you wanted and expected)

The compound statement
   for I in A'Range loop
      A(I) := 0;
   end loop;
has information flow "derives A from A", which is significantly
different.

Proof of partial correctness is also affected - proving
  --# post A = A_Type'(others => 0);
is trivial in the first case, but rather harder in the latter, so
we nearly always prefer the aggregate.  Our device driver is a fine
example of where we (justifiably) bend the rules... :-)
 - Rod



Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31 10:09       ` Rod Chapman
@ 2001-01-31 21:41         ` Tucker Taft
  2001-02-01  5:33           ` Robert Dewar
                             ` (4 more replies)
  0 siblings, 5 replies; 31+ messages in thread
From: Tucker Taft @ 2001-01-31 21:41 UTC (permalink / raw)


Rod Chapman wrote:
> 
> In article <3A76E455.AABF2490@averstar.com>,
>   Tucker Taft <stt@averstar.com> wrote:
> 
> > I don't agree with Robert on this.  Have you tried writing it
> > as a loop rather than an aggregate assignment.
> 
> Of course, but that would usually be considered bad style in
> SPARK.  The assignment
>   A := A_Type'(others => 0);
> has information flow "derives A from ;" (i.e. the final value of
> A is derived from "nothing" - a constant - which is probably what
> you wanted and expected)
> 
> The compound statement
>    for I in A'Range loop
>       A(I) := 0;
>    end loop;
> has information flow "derives A from A", which is significantly
> different.

I don't understand why this derives A from A.  Is this just
a limitation of SPARK?  Clearly, we are assigning a new
value to every component of A, making no use of the original
values.

> ... Our device driver is a fine
> example of where we (justifiably) bend the rules... :-)

That doesn't surprise me.  Device drivers take special care.

I just bemoan anything that forces one to start using machine
code to write a device driver.  I know that 25 years ago Unix
was one of the first operating systems to have device drivers
written in something other than assembly code.  (I know it was
not *the* first, given Multics, etc.)  If 25 years
later I find we have to drop back to assembly code in Ada,
I would be quite disappointed, and believe we messed up the
language definition somewhere.

>  - Rod
-- 
-Tucker Taft   stt@avercom.net   http://www.averstar.com/~stt/
Chief Technology Officer, AverCom, Inc. (A Titan Company) Burlington, MA  USA
(AverCom was formed 1/1/01 from the Commercial Division of AverStar)
(http://www.averstar.com/services/ebusiness_applications.html)



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31  5:57             ` Robert Dewar
@ 2001-02-01  3:31               ` DuckE
  2001-02-02 21:38               ` Mark Lundquist
  1 sibling, 0 replies; 31+ messages in thread
From: DuckE @ 2001-02-01  3:31 UTC (permalink / raw)


Thank you.  I have sent a request to the ARG to introduce this
implementation advice.

SteveD

"Robert Dewar" <robert_dewar@my-deja.com> wrote in message
news:9589fj$k66$1@nnrp1.deja.com...
[snip]
>
> That's irrelevant, since the AARM is not an official document.
> The only way to resolve confusion on this issue is to send a
> comment following the RM procedures, and have the ARG address
> the issue.
>
> I would think that the appropriate approach would be to
> introduce implementation advice, something to the effect
>
> Implementation Advice
> ---------------------
>
> A load or store of an atomic object should, where possible,
> be implemented by a single load or store instruction which
> accesses exactly the bits of the object and no others. The
> implementation should document those instances in which
> it is not possible to follow this advice.
>
> -----------
> The reason this should be IA is that in IA, we are allowed
> to talk about things like load and store instructions, and
> we can intepret a statement like this in a helpful pragmatic
> manner, whereas if it appeared as a formal requirement, it
> would be meaningless (since it contains many undefined terms,
> and would be susecptible to the as-if semanitc interpretation
> which we specifically do NOT want in this case).
>
> I think it is quite reasonable to consider adding some
> IA of this kind. I suspect that most implementations can
> follow this easily enough -- what is missing is documentation
> of when it is not possible.
>
>
> Sent via Deja.com
> http://www.deja.com/





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31 21:41         ` Tucker Taft
@ 2001-02-01  5:33           ` Robert Dewar
  2001-02-01  9:42           ` Rod Chapman
                             ` (3 subsequent siblings)
  4 siblings, 0 replies; 31+ messages in thread
From: Robert Dewar @ 2001-02-01  5:33 UTC (permalink / raw)


In article <3A7886A7.F1BB5513@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:
> I just bemoan anything that forces one to start using machine
> code to write a device driver.  I know that 25 years ago Unix
> was one of the first operating systems to have device drivers
> written in something other than assembly code.  (I know it
> was
> not *the* first, given Multics, etc.)  If 25 years
> later I find we have to drop back to assembly code in Ada,
> I would be quite disappointed, and believe we messed up the
> language definition somewhere.

As I noted before, device drivers often require very specific
instructions to be issued to the hardware. This is WAY beyond
what can be required in the language definition.


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 21:30         ` Simon Wright
@ 2001-02-01  6:11           ` Robert Dewar
  0 siblings, 0 replies; 31+ messages in thread
From: Robert Dewar @ 2001-02-01  6:11 UTC (permalink / raw)


In article <x7vsnm0vick.fsf@smaug.pushface.org>,
  Simon Wright <simon@pushface.org> wrote:

> If it were another compiler provider, I would be tempted to
> read this whole discussion as "it would cost us a bundle to
> implement this, so let's dig our heels in". I don't for one
> moment believe that that's the case here.

You miss the point entirely.

Probably most compilers DO implement MOST of what is wanted,
but MOST is not really good enough if you are trying to write
reliable portable code.

The trouble is that "it" is not properly defined, and is not
easy to define from a formal requirements point of view. Too
many people write code that they think is correct because it
happens to work using one specific version of one compiler.

It is quite interesting to note that there is MORE machine
code in the Linux kernel than there used to be, precisely
because new better optimizing versions of gcc violated
improper assumptions about code generation sequences.


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31 21:41         ` Tucker Taft
  2001-02-01  5:33           ` Robert Dewar
@ 2001-02-01  9:42           ` Rod Chapman
  2001-02-01 18:10             ` Robert Dewar
  2001-02-01 13:14           ` SPARK flow analysis (was Help with Atomic_Components and whole array assignment) Stuart Palin
                             ` (2 subsequent siblings)
  4 siblings, 1 reply; 31+ messages in thread
From: Rod Chapman @ 2001-02-01  9:42 UTC (permalink / raw)


In article <3A7886A7.F1BB5513@averstar.com>,
  Tucker Taft <stt@averstar.com> wrote:
> Rod Chapman wrote:
> > The compound statement
> >    for I in A'Range loop
> >       A(I) := 0;
> >    end loop;
> > has information flow "derives A from A", which is significantly
> > different.
>
> I don't understand why this derives A from A.  Is this just
> a limitation of SPARK?  Clearly, we are assigning a new
> value to every component of A, making no use of the original
> values.

This is what we call the "array update anomaly" in SPARK.  Consider
the simple assignment statement
  A(1) := 0;
This has information flow "derives A from A" since
1 element of A is changed and all the others are preserved, and
"0" is a literal constant.

The info. flow for a loop is formed (see the maths in Barnes
or in the Bergeretti/Carre ACM TOPLAS paper) from the transitive
closure of the info. flow for its body, so the loop above does
indeed have info. flow "derives A from A".

In _general_, the Examiner is not capable of determining that
all the elements of an array just happen to have been updated
by a sequence or loop of such statements, and the Examiner
does not attempt to spot any such special cases.
(Such as analysis _is_ possible for record fields, though...)

Consider an array A with only 2 elements, and the statements
  A(I) := 0
  A(J) := 1;
where I and J are variables.

Have we updated all the elements of A?  Don't know, so we have
to be conservative.  (Flow analysis is essentially syntax driven -
we do not attempt to solve proof problems during flow analysis!)

In real life, if we really need a loop to initialise, then we'd
do

  procedure Init ( A : out A_Type );
  --# derives A from ;

  procedure Init ( A : out A_Type )
  is
     --# hide Init;
  begin
     ... -- as before...
  end Init;

instructing the Examiner to believe the spec. and to ignore the
body.
 - Rod


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: SPARK flow analysis (was Help with Atomic_Components and whole array assignment)
  2001-01-31 21:41         ` Tucker Taft
  2001-02-01  5:33           ` Robert Dewar
  2001-02-01  9:42           ` Rod Chapman
@ 2001-02-01 13:14           ` Stuart Palin
  2001-02-01 23:38           ` Help with Atomic_Components and whole array assignment Nick Roberts
  2001-02-07 21:40           ` Nick Williams
  4 siblings, 0 replies; 31+ messages in thread
From: Stuart Palin @ 2001-02-01 13:14 UTC (permalink / raw)


Tucker Taft wrote:
<with snipping; use snipping;>

> Rod Chapman wrote:
> > The assignment
> >   A := A_Type'(others => 0);
> > has information flow "derives A from ;" (i.e. the final value of
> > A is derived from "nothing" - a constant - which is probably what
> > you wanted and expected)
> >
> > The compound statement
> >    for I in A'Range loop
> >       A(I) := 0;
> >    end loop;
> > has information flow "derives A from A", which is significantly
> > different.
> 
> I don't understand why this derives A from A.  Is this just
> a limitation of SPARK?  Clearly, we are assigning a new
> value to every component of A, making no use of the original
> values.

You are correct in that in the overall scheme of things A does not
derive from A, because in both cases A is entirely defined as 0. 
However, in the first case the fact that A is fully defined as 0 is
obvious from the _syntax_ of the single statement; whereas in the second
case it only becomes apparent from the _semantics_ of the set of
statements.

The SPARK Examiner analyses code at 2 levels; the less sophisticated of
the two is Flow Analysis which reports on the apparent behaviour of a
subprogram based upon the cumulative effects of statements, using only
the simple syntactic properties of each statement.  Despite being a
"simpler" analysis it is still quite capable of detecting significant
classes of faults, and the more the code behaviour is reflected in the
syntax the better the analysis.
(The value of flow analysis is that it can help eliminate many common
programming errors before investing time and effort into creating proofs
of correctness - or rather, if the program is flawed, failing to produce
a proof and realising your mistake after many hours).

Another example of syntax v semantics would be:
      if B then                if B then
         x := 0;                  x := 0;
      else                     end if;
         x := 1;
      end if;                  if not B then
                                  x := 1;
                               end if;


In the left hand case the fact that x is only dependent on B is clear
from the syntax; whereas in the right hand case this only becomes clear
from the semantics (Flow analysis of the right hand case would suggest
that x may depend on its original value as well as B.  This is because
until you examine the semantics and establish that if x has not been
assigned the value 0 it must be assigned 1.  Looking at the syntax alone
suggests that there might be a path through the code in which x is never
given a value (it also suggests there might be a path in which it is
assigned the value 0 then, without that being used, it might be
re-assigned the value 1: but that is a different story and a different
warning).

When you use SPARK to do semantic analysis and construct program proofs
you would would be able to show that the two programs are equivalent.

--
Stuart Palin
Principal Software Engineer
BAE SYSTEMS Avionics Ltd, Rochester



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-02-01  9:42           ` Rod Chapman
@ 2001-02-01 18:10             ` Robert Dewar
  0 siblings, 0 replies; 31+ messages in thread
From: Robert Dewar @ 2001-02-01 18:10 UTC (permalink / raw)


In article <95bb20$7jb$1@nnrp1.deja.com>,
  Rod Chapman <r_c_chapman@my-deja.com> wrote:
> This is what we call the "array update anomaly" in SPARK.
Consider
> the simple assignment statement
>   A(1) := 0;
> This has information flow "derives A from A" since
> 1 element of A is changed and all the others are preserved,
and
> "0" is a literal constant.

This makes perfectly good sense to me, The array update
notation in these kinds of languages is just a short hand
for

   A := A with (1 => 0)

or somesuch, and in that form, it becomes clear that this
derives A from A




>
> The info. flow for a loop is formed (see the maths in Barnes
> or in the Bergeretti/Carre ACM TOPLAS paper) from the
transitive
> closure of the info. flow for its body, so the loop above
does
> indeed have info. flow "derives A from A".
>
> In _general_, the Examiner is not capable of determining that
> all the elements of an array just happen to have been updated
> by a sequence or loop of such statements, and the Examiner
> does not attempt to spot any such special cases.
> (Such as analysis _is_ possible for record fields, though...)
>
> Consider an array A with only 2 elements, and the statements
>   A(I) := 0
>   A(J) := 1;
> where I and J are variables.
>
> Have we updated all the elements of A?  Don't know, so we
have
> to be conservative.  (Flow analysis is essentially syntax
driven -
> we do not attempt to solve proof problems during flow
analysis!)
>
> In real life, if we really need a loop to initialise, then
we'd
> do
>
>   procedure Init ( A : out A_Type );
>   --# derives A from ;
>
>   procedure Init ( A : out A_Type )
>   is
>      --# hide Init;
>   begin
>      ... -- as before...
>   end Init;
>
> instructing the Examiner to believe the spec. and to ignore
the
> body.
>  - Rod
>
> Sent via Deja.com
> http://www.deja.com/
>


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31 21:41         ` Tucker Taft
                             ` (2 preceding siblings ...)
  2001-02-01 13:14           ` SPARK flow analysis (was Help with Atomic_Components and whole array assignment) Stuart Palin
@ 2001-02-01 23:38           ` Nick Roberts
  2001-02-02  3:45             ` Robert Dewar
  2001-02-07 21:40           ` Nick Williams
  4 siblings, 1 reply; 31+ messages in thread
From: Nick Roberts @ 2001-02-01 23:38 UTC (permalink / raw)


If it's any consolation Tuck, my interpretation of Volatile (nothing to do
with Atomic) would always have been (and still is) that:

   for i in A'Range loop
      A(i) := 0;
   end loop;

where Volatile (or Volatile_Components) applied to A, would generate
A'Length separate copies into memory, in whatever machine code it was.

My interpretation of Atomic would be simply to avoid generating code that
might bugger up multi-task access to the object Atomicked (or its components
if Atomic_Componented). Of course, Atomic shoves in a dose of Volatile
automatically, and quite right too.

I propose a representation attribute, Storage_Operations, of type
System.Storage_Operations.Operation_Profile, which is an array of Boolean
indexed on an enumerated type System.Storage_Operations.Operation_Mode,
which would have a value for every (relevant) kind of basic memory access
the compiler could generate. E.g.:

   package System.Storage_Operations is
      type Operation_Mode is (Read_8, Read_16, Read_32, Write_8, Write_16,
Write_32);
      type Operation_Profile is array (Access_Mode) of Boolean;
   end;

   A: array (...) of ...;
   for A'Storage_Operations use (Read_8, Write_8);

This attribute could be used in a representation clause to specify precisely
which kinds of memory access are allowed for an object or type. Perhaps its
use should imply or require Volatile. It would, of course, be fairly
machine-dependent, but that's unavoidable. It would often allow the
avoidance of assembly; in some situations this could be very valuable.

We could have a package e.g.:

   with Interfaces;
   package System.Port_Access is
      type Port_8_Address is mod 2**16;
      type Port_8_Element is new Interfaces.Unsigned_8;
      type Port_16_Address is mod 2**16;
      type Port_16_Element is new Interfaces.Unsigned_16;
      generic
         type Index_Type is (<>);
      package Arrays_Of is
         type Port_8_Array is array (Index_Type range <>) of Port_8_Element;
         type Port_16_Array is array (Index_Type range <>) of
Port_16_Element;
      end;
      -- also provide for offsets, arithmetic, etc.
   end;

and then:

   Flags: System.Port_Access.Port_16_Element;
   for Flags'Port_Address use 16#012E#;

   subtype Data_Port is Integer range 0..3;
   package Data_IO is System.Port_Access.Arrays_Of(Data_Port)
   Data: Data_IO.Port_8_Array(Data_Port);
   subtype Data_Area is System.Port_Access.Port_8_Address range
16#0120#..16#0123#;
   for Data'Port_Address use Data_Area;

This would often allow assembly to be avoided for port access. Better and
better, eh?

Finally, if I were writing a device driver, in any language, I would want to
look at the machine code produced - very carefully, in places - regardless
of whether it seemed to work or not, just to see what it was really doing.
(But then I'm paranoid like that ;-)

PS: I'm making proposals with the aim of putting them into an actual
compiler which will be used in a specific situation (which involves lots of
device drivers). Helpful criticism or better proposals welcome!

--
Nick Roberts
http://www.AdaOS.org






^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-02-01 23:38           ` Help with Atomic_Components and whole array assignment Nick Roberts
@ 2001-02-02  3:45             ` Robert Dewar
  0 siblings, 0 replies; 31+ messages in thread
From: Robert Dewar @ 2001-02-02  3:45 UTC (permalink / raw)


In article <95ctln$ff437$2@ID-25716.news.dfncis.de>,
  "Nick Roberts" <nickroberts@callnetuk.com> wrote:
> If it's any consolation Tuck

I doubt Tuck needs consolation at all, let alone from Nick :-)
:-)

> my interpretation of Volatile (nothing to do
> with Atomic) would always have been (and still is) that:
>
>    for i in A'Range loop
>       A(i) := 0;
>    end loop;
>
> where Volatile (or Volatile_Components) applied to A, would
> generate A'Length separate copies into memory, in whatever
> machine code it was.

Fine, but you cannot just state "your interpretation" without
backing it up with evidence from the RM.

> My interpretation of Atomic would be simply to avoid
> generating code that might bugger up multi-task access to the
> object Atomicked

But as you surely know, all Atomic objects are also Volatile,
so I don't see your point

> I propose a representation attribute, Storage_Operations

<<proposal snipped>>

This seems ill-conceived and far too complex. I don't see what
it would buy in terms of portable code. I think the paragraph
of implementation advice I suggested would be adequate to
achieve everything this more complex proposal does in practice.


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31  5:57             ` Robert Dewar
  2001-02-01  3:31               ` DuckE
@ 2001-02-02 21:38               ` Mark Lundquist
  2001-02-02 23:08                 ` Robert Dewar
  2001-02-03  1:39                 ` tmoran
  1 sibling, 2 replies; 31+ messages in thread
From: Mark Lundquist @ 2001-02-02 21:38 UTC (permalink / raw)



Robert Dewar <robert_dewar@my-deja.com> wrote in message
news:9589fj$k66$1@nnrp1.deja.com...
>[...]
> Any *semantic* rule in the standard is always an "as-if" rule.
> This is fundamental to the nature of semantic specification.
> This means that if two possible translations have the same
> semantic effect, then they are equivalent.

[DING!] (light bulb turning on...)

Robert, when you first (in a reply to my post) stated that IA would be more
binding in this case than a requirement, I did not understand what you could
be talking about.  If something were meaningless, then what would it mean
for an implementation to follow or not follow it?  The "as if" explanation
clears this up.  The key phrase is "semantically meaningless", and that is
precisely defined.  If a language rule's only meaning is at other than the
semantic level, then as a requirement it has all the force of a bogus
requirement, namely nil.  But as IA it can have some teeth.






^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-02-02 21:38               ` Mark Lundquist
@ 2001-02-02 23:08                 ` Robert Dewar
  2001-02-03  1:39                 ` tmoran
  1 sibling, 0 replies; 31+ messages in thread
From: Robert Dewar @ 2001-02-02 23:08 UTC (permalink / raw)


In article <95fbit$nen$2@usenet.rational.com>,
  "Mark Lundquist" <mark@rational.com> wrote:
  But as IA it can have some teeth.

Exactly! :-)


Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-02-02 21:38               ` Mark Lundquist
  2001-02-02 23:08                 ` Robert Dewar
@ 2001-02-03  1:39                 ` tmoran
  1 sibling, 0 replies; 31+ messages in thread
From: tmoran @ 2001-02-03  1:39 UTC (permalink / raw)


Suppose a compiler's target machine had a two-level memory architecture,
wouldn't you expect a serious compiler to generate code using, in a
reasonably decent way, the architecture?  Suppose instead the target
machine had two kinds of memory addresses: RAM and IO ports.  Seems
to me a serious compiler would know the difference and generate
appropriate instructions for each.  Code generation for a (non-existent)
machine where all the addresses were RAM, would rightly be
considered irrelevant.



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-30 18:26       ` Robert Dewar
  2001-01-30 21:30         ` Simon Wright
@ 2001-02-06  0:32         ` Richard Kenner
  2001-02-06  3:15           ` Robert Dewar
  1 sibling, 1 reply; 31+ messages in thread
From: Richard Kenner @ 2001-02-06  0:32 UTC (permalink / raw)


In article <9570vu$fv0$1@nnrp1.deja.com> Robert Dewar <robert_dewar@my-deja.com> writes:
>The GNU/Linux kernel had endless problems from assumptions
>of this kind, and finally they have all been replaced by
>machine language insertions, to avoid the problems. What
>happened in this case is that new improved and correct gcc
>compilers blew the kernel out of the water by breaking these
>undocumented assumptions.

That's an oversimplification, unfortunately.  Most of the assumptions
were indeed in machine language insertions, but the assumption were
things that GCC would do *around* those insertions (such as register
choice).  GCC has powerful facilities for saying where operands are
found and such, but they weren't fully used since "it worked without them".
The change was to use the machine-code insertions properly.

One other thing that would sometimes be seen was going off the end of
an array purposely in order to reference a variable in the calling
program.



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-02-06  0:32         ` Richard Kenner
@ 2001-02-06  3:15           ` Robert Dewar
  0 siblings, 0 replies; 31+ messages in thread
From: Robert Dewar @ 2001-02-06  3:15 UTC (permalink / raw)


In article <RCHf6.24$OP6.330@typhoon.nyu.edu>,
  kenner@lab.ultra.nyu.edu (Richard Kenner) wrote:
> One other thing that would sometimes be seen was going off
> the end of an array purposely in order to reference a
> variable in the calling program.

And that of course is just clearly undefined code, so there is
no way a compiler can guarantee to behave as expected for this
kind of error.



Sent via Deja.com
http://www.deja.com/



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Help with Atomic_Components and whole array assignment
  2001-01-31 21:41         ` Tucker Taft
                             ` (3 preceding siblings ...)
  2001-02-01 23:38           ` Help with Atomic_Components and whole array assignment Nick Roberts
@ 2001-02-07 21:40           ` Nick Williams
  4 siblings, 0 replies; 31+ messages in thread
From: Nick Williams @ 2001-02-07 21:40 UTC (permalink / raw)


Tucker Taft wrote:


>> The compound statement
>>    for I in A'Range loop
>>       A(I) := 0;
>>    end loop;
>> has information flow "derives A from A", which is significantly
>> different.

> I don't understand why this derives A from A.  Is this just
> a limitation of SPARK?  Clearly, we are assigning a new
> value to every component of A, making no use of the original
> values.

Well, yes; clearly, it is simple to prove that this loop assigns new 
values to every element of A, but in terms of information flow (as 
defined by Bergeretti and Carre, and as implemented in the SPARK 
Examiner) it 'derives A from A'.

The central intuition derives from the first iteration through the loop 
- in this case, the new value of A is derived from a constant loop 
range, a literal constant and A itself (since only one element has changed).

The limitation is that array elements are not 'first class' from the 
perspective of the flow analyser - even if this were theoretically 
viable, the practicalities of tracking flow relations for a ten million 
element array would, I suspect, be prohibitive.

However - as I understand it - it's not even technically useful to 
promote array elements in this way within the current framework; to do 
so makes flow analysis equivalent to execution:

   subtype A_Type is Integer range 1 .. 1000;
   type An_Array is array A_Type of Integer;

   A : An_Array;
   X : A_Type;
   function Complicated_Function returns A_Type;
   function Another_Complicated_Function returns Integer;

   ...

   X := Complicated_Function;
   A(X) := Another_Complicated_Function;

Without actually calculating X, all that can be said is that any given 
element of A might potentially be assigned to by the above statements. 
However it equally well might not, and (as such) for all relevant I, 
A(I) would be derived from A(I), and whatever variables are used in the 
derivation of the result of Another_Complicated_Function.

Although I'm sure there are some simple cases where performing flow 
analysis at the array element level gives more intuitively 'correct' 
analyses, I'm minded to think that it probably would not be a very 
useful addition - I'm sure Peter or Rod will pick me up if they disagree!

Cheers,

Nick
PxCS




^ permalink raw reply	[flat|nested] 31+ messages in thread

end of thread, other threads:[~2001-02-07 21:40 UTC | newest]

Thread overview: 31+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2001-01-22 11:22 Help with Atomic_Components and whole array assignment r_c_chapman
2001-01-22 12:51 ` Stuart Palin
2001-01-22 14:16   ` mark_lundquist
2001-01-22 16:09     ` Pat Rogers
2001-01-22 16:29     ` Robert Dewar
2001-01-22 19:52       ` Mark Lundquist
2001-01-30 15:54       ` Tucker Taft
2001-01-30 18:20         ` Robert Dewar
2001-01-31  5:08           ` DuckE
2001-01-31  5:57             ` Robert Dewar
2001-02-01  3:31               ` DuckE
2001-02-02 21:38               ` Mark Lundquist
2001-02-02 23:08                 ` Robert Dewar
2001-02-03  1:39                 ` tmoran
2001-01-22 16:21 ` Robert Dewar
2001-01-22 16:39   ` r_c_chapman
2001-01-30 15:57     ` Tucker Taft
2001-01-30 18:26       ` Robert Dewar
2001-01-30 21:30         ` Simon Wright
2001-02-01  6:11           ` Robert Dewar
2001-02-06  0:32         ` Richard Kenner
2001-02-06  3:15           ` Robert Dewar
2001-01-31 10:09       ` Rod Chapman
2001-01-31 21:41         ` Tucker Taft
2001-02-01  5:33           ` Robert Dewar
2001-02-01  9:42           ` Rod Chapman
2001-02-01 18:10             ` Robert Dewar
2001-02-01 13:14           ` SPARK flow analysis (was Help with Atomic_Components and whole array assignment) Stuart Palin
2001-02-01 23:38           ` Help with Atomic_Components and whole array assignment Nick Roberts
2001-02-02  3:45             ` Robert Dewar
2001-02-07 21:40           ` Nick Williams

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox