From: | "John R. Strohm" <strohm@airmail.net> |
Newsgroups: | comp.compilers |
Date: | 29 Jan 2003 23:37:52 -0500 |
Organization: | Compilers Central |
References: | 03-01-065 03-01-070 03-01-126 03-01-164 03-01-169 |
Keywords: | code, optimize |
Posted-Date: | 29 Jan 2003 23:37:52 EST |
"Rodney M. Bates" wrote:
> Actually, this is somewhat of a time-bomb in Ada. On some cases, the
> language specifies the actual parameter transmission mechanism. But in
> some combinations of types and transmission modes, the language leaves
> it up to the compiler writer whether to use reference or some
> variation of copy in/out, etc. In the presence of non-local variable
> references, aliasing, etc., this can affect program semantics.
True. On the other hand, it is generally understood by now, thirty years
after the Structured Programming Revolution, that non-local variable
references and aliasing are Bad Things To Do.
> If you write an Ada program that depends on which mechanism the
> compiler chooses, the language defines your program as "erroneous",
> which means you will not get any error message and whatever happens
> is entirely your fault. I'm sure erroneousness is undecidable.
One you allow non-local variable references in the presence of
interrupts, for example, you are in a world of hurt, because it is
impossible to say from one instant to the next what value a non-local
variable might actually have, without examining EVERY line of code in
the system that MIGHT touch that variable. You may write it in one
line, and test it in the next, but in between the two an interrupt
occurred and the interrupt handler had to change the state variable.
(This may not be directly do-able in Ada, but the principle applies.)
Observe that this makes it impossible to say that a procedure actually
does what it claims to do, if one of the variables it uses can be
trashed by someone else.
The Gypsy language at UT Austin in the late 1970s (Ambler, Good, et
al) was designed specifically to be formally verifiable. They did it
the easy way, and outlawed aliasing and non-local references
altogether. Every variable was local to some task, and tasks could
only send messages through message buffers (FIFO queues protected by
semaphores). The message buffers were built-in to the language, with
semantics carefully defined.
Return to the
comp.compilers page.
Search the
comp.compilers archives again.