Type safety on wikipedia

Type safety on wikipedia

[Martin Krischik]

Hello

I found this interesting article on Wikipedia which made me think a
bit:

http://en.wikipedia.org/wiki/Type_safety

Do have a look at the talk page as well.

Martin

Re: Type safety on wikipedia

[Alex R. Mosteo]

Martin Krischik wrote:
> Hello
> 
> I found this interesting article on Wikipedia which made me think a
> bit:
> 
> http://en.wikipedia.org/wiki/Type_safety
> 
> Do have a look at the talk page as well.

After reading that I'm not sure how Ada can be type safe if unchecked 
deallocation is a common way of implementing relatively common tasks as 
linked lists and so. The explicit example given for "type unsafety" is 
easily doable in Ada.

But I acknowledge that I'm new to the topic, anyone can explain?

Re: Type safety on wikipedia

[Rod Chapman]

We would make a strong case the SPARK is statically type-safe.
 - Rod, SPARK Team

Re: Type safety on wikipedia

[jimmaureenrogers]

"The appropriate formalization of this slogan depends on the style of
formal semantics used for a particular language. In the context of
denotational semantics, type safety means that the meaning (or the
value) of an expression that is well-typed, say with type t, is a bona
fide member of the set corresponding to t."

Even with unchecked conversion Ada has the 'Valid attribute, allowing
the programmer to determine if the result of an unchecked conversion is
a valid value.

I do not see how Unchecked_Deallocation interferes with type safety.
Ada access types are typed. There is no Ada equivalent to a C void*. An
Ada access type cannot be made to point to an object of some foreign
type. For instance,

    type Integer_Access is access Integer;

An instance of Integer_Access cannot reference a task, or a real
number, or some record type. Garbage collection cannot improve type
safety in Ada or any other language. It can only automate the process
of deallocating dynamically allocated objects.

Jim Rogers

Re: Type safety on wikipedia

[Alex R. Mosteo]

jimmaureenrogers@worldnet.att.net wrote:

> I do not see how Unchecked_Deallocation interferes with type safety.
> Ada access types are typed. There is no Ada equivalent to a C void*. An
> Ada access type cannot be made to point to an object of some foreign
> type. For instance,
> 
>     type Integer_Access is access Integer;
> 
> An instance of Integer_Access cannot reference a task, or a real
> number, or some record type. Garbage collection cannot improve type
> safety in Ada or any other language. It can only automate the process
> of deallocating dynamically allocated objects.

Well, the argument given in the discussion is like this: you allocate a 
pointer, make some aliases and free one of them. Further allocations 
(presumibly unrelated) reuse the same heap area. You can now use a 
dangling pointer not correctly deallocated pointing to a valid memory 
area within the program, but holding completely unrelated data (from 
other types, probably).

Obviously, in a GCed language, no memory area can be reallocated as long 
as any reference to it is still alive.

There's a glaring affirmation in the article (not discussion) saying 
that Ada is type safe, with ML. So I wonder.

Re: Type safety on wikipedia

[Martin Krischik]

Alex R. Mosteo wrote:

> jimmaureenrogers@worldnet.att.net wrote:
> 
>> I do not see how Unchecked_Deallocation interferes with type safety.
>> Ada access types are typed. There is no Ada equivalent to a C void*. An
>> Ada access type cannot be made to point to an object of some foreign
>> type. For instance,
>> 
>>     type Integer_Access is access Integer;
>> 
>> An instance of Integer_Access cannot reference a task, or a real
>> number, or some record type. Garbage collection cannot improve type
>> safety in Ada or any other language. It can only automate the process
>> of deallocating dynamically allocated objects.
> 
> Well, the argument given in the discussion is like this: you allocate a
> pointer, make some aliases and free one of them. Further allocations
> (presumibly unrelated) reuse the same heap area. You can now use a
> dangling pointer not correctly deallocated pointing to a valid memory
> area within the program, but holding completely unrelated data (from
> other types, probably).
> 
> Obviously, in a GCed language, no memory area can be reallocated as long
> as any reference to it is still alive.
> 
> There's a glaring affirmation in the article (not discussion) saying
> that Ada is type safe, with ML. So I wonder.

It's a Wiki and there is a dispute warning on top of it. I wonder if the Ada
link need to be removed! And perhaps a chapter on almost type save
languages could be added where Ada would more better placed.

But then Ada is supposed to me GC - only the vendors are to lazy to add an
collector.

As said: It made me think.

Martin

-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Rod Chapman wrote:

> We would make a strong case the SPARK is statically type-safe.
>  - Rod, SPARK Team

It's a wiki - go ahead. I think that SPARK will then the only statically
type-safe language - as Ada will only make it to almost type save group.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Alex R. Mosteo wrote:

> Martin Krischik wrote:
>> Hello
>> 
>> I found this interesting article on Wikipedia which made me think a
>> bit:
>> 
>> http://en.wikipedia.org/wiki/Type_safety
>> 
>> Do have a look at the talk page as well.
> 
> After reading that I'm not sure how Ada can be type safe if unchecked
> deallocation is a common way of implementing relatively common tasks as
> linked lists and so. The explicit example given for "type unsafety" is
> easily doable in Ada.

That is my thinking as well. 

> But I acknowledge that I'm new to the topic, anyone can explain?

The Wikipage describes a stricter rule to the term "type save" then most Ada
programmer would think. Have we been wrong or is this rule to strict to be
practical. Mind you academics never cared for practical.

And I have allways been an advocate for GC and this proves me somehow.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

<verï¿œffentlicht & per Mail versendet>

Rod Chapman wrote:

> We would make a strong case the SPARK is statically type-safe.
>  - Rod, SPARK Team

I changed the text to be more honest about things. I also mentioned SPARK -
but perhaps a  "SPARK Team" memeber want to have a look and improve.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Alex R. Mosteo]

Martin Krischik wrote:

> But then Ada is supposed to me GC - only the vendors are to lazy to add an
> collector.

This is something I've mused about sometimes: Let's suppose some Ada 
compiler goes ahead and provides a GC. What happens with programs 
written without taking this into account?

AFAIK, there's pragma Controlled (ARM 13.11.3) which /prevents/ 
collection (this is already curious, since it suggest to me that GC 
tends to be implemented by default). I have never used it, so, are all 
my types using unchecked deallocation potentially problematic? Would a 
compiler implementing GC suddenly start to give errors when 
instantiating UD for types without this pragma?

And what a curious name election? Talking about controlled types can 
refer to Finalization or to access types with this pragma applied.

Just curious.

Re: Type safety on wikipedia

[Florian Weimer]

> Even with unchecked conversion Ada has the 'Valid attribute, allowing
> the programmer to determine if the result of an unchecked conversion is
> a valid value.

Only in very limited cases.

> I do not see how Unchecked_Deallocation interferes with type safety.

The following is just a rough sketch, but maybe it helps to clarify
the terms.

A type system gives you a subset of all expressions which are
well-typed (in Ada, 1 + 1 is well-typed, but 1.0 + 1 is not).

A type-safe language has a type system with these two properties: any
well-typed expression which is not a value can be reduced to a simpler
expression, according to a set of run-time evaluation rules (which
define the semantics of the language) -- and these simplification
steps preserve the well-typedness of expressions.

(Of course, considerable notational overhead is needed to apply this
definitions in a rigorous manner to real-world programming languages.)

Now, suppose that X is a pool-specific access value for some type T,
and Free is a corresponding instance of Ada.Unchecked_Deallocation.
Suppose that


   Free (X);

has just been exected.  Suppose the next thing to be evaluated is

   declare
      Y : T := X.all;
   begin
      ...

Now X.all is not a value, so it has to reduce (at run-time) to some
other expression.  But the language definition explicitly tells you
that no such rule exists.  Therefore, the first rule I mentioned is
violated, and Ada with Ada.Unchecked_Deallocation is not type-safe.

Re: Type safety on wikipedia

[Dmitry A. Kazakov]

On Thu, 26 Jan 2006 16:18:52 +0100, Alex R. Mosteo wrote:

> Well, the argument given in the discussion is like this: you allocate a 
> pointer, make some aliases and free one of them.

This is bad, but has nothing to do with type safety. The contract of a
pointer (access type) isn't violated this way.

> Obviously, in a GCed language, no memory area can be reallocated as long 
> as any reference to it is still alive.

Reference is not pointer. The contract of reference may require the above.
As such memory has no contract, it is untyped. Further, there is nothing in
type system that prevents typed objects from sharing memory, even when
types are different. Example: T and T'Class.
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Type safety on wikipedia

[Simon Wright]

"Alex R. Mosteo" <devnull@mailinator.com> writes:

> Martin Krischik wrote:
>> Hello
>> I found this interesting article on Wikipedia which made me think a
>> bit:
>> http://en.wikipedia.org/wiki/Type_safety
>> Do have a look at the talk page as well.
>
> After reading that I'm not sure how Ada can be type safe if unchecked
> deallocation is a common way of implementing relatively common tasks
> as linked lists and so. The explicit example given for "type unsafety"
> is easily doable in Ada.
>
> But I acknowledge that I'm new to the topic, anyone can explain?

As the page says (near the end) "The following languages are type safe
by default but can free themself from the type systems when needed."
and then lists Ada.

Re: Type safety on wikipedia

[Simon Wright]

"Alex R. Mosteo" <devnull@mailinator.com> writes:

> This is something I've mused about sometimes: Let's suppose some Ada
> compiler goes ahead and provides a GC. What happens with programs
> written without taking this into account?

13.11.2(17) only says that Free _should_ reclaim the storage. I
suppose for a GC implementation there could be at least 2
implementation strategies:

 * don't actually reclaim, just remove local reference and deal with
   tasks if necessary

 * check that the reference count is in fact 1 and raise *_Error if
   not! That would be useful!

Re: Type safety on wikipedia

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> "Alex R. Mosteo" <devnull@mailinator.com> writes:
[cut]
> As the page says (near the end) "The following languages are type safe
> by default but can free themself from the type systems when needed."
> and then lists Ada.

I think that Martin has changed the page that Alex was talking about
into the page I was talking about. The dangers of async communication!

Re: Type safety on wikipedia

[Bobby D. Bryant]

On Thu, 26 Jan 2006, "Alex R. Mosteo" <devnull@mailinator.com> wrote:

> Martin Krischik wrote:
>> Hello
>> 
>> I found this interesting article on Wikipedia which made me think a
>> bit:
>> 
>> http://en.wikipedia.org/wiki/Type_safety
>> 
>> Do have a look at the talk page as well.
> 
> After reading that I'm not sure how Ada can be type safe if unchecked 
> deallocation is a common way of implementing relatively common tasks as 
> linked lists and so. The explicit example given for "type unsafety" is 
> easily doable in Ada.
> 
> But I acknowledge that I'm new to the topic, anyone can explain?

The Unchecked_Deallocation has to be instantiated for a specific type.
Is there a way of using it that isn't type safe?  (Surely it isn't the
type that's "Unchecked" ?)

-- 
Bobby Bryant
Austin, Texas

Re: Type safety on wikipedia

[jimmaureenrogers]

Florian Weimer wrote:
> Now, suppose that X is a pool-specific access value for some type T,
> and Free is a corresponding instance of Ada.Unchecked_Deallocation.
> Suppose that
>
>
>    Free (X);
>
> has just been exected.  Suppose the next thing to be evaluated is
>
>    declare
>       Y : T := X.all;
>    begin
>       ...


Let's look at an actual program doing an equivalent action:

with Ada.Text_Io;

procedure Access_Test is
   type Int_Access is access Integer;
   P : Int_Access;
begin
   P := null;
   Ada.Text_Io.Put_Line(Integer'Image(P.All));
end Access_Test;


The problem is one of attempting to dereference a null access object.
The above program compiles without error.

When run, I get the following error message:

raised CONSTRAINT_ERROR: access_test.adb:8 access check failed

It appears that Ada's runtime checks detect an erroneous problem.
I would say that a program that terminates with a CONSTRAINT_ERROR
has not exhibited the same kind of improper behavior as a program that
does not detect the problem.

In C, while it is an error to de-reference a null pointer, the runtime
system
does nothing to detect the problem. C programs continue with really
nasty
garbage values.

Jim Rogers

Re: Type safety on wikipedia

[Martin Krischik]

Indeed. I have barely finished my changes when they where "imporved".

Martin

PS: the "improvement" is ok so I leave it as it is.

Re: Type safety on wikipedia

[Alex R. Mosteo]

Simon Wright wrote:
> "Alex R. Mosteo" <devnull@mailinator.com> writes:
> 
> 
>>This is something I've mused about sometimes: Let's suppose some Ada
>>compiler goes ahead and provides a GC. What happens with programs
>>written without taking this into account?
> 
> 
> 13.11.2(17) only says that Free _should_ reclaim the storage. I
> suppose for a GC implementation there could be at least 2
> implementation strategies:
> 
>  * don't actually reclaim, just remove local reference and deal with
>    tasks if necessary
> 
>  * check that the reference count is in fact 1 and raise *_Error if
>    not! That would be useful!

Neat! I hadn't figured that path of action. Indeed it seems a very good 
strategy. I can imagine unknown bugs popping out after years of silently 
wait and rare crashes... hehe...

Re: Type safety on wikipedia

[Alex R. Mosteo]

Bobby D. Bryant wrote:
> On Thu, 26 Jan 2006, "Alex R. Mosteo" <devnull@mailinator.com> wrote:
> 
> 
>>Martin Krischik wrote:
>>
>>>Hello
>>>
>>>I found this interesting article on Wikipedia which made me think a
>>>bit:
>>>
>>>http://en.wikipedia.org/wiki/Type_safety
>>>
>>>Do have a look at the talk page as well.
>>
>>After reading that I'm not sure how Ada can be type safe if unchecked 
>>deallocation is a common way of implementing relatively common tasks as 
>>linked lists and so. The explicit example given for "type unsafety" is 
>>easily doable in Ada.
>>
>>But I acknowledge that I'm new to the topic, anyone can explain?
> 
> 
> The Unchecked_Deallocation has to be instantiated for a specific type.
> Is there a way of using it that isn't type safe?  (Surely it isn't the
> type that's "Unchecked" ?)

If I've understood things correctly, the problem isn't that UD is typed, 
but that once you start manipulating heap pointers by hand, you're out 
of the game (due to dangling pointers and so).

But then, I'm talking by hearsay from wikipedia sources that I don't 
really trust. The last post from Florian seems to point that the problem 
is much more fundamental (again, if IIUTC).

Re: Type safety on wikipedia

[Alex R. Mosteo]

Florian Weimer wrote:
>>Even with unchecked conversion Ada has the 'Valid attribute, allowing
>>the programmer to determine if the result of an unchecked conversion is
>>a valid value.
> 
> 
> Only in very limited cases.
> 
> 
>>I do not see how Unchecked_Deallocation interferes with type safety.
> 
> 
> The following is just a rough sketch, but maybe it helps to clarify
> the terms.
> 
> A type system gives you a subset of all expressions which are
> well-typed (in Ada, 1 + 1 is well-typed, but 1.0 + 1 is not).
> 
> A type-safe language has a type system with these two properties: any
> well-typed expression which is not a value can be reduced to a simpler
> expression, according to a set of run-time evaluation rules (which
> define the semantics of the language) -- and these simplification
> steps preserve the well-typedness of expressions.
> 
> (Of course, considerable notational overhead is needed to apply this
> definitions in a rigorous manner to real-world programming languages.)
> 
> Now, suppose that X is a pool-specific access value for some type T,
> and Free is a corresponding instance of Ada.Unchecked_Deallocation.
> Suppose that
> 
> 
>    Free (X);
> 
> has just been exected.  Suppose the next thing to be evaluated is
> 
>    declare
>       Y : T := X.all;
>    begin
>       ...
> 
> Now X.all is not a value, so it has to reduce (at run-time) to some
> other expression.  But the language definition explicitly tells you
> that no such rule exists.  Therefore, the first rule I mentioned is
> violated, and Ada with Ada.Unchecked_Deallocation is not type-safe.

Thanks for your effort in making us understand. However, there's still 
something fundamental that I'm not grasping.

According to the current Wikipedia article, Java is believed to be type 
safe. However, one can have null pointers in Java. For example:

public class Test {
	public static void main (String args[]) {
		Integer x = new Integer (5);
		Integer y = null;
		
		System.out.println ("X + Y: " + (x + y));
	}
}

will compile without warnings with latest JDK1.5 and run as:

$ java Test
X: 5
Exception in thread "main" java.lang.NullPointerException
         at Test.main(Test.java:7)

This means that Java has explicit rules for when this happens that 
differ from those in Ada? Since Ada also detects null pointer usage, and 
per your example it makes Ada type unsafe.

Conversely, I understand that evaluations that yield out-of-range values 
don't make a language type-unsafe because these cases have well-defined 
rules of behavior.

Maybe I should go now to read the original paper linked from the wikipedia.

Re: Type safety on wikipedia

[Martin Krischik]

You can manualy free memory - provided all pointers pointing to the
freed memory are set to null at the same time. And access to a null
pointer is handled in orderly manner.

This could be implemented by using a linked list of smart pointers. GC
is only one option open.

Martin

Re: Type safety on wikipedia

[Martin Krischik]

Hello Alex,

null pointer are ok - provides they are handled in orderly manner. An
exception is orderly manner.

i.E. On my old Atari many years ago one could easily access (int*)0
returning some silly value - no MMU was there to prevent that. Now that
is not orderly manner.

The same holds for  out-of-range values. If they are handled in an
orderly manner (exception) then it's ok. Ada's mod types are ok as well
as the wrap around is properly defined and not "undefined behavior".

Martin

Re: Type safety on wikipedia

[Georg Bauhaus]

On Fri, 2006-01-27 at 12:14 +0100, Alex R. Mosteo wrote:
 
> > The Unchecked_Deallocation has to be instantiated for a specific type.
> > Is there a way of using it that isn't type safe?  (Surely it isn't the
> > type that's "Unchecked" ?)
> 
> If I've understood things correctly, the problem isn't that UD is typed, 
> but that once you start manipulating heap pointers by hand, you're out 
> of the game (due to dangling pointers and so).

I have added a sentence on the effects of pragma Pure to the Ada section
of the article. (No named access types.)


-- Georg 

Re: Type safety on wikipedia

[Florian Weimer]

* Alex R. Mosteo:

>> Suppose that
>>    Free (X);
>> has just been exected.  Suppose the next thing to be evaluated is
>>    declare
>>       Y : T := X.all;
>>    begin

Make that:

   X2 := X;
   Feee (X);

   declare
      Y : T := X2.all;
   begin

This one is clearly erroneous -- I forgot the other side effect of
Free.

Re: Type safety on wikipedia

[Larry Kilgallen]

In article <1138363035.664717.262330@g47g2000cwa.googlegroups.com>, "Martin Krischik" <krischik@users.sourceforge.net> writes:

> You can manualy free memory - provided all pointers pointing to the
> freed memory are set to null at the same time. And access to a null
> pointer is handled in orderly manner.

If a program is correct, having the pointers become null is not an issue.
Referencing through a null pointer or a stale pointer is equally wrong.

Re: Type safety on wikipedia

[Martin Krischik]

jimmaureenrogers@worldnet.att.net wrote:

> 
> Florian Weimer wrote:
>> Now, suppose that X is a pool-specific access value for some type T,
>> and Free is a corresponding instance of Ada.Unchecked_Deallocation.
>> Suppose that
>>
>>
>>    Free (X);
>>
>> has just been exected.  Suppose the next thing to be evaluated is
>>
>>    declare
>>       Y : T := X.all;
>>    begin
>>       ...
> 
> 
> Let's look at an actual program doing an equivalent action:

> with Ada.Text_Io;
> 
> procedure Access_Test is
>    type Int_Access is access Integer;
>    P : Int_Access;
> begin
>    P := null;
>    Ada.Text_Io.Put_Line(Integer'Image(P.All));
> end Access_Test;

Make that

with Ada.Text_Io;

procedure Access_Test is
    type Int_Access is access Integer;
    procedure Deallocate is new Unchecked_Deallocation ....

   P : Int_Access := new Integer;
   Q : Int_Access := P;
begin
    Deallocate (P);
    Ada.Text_Io.Put_Line(Integer'Image(Q.All));
 end Access_Test;

That is what the garbage collection chapter of the article is all about. 
For a type save language behavior of this code snippet must be well
defined. But in Ada it is not. 

Martin

-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Simon Wright wrote:

> "Alex R. Mosteo" <devnull@mailinator.com> writes:
> 
>> This is something I've mused about sometimes: Let's suppose some Ada
>> compiler goes ahead and provides a GC. What happens with programs
>> written without taking this into account?
> 
> 13.11.2(17) only says that Free _should_ reclaim the storage. I
> suppose for a GC implementation there could be at least 2
> implementation strategies:
> 
>  * don't actually reclaim, just remove local reference and deal with
>    tasks if necessary
> 
>  * check that the reference count is in fact 1 and raise *_Error if
>    not! That would be useful!

That is indeed interesting. Up until now I have implemented the interface to
the bohem-weiser collector as such that memory is reclaimed. Being German I
did not spot the true meaning of should. I might reconsider the
implementation.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Larry Kilgallen wrote:

> In article <1138363035.664717.262330@g47g2000cwa.googlegroups.com>,
> "Martin Krischik" <krischik@users.sourceforge.net> writes:
> 
>> You can manualy free memory - provided all pointers pointing to the
>> freed memory are set to null at the same time. And access to a null
>> pointer is handled in orderly manner.
> 
> If a program is correct, having the pointers become null is not an issue.
> Referencing through a null pointer or a stale pointer is equally wrong.

Not of access of a null pointer raises an exceptions. Exceptions are
considered well defined. See the talk page.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Simon Wright]

"Alex R. Mosteo" <devnull@mailinator.com> writes:

> Simon Wright wrote:
>> "Alex R. Mosteo" <devnull@mailinator.com> writes:
>> 
>>>This is something I've mused about sometimes: Let's suppose some Ada
>>>compiler goes ahead and provides a GC. What happens with programs
>>>written without taking this into account?
>> 13.11.2(17) only says that Free _should_ reclaim the storage. I
>> suppose for a GC implementation there could be at least 2
>> implementation strategies:
>>  * don't actually reclaim, just remove local reference and deal with
>>    tasks if necessary
>>  * check that the reference count is in fact 1 and raise *_Error if
>>    not! That would be useful!
>
> Neat! I hadn't figured that path of action. Indeed it seems a very
> good strategy. I can imagine unknown bugs popping out after years of
> silently wait and rare crashes... hehe...

One point I had forgotten is that deallocation of a controlled object
will finalize it -- LRM 13.11.2(9) -- so looking at it through a
dangling pointer will be a Bad Thing even if GC has ensured that the
mamory hasn't been re-used for something else.

Re: Type safety on wikipedia

[Simon Wright]

Martin Krischik <krischik@users.sourceforge.net> writes:

> Simon Wright wrote:
>
>> "Alex R. Mosteo" <devnull@mailinator.com> writes:
>> 
>>> This is something I've mused about sometimes: Let's suppose some Ada
>>> compiler goes ahead and provides a GC. What happens with programs
>>> written without taking this into account?
>> 
>> 13.11.2(17) only says that Free _should_ reclaim the storage. I
>> suppose for a GC implementation there could be at least 2
>> implementation strategies:
>> 
>>  * don't actually reclaim, just remove local reference and deal with
>>    tasks if necessary
>>
>>  * check that the reference count is in fact 1 and raise *_Error if
>>    not! That would be useful!
>
> That is indeed interesting. Up until now I have implemented the interface to
> the bohem-weiser collector as such that memory is reclaimed. Being German I
> did not spot the true meaning of should. I might reconsider the
> implementation.

I was imagining that GC and Free might be independent, so that (modulo
tasks and finalization) Free would only have to null the pointer and
GC would magically see later that the memory was no longer
referenced. I think the collector you're working on s more
cooperative?

I think that a dangling pointer is only a _potential_ deathtrap, so my
second suggestion is perhaps a bit over the top. On the other hand, in
safety-related systems one would prefer to avoid even the possibility
...

Re: Type safety on wikipedia

[Larry Kilgallen]

In article <17514424.vPDbTzKvie@linux1.krischik.com>, Martin Krischik <krischik@users.sourceforge.net> writes:
> Larry Kilgallen wrote:
> 
>> In article <1138363035.664717.262330@g47g2000cwa.googlegroups.com>,
>> "Martin Krischik" <krischik@users.sourceforge.net> writes:
>> 
>>> You can manualy free memory - provided all pointers pointing to the
>>> freed memory are set to null at the same time. And access to a null
>>> pointer is handled in orderly manner.
>> 
>> If a program is correct, having the pointers become null is not an issue.
>> Referencing through a null pointer or a stale pointer is equally wrong.
> 
> Not of access of a null pointer raises an exceptions. Exceptions are
> considered well defined. See the talk page.

I gather you are trying to say some people plan to have their programs
access via a null pointer and then handle an exception.  That seems
incredibly sloppy.  It is also likely to be quite inefficient on some
Ada implementations.

I have no idea what you mean by "the talk page".

Re: Type safety on wikipedia

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message
news:m23bj9h35k.fsf@grendel.local...
...
> One point I had forgotten is that deallocation of a controlled object
> will finalize it -- LRM 13.11.2(9) -- so looking at it through a
> dangling pointer will be a Bad Thing even if GC has ensured that the
> mamory hasn't been re-used for something else.

Which reminds me of a significant issue: Ada 95 doesn't allow early (or
late) finalization of limited controlled objects. (Whether it allows early
finalization of nonlimited controlled objects is open to debate.) That means
that GC cannot collect objects containing limited controlled components
"early". But since a program written with GC in mind won't use
Unchecked_Deallocation, and the access types will likely be library level,
"early" and "anytime before completion of main" are the same. Since I think
most objects in a program ought to be controlled, that's a significant
problem.

We talked about this a few times, but never came near a consensus on how to
fix this, so Ada 2005 inherits the issue intact. I suppose if anyone was
seriously trying to use GC in their implementation, the priority level would
go up...

                                    Randy.

Re: Type safety on wikipedia

[Jan Andres]

On 2006-01-27, Martin Krischik <krischik@users.sourceforge.net> wrote:
> with Ada.Text_Io;
>
> procedure Access_Test is
>     type Int_Access is access Integer;
>     procedure Deallocate is new Unchecked_Deallocation ....
>
>    P : Int_Access := new Integer;
>    Q : Int_Access := P;
> begin
>     Deallocate (P);
>     Ada.Text_Io.Put_Line(Integer'Image(Q.All));
>  end Access_Test;

Hmm, but aren't all the restrictions on the scope of access values
actually there in order to guarantee type safety, as long as no unsafe
constructs like 'Unchecked_Access are used? Or is
Unchecked_Deallocation itself considered to be such an unsafe construct?
If so, is there any "safe" alternative in Ada that we can use if we
don't have GC?

Of course you could simply avoid such constructs as quoted above but
the downside is that the language will not actually enforce this.

Regards
-- 
Jan Andres <jandres@gmx.net>

Re: Type safety on wikipedia

[Martin Krischik]

Jan Andres wrote:

> On 2006-01-27, Martin Krischik <krischik@users.sourceforge.net> wrote:
>> with Ada.Text_Io;
>>
>> procedure Access_Test is
>>     type Int_Access is access Integer;
>>     procedure Deallocate is new Unchecked_Deallocation ....
>>
>>    P : Int_Access := new Integer;
>>    Q : Int_Access := P;
>> begin
>>     Deallocate (P);
>>     Ada.Text_Io.Put_Line(Integer'Image(Q.All));
>>  end Access_Test;
> 
> Hmm, but aren't all the restrictions on the scope of access values
> actually there in order to guarantee type safety, as long as no unsafe
> constructs like 'Unchecked_Access are used? Or is
> Unchecked_Deallocation itself considered to be such an unsafe construct?
> If so, is there any "safe" alternative in Ada that we can use if we
> don't have GC?

No, there is no save alternative. There is a talk page where the authors of
the page discuss the page content and how to improve.

From there it becomes more and more clear that strictly type save language
might only be a special purpose language and that general purpose languages
can't be type save. A bit like original Pascal.

If you look at the page now: There is no list of type save languages - there
is a list of almost type save languages and there weak spots. Even
Standart-ML has a weak spot: interfacing with other languages.

Ok, there is SPARK. But for once SPARK is special purpose and hey, does
SPARK not allow interfacing with other non-type-save languages?

> Of course you could simply avoid such constructs as quoted above but
> the downside is that the language will not actually enforce this.

Indeed. For me this discussion means that I will renew my effort on garbage
collection in Ada. AdaCL was the next on the list for the gnuada
distribution anyway - now that ASIS has been added.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Simon Wright wrote:

> Martin Krischik <krischik@users.sourceforge.net> writes:
> 
>> Simon Wright wrote:
>>
>>> "Alex R. Mosteo" <devnull@mailinator.com> writes:
>>> 
>>>> This is something I've mused about sometimes: Let's suppose some Ada
>>>> compiler goes ahead and provides a GC. What happens with programs
>>>> written without taking this into account?
>>> 
>>> 13.11.2(17) only says that Free _should_ reclaim the storage. I
>>> suppose for a GC implementation there could be at least 2
>>> implementation strategies:
>>> 
>>>  * don't actually reclaim, just remove local reference and deal with
>>>    tasks if necessary
>>>
>>>  * check that the reference count is in fact 1 and raise *_Error if
>>>    not! That would be useful!
>>
>> That is indeed interesting. Up until now I have implemented the interface
>> to the bohem-weiser collector as such that memory is reclaimed. Being
>> German I did not spot the true meaning of should. I might reconsider the
>> implementation.
> 
> I was imagining that GC and Free might be independent, so that (modulo
> tasks and finalization) Free would only have to null the pointer and
> GC would magically see later that the memory was no longer
> referenced. I think the collector you're working on s more
> cooperative?

The collector I work on (or better bind to) is also used in GCC Java and GCC
Objective-C and supports finalization and unchecked deallocation.

Current Roadmap:

* stress tests the collector interface -  especially task and finalization.
* make the collector interface available via the GNU Ada project.

Martinn
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Simon Wright wrote:

> "Alex R. Mosteo" <devnull@mailinator.com> writes:
> 
>> Simon Wright wrote:
>>> "Alex R. Mosteo" <devnull@mailinator.com> writes:
>>> 
>>>>This is something I've mused about sometimes: Let's suppose some Ada
>>>>compiler goes ahead and provides a GC. What happens with programs
>>>>written without taking this into account?
>>> 13.11.2(17) only says that Free _should_ reclaim the storage. I
>>> suppose for a GC implementation there could be at least 2
>>> implementation strategies:
>>>  * don't actually reclaim, just remove local reference and deal with
>>>    tasks if necessary
>>>  * check that the reference count is in fact 1 and raise *_Error if
>>>    not! That would be useful!
>>
>> Neat! I hadn't figured that path of action. Indeed it seems a very
>> good strategy. I can imagine unknown bugs popping out after years of
>> silently wait and rare crashes... hehe...
> 
> One point I had forgotten is that deallocation of a controlled object
> will finalize it -- LRM 13.11.2(9) -- so looking at it through a
> dangling pointer will be a Bad Thing even if GC has ensured that the
> mamory hasn't been re-used for something else.

Damm - so I have to leave everything as it is.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Martin Krischik]

Larry Kilgallen wrote:

> In article <17514424.vPDbTzKvie@linux1.krischik.com>, Martin Krischik
> <krischik@users.sourceforge.net> writes:
>> Larry Kilgallen wrote:
>> 
>>> In article <1138363035.664717.262330@g47g2000cwa.googlegroups.com>,
>>> "Martin Krischik" <krischik@users.sourceforge.net> writes:
>>> 
>>>> You can manualy free memory - provided all pointers pointing to the
>>>> freed memory are set to null at the same time. And access to a null
>>>> pointer is handled in orderly manner.
>>> 
>>> If a program is correct, having the pointers become null is not an
>>> issue. Referencing through a null pointer or a stale pointer is equally
>>> wrong.
>> 
>> Not of access of a null pointer raises an exceptions. Exceptions are
>> considered well defined. See the talk page.
> 
> I gather you are trying to say some people plan to have their programs
> access via a null pointer and then handle an exception.  That seems
> incredibly sloppy.  It is also likely to be quite inefficient on some
> Ada implementations.

In praxis it is indeed sloppy. However: the program does not get "stuck" and
has a well defined path of execution - and that is the important part for
the theory.
 
> I have no idea what you mean by "the talk page".

Any Wikimedia page has a talk page associated where the authors discuss the
page progress:

Page: http://en.wikipedia.org/wiki/Type_safety
Talk: http://en.wikipedia.org/wiki/Talk:Type_safety

There is a link at the top of the page to the talk page. Using the
English/Monobook user interface the link is called [_Discussion_].

For the page in question the discussion is about thee time the main article
- a very controversial toppic indeed.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Type safety on wikipedia

[Florian Weimer]

* Larry Kilgallen:

> I gather you are trying to say some people plan to have their programs
> access via a null pointer and then handle an exception.  That seems
> incredibly sloppy.

Sure, but it's still well-defined in terms of language semantics.  The
program does not "go wrong", as required by the rules for type safety.

The null pointer example is actually a good one because it shows that
even if a program is type safe, it is not necessarily correct.  And
Java with its null pointer exception problem shows that a language
with a type system which is believed to be safe can result in
practical problems which other, even unsafe type systems avoid
(cf. C++ references).

Re: Type safety on wikipedia

[Randy Brukardt]

"Jan Andres" <jandres@gmx.net> wrote in message
news:dreihb$712$1@pitr.home.jan...
...
> Hmm, but aren't all the restrictions on the scope of access values
> actually there in order to guarantee type safety, as long as no unsafe
> constructs like 'Unchecked_Access are used? Or is
> Unchecked_Deallocation itself considered to be such an unsafe construct?
> If so, is there any "safe" alternative in Ada that we can use if we
> don't have GC?
>
> Of course you could simply avoid such constructs as quoted above but
> the downside is that the language will not actually enforce this.

The language (well, a compiler) can be made to enforce "No
Unchecked_Deallocation" using pragma Restrictions
(No_Unchecked_Deallocation); Similarly, you can prevent the use of
'Unchecked_Access with pragma Restrictions (No_Unchecked_Access); [Note that
these are program-wide, which might restrict the standard packages that you
can use.]

You can avoid using Unchecked_Deallocation if you can arrange for the access
type itself to go away, and then use a storage_pool for the storage. Or,
sometimes, you never need to free the data structure anyway (a compiler
symbol table comes to mind; it exists until the compile finishes). But both
of those are often impractical.

                                 Randy.

Re: Type safety on wikipedia

[Dave Thompson]

On 26 Jan 2006 16:38:29 -0800, "jimmaureenrogers@worldnet.att.net"
<jimmaureenrogers@worldnet.att.net> wrote:
<snip>
> The problem is one of attempting to dereference a null access object.
> The above program compiles without error.
> 
The actual problem is a dangling access (pointer) not a null one, as
already noted elsethread.

> When run, I get [CONSTRAINT_ERROR]...
> It appears that Ada's runtime checks detect an erroneous problem. ...

Yes, at least by default.

> In C, while it is an error to de-reference a null pointer, the runtime
> system
> does nothing to detect the problem. C programs continue with really
> nasty
> garbage values.
> 
Yes and no. The C standard leaves it up to the implementation.

On some (increasingly many) systems with virtual memory where it is
easy (enough) to leave page (or even segment) 0 unmapped, it will give
a clear error, usually even a recoverable signal (roughly like the
exception in Ada). On some (other) systems, (virtual) 0 is accessible
(and accessed) but is reserved and initialized with "useful" data,
such as 4 bytes of zero which in the most common read cases (as a
string, char, or int) gives a safe and possibly even useful result.

But you can't portably rely on, or enforce, this; and garbage is
certainly a possibility.


- David.Thompson1 at worldnet.att.net

Re: Type safety on wikipedia

[Larry Kilgallen]

In article <fildu1p2q1glsq3kmmpaesumabg0p5gjc0@4ax.com>, Dave Thompson <david.thompson1@worldnet.att.net> writes:

> On some (increasingly many) systems with virtual memory where it is
> easy (enough) to leave page (or even segment) 0 unmapped, it will give
> a clear error, usually even a recoverable signal (roughly like the
> exception in Ada). On some (other) systems, (virtual) 0 is accessible
> (and accessed) but is reserved and initialized with "useful" data,
> such as 4 bytes of zero which in the most common read cases (as a
> string, char, or int) gives a safe and possibly even useful result.

Well, there is only one virtual zero address within a given program
execution address space, and I seem to recall that at least one LISP
implementation used that for a crucial piece of data (that had to be
addressed as zero in that implementation).  Thus one could not depend
on the lack of physical memory at zero in any program built from both
LISP and Ada modules.