High-Integrity OO and controlled types

High-Integrity OO and controlled types

[Maciej Sobczak]

There is an interesting white paper describing the high-integrity
point of view on object-oriented programming:

http://www.open-do.org/high-integrity-oo-programming-in-ada/

One of the parts that has caught my attention is the description of
GNAT high-integrity profiles, where it is written that controlled
types are not supported (page 43):

"Controlled types are not supported since they require extensive run-
time support."

This is surprising to me. I don't see anything in controlled types
that would require "extensive run-time support". Obviously, there is
some implicit additional code required for controlled types to work,
but as far as I understand this additional code can be entirely
generated by the compiler (in many cases even the dynamic dispatch can
be omitted) and no run-time library is necessary for it at all.

Am I missing something? What "extensive run-time support" is needed
for controlled types that excludes them from high-integrity GNAT
profiles?

There is another angle to this question: the Ravenscar profile does
not exclude controlled types. If GNAT's so-called Ravenscar profile
does exclude them, then it looks that it does not support some
formally valid Ravenscar programs, even some very trivial ones. Am I
missing something?

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

Re: High-Integrity OO and controlled types

[Robert A Duff]

Maciej Sobczak <see.my.homepage@gmail.com> writes:

> "Controlled types are not supported since they require extensive run-
> time support."
>
> This is surprising to me. I don't see anything in controlled types
> that would require "extensive run-time support".

Most of the "extensive run-time support" comes from heap-allocated
objects containing controlled parts.

If you say (for example, perhaps in a nested scope):

    type A is access T'Class;
    type T2 is new T with ...;
    X : A := new T2'(...);

the language requires that Unchecked_Deallocation of X calls Finalize on
all the controlled subcomponents of X.all, plus X.all itself if that's
controlled.  Also, that finalization of type A finalizes all objects in
the "collection" that still exist (U_D wasn't called).  This requires
that the implementation keep track of which objects (that have some
controlled parts) still exist.

So "new" has to put the object on some sort of list, and U_D has to take
it off the list, and finalization of the access type has to worry about
all the objects still on the list, and worry about Finalize operations
that (try to) do "new", putting more objects on the list.

And that "list" (or whatever it is) has to be protected from concurrent
access, via some sort of locking.

Note that for "new T'Class'(...)", it is not necessarily known at
compile time whether the new object has some controlled parts.

Finalization also needs to deal with partially-initialized objects,
and finalize exactly those subcomponents that were successfully
initialized.

That's all "extensive run-time support".

>...Obviously, there is
> some implicit additional code required for controlled types to work,
> but as far as I understand this additional code can be entirely
> generated by the compiler (in many cases even the dynamic dispatch can
> be omitted) and no run-time library is necessary for it at all.

In theory, yes, all of it could be compiler-generated code.
But you really wouldn't want that.

- Bob

Re: High-Integrity OO and controlled types

[Simon Wright]

Robert A Duff <bobduff@shell01.TheWorld.com> writes:

> Maciej Sobczak <see.my.homepage@gmail.com> writes:
[...]
>>...Obviously, there is
>> some implicit additional code required for controlled types to work,
>> but as far as I understand this additional code can be entirely
>> generated by the compiler (in many cases even the dynamic dispatch can
>> be omitted) and no run-time library is necessary for it at all.
>
> In theory, yes, all of it could be compiler-generated code.
> But you really wouldn't want that.

Because there'll be more of it?

And I don't suppose there's much difference from the point of view of
creating an audited application between code generated by the compiler
and code in an RTS (after all, it's probably the same team in both
cases!)

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Sun, 01 May 2011 17:29:10 -0400, Robert A Duff wrote:

> Maciej Sobczak <see.my.homepage@gmail.com> writes:
> 
>> "Controlled types are not supported since they require extensive run-
>> time support."

A prejudice

>> This is surprising to me. I don't see anything in controlled types
>> that would require "extensive run-time support".
> 
> Most of the "extensive run-time support" comes from heap-allocated
> objects containing controlled parts.
> 
> If you say (for example, perhaps in a nested scope):
> 
>     type A is access T'Class;
>     type T2 is new T with ...;
>     X : A := new T2'(...);
[...]
> Finalization also needs to deal with partially-initialized objects,
> and finalize exactly those subcomponents that were successfully
> initialized.
>
> That's all "extensive run-time support".

No, that is an extensive run-time support of dynamically allocated
controlled objects. Any dynamically allocated object requires run-time
support (e.g. heap), which can be considered extensive.

Regarding Finalization, that is not "support", it is a part of the type's
semantics. In this sense the ADD instruction is a run-time support of
Integer type, and thus the whole program's code is "support" of itself. 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Cyrille]

On May 1, 10:38 pm, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
> There is an interesting white paper describing the high-integrity
> point of view on object-oriented programming:
>
> http://www.open-do.org/high-integrity-oo-programming-in-ada/
>
> One of the parts that has caught my attention is the description of
> GNAT high-integrity profiles, where it is written that controlled
> types are not supported (page 43):
>
> "Controlled types are not supported since they require extensive run-
> time support."
>
> This is surprising to me. I don't see anything in controlled types
> that would require "extensive run-time support".

Admittedly, we could provide more info here. "Extensive runtime
support" is, in fact, only one aspect of it. Let me first say why
"runtime support" is an issue: that's because in a HI context, the Ada
runtime needs to be certified along with the application and thus
certification material  (for various standards) needs to be developed
and maintained. This is one of the reasons why we minimize  our HI
runtime footprint. There are other reasons: source to object tracea

> Obviously, there is
> some implicit additional code required for controlled types to work,
> but as far as I understand this additional code can be entirely
> generated by the compiler (in many cases even the dynamic dispatch can
> be omitted) and no run-time library is necessary for it at all.
>
> Am I missing something? What "extensive run-time support" is needed
> for controlled types that excludes them from high-integrity GNAT
> profiles?
>
> There is another angle to this question: the Ravenscar profile does
> not exclude controlled types. If GNAT's so-called Ravenscar profile
> does exclude them, then it looks that it does not support some
> formally valid Ravenscar programs, even some very trivial ones. Am I
> missing something?
>
> --
> Maciej Sobczak *http://www.msobczak.com*http://www.inspirel.com

Re: High-Integrity OO and controlled types

[Cyrille]

> > This is surprising to me. I don't see anything in controlled types
> > that would require "extensive run-time support".
>
> Admittedly, we could provide more info here. "Extensive runtime
> support" is, in fact, only one aspect of it. Let me first say why
> "runtime support" is an issue: that's because in a HI context, the Ada
> runtime needs to be certified along with the application and thus
> certification material  (for various standards) needs to be developed
> and maintained. This is one of the reasons why we minimize  our HI
> runtime footprint. There are other reasons: source to object tracea

(this message was posted too fast...)

so I was saying "source to object" traceability (as required for
do-178b level A) becomes more difficult. And finally, this feature is
not that useful in very critical part of a system. The most common use
of controlled types is for dynamic memory management. something that
is usually avoided in the most critical part of the system. If you
really need to use dynamic memory management, then demonstrating the
correctness of the allocation strategy is not particularly easy in
such a context. It's probably simpler to wait for a fully certified GC
system to appear and used that instead...


> > There is another angle to this question: the Ravenscar profile does
> > not exclude controlled types. If GNAT's so-called Ravenscar profile
> > does exclude them, then it looks that it does not support some
> > formally valid Ravenscar programs, even some very trivial ones. Am I
> > missing something?

right. HI profiles come with additional restrictions. Note that
Ravenscar is just a restriction of the tasking model. So many
different profiles can claim to be "Ravenscar" compliant. For some of
our ports we provide 2 different ones: one less restricted than the
other.

Re: High-Integrity OO and controlled types

[Robert A Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Sun, 01 May 2011 17:29:10 -0400, Robert A Duff wrote:
>
>> Maciej Sobczak <see.my.homepage@gmail.com> writes:
>> 
>>> "Controlled types are not supported since they require extensive run-
>>> time support."
>
> A prejudice

Note that we're talking about pragmas Restrictions and Profile.
That is, self-imposed restrictions.  If you don't want to obey
these restrictions, you don't have to -- just don't use those
pragmas in your project.

- Bob

Re: High-Integrity OO and controlled types

[Maciej Sobczak]

On May 2, 12:01 pm, Cyrille <co...@eu.adacore.com> wrote:

> not that useful in very critical part of a system. The most common use
> of controlled types is for dynamic memory management.

[...]

(this is in line with other responses)

Thank you, this explains it a bit. Note, however, that controlled
types can be also useful for more general resource management,
including I/O resources. It is not clear to me how much of it can be
expected in a typical (is there such a thing?) HI system, but
controlled types can add to the overall safety by ensuring proper
resource management, especially in the presence of exceptions - which
are inherent part of Ada, unless SPARK is involved.

Excluding controlled types altogether sounded like throwing baby out
with the water, but now the motivations are a bit more clear to me.

> Note that
> Ravenscar is just a restriction of the tasking model. So many
> different profiles can claim to be "Ravenscar" compliant. For some of
> our ports we provide 2 different ones: one less restricted than the
> other.

Now I understand.

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Mon, 02 May 2011 12:32:53 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Sun, 01 May 2011 17:29:10 -0400, Robert A Duff wrote:
>>
>>> Maciej Sobczak <see.my.homepage@gmail.com> writes:
>>> 
>>>> "Controlled types are not supported since they require extensive run-
>>>> time support."
>>
>> A prejudice
> 
> Note that we're talking about pragmas Restrictions and Profile.

Rather about rationale behind such restrictions. You gave an example of an
overhead caused by local access-to-controlled types. That has a far
narrower scope than *any* usage of controlled types. A restriction of such
access types can be reasonable (as well as, and much more importantly,
precluding dynamic accessibility checks). Prohibiting all controlled types
is just irrational.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Robert A Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Mon, 02 May 2011 12:32:53 -0400, Robert A Duff wrote:
>> Note that we're talking about pragmas Restrictions and Profile.
>
> Rather about rationale behind such restrictions.

OK.

>...You gave an example of an
> overhead caused by local access-to-controlled types.

No, all access-to-controlled types -- not just local ones.
And access to non-controlled types that contain controlled components.

And it's not just overhead (as in run-time efficiency) -- it's the complexity of
the run-time support.

And it's not access types per se -- it's heap-allocated objects
(i.e. "new") that introduces most of the complexity.

>..That has a far
> narrower scope than *any* usage of controlled types.

Yes, that's a fair point.  Perhaps the restrictions should have been
somewhat narrower.  But note that until recently, GNAT used a bunch of
run-time system calls (and linked lists) for stack-allocated controlled
objects, too.  It was a huge amount of work to fix that.

Another thing to consider: limited controlled types are simpler than
non-limited ones.

>...A restriction of such
> access types can be reasonable (as well as, and much more importantly,
> precluding dynamic accessibility checks).

Well, dynamic accessibility checks are a separate issue, but I must say:
I do NOT like dynamic accessibility checks.

>...Prohibiting all controlled types
> is just irrational.

I think "irrational" is too strong.  The people who want these sorts
of restrictions tend to like conservative rules.

- Bob

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Mon, 02 May 2011 20:08:43 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>>...You gave an example of an
>> overhead caused by local access-to-controlled types.
> 
> No, all access-to-controlled types -- not just local ones.
> And access to non-controlled types that contain controlled components.

If Unchecked_Deallocation is called on each allocated object controlled or
with controlled components, that would make keeping the list of allocated
objects superfluous. I think that restrictions should work in this
direction.

> And it's not just overhead (as in run-time efficiency) -- it's the complexity of
> the run-time support.

Well, but this applies to compile time support too, e.g. optimization and
the GENERICS! Pragmatically, yes, certainly more complex the language thing
is, more likely it is broken. But it is a compiler's property. I, as a
software designer, am not in the position to decide, if the given compiler
has bugs and which language features get spoiled. Thus it does not belong
to a profile.

> And it's not access types per se -- it's heap-allocated objects
> (i.e. "new") that introduces most of the complexity.

I agree, but that is not specific to controlled types.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Cyrille]

On May 2, 9:25 pm, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
>
> Excluding controlled types altogether sounded like throwing baby out
> with the water, but now the motivations are a bit more clear to me.
>

HI profiles are usually much more constrained. The first goal of this
document is to gather the necessary information to make it possible to
build a safety case when using tagged types and more generally OOP in
a HI context. Usually those are banned along with almost all the
"advanced" features of the language. So no baby thrown with the water.
This is a the other way around: we put more water in the bath so that
maybe one day we can consider bathing your "controlled" baby ;-)

Once tagged types and their additional verification activities are
accepted, adding "controlled" types to the mix doesn't require a major
step forward and becomes mostly a matter of cost since there would be
additional runtime to certify and a more complex source to object
traceability.

Re: High-Integrity OO and controlled types

[Maciej Sobczak]

On May 3, 11:32 am, Cyrille <co...@eu.adacore.com> wrote:

> > Excluding controlled types altogether sounded like throwing baby out
> > with the water, but now the motivations are a bit more clear to me.
>
> HI profiles are usually much more constrained. The first goal of this
> document is to gather the necessary information to make it possible to
> build a safety case when using tagged types and more generally OOP in
> a HI context. Usually those are banned along with almost all the
> "advanced" features of the language. So no baby thrown with the water.
> This is a the other way around: we put more water in the bath so that
> maybe one day we can consider bathing your "controlled" baby ;-)

I see. Note that between these two:

1. dynamically allocated class-wide (with open hierarchy) objects tied
to locally scoped storage pool with all resulting mess, and

2. limited controlled object on the stack as a way to hook scope exit
event

there is a *wide* spectrum of use cases, some of them being
unreasonable in the HI context, but some of them being entirely
justified.

I would very much welcome at least that second extreme above being
acknowledged as a valid programming pattern in safety critical
systems.

Another angle: the fact that the lack of controlled types in HI
profiles can be considered as a problem is entirely a result of the
fact that Ada completely screwed this aspect at the beginning.
Controlledness should not be based on tags - it should be a completely
orthogonal property of the type, without any relation to class-wide
objects and dispatching calls (see C++ for an example). Interestingly
this conclusion comes up regularly. Time to fix that part of the
language, perhaps? ;-)

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Tue, 3 May 2011 02:59:05 -0700 (PDT), Maciej Sobczak wrote:

> Controlledness should not be based on tags - it should be a completely
> orthogonal property of the type, without any relation to class-wide
> objects and dispatching calls (see C++ for an example). Interestingly
> this conclusion comes up regularly. Time to fix that part of the
> language, perhaps? ;-)

There are three meaning of being controlled:

1. Ada 83 used it to refer memory allocation (pragma Controlled)
2. Since Ada 95 it is both
2.a. An ability to influence initialization and finalization
2.b. An ability to have a [non-generic] class

Yes, things need to be sorted out.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Georg Bauhaus]

On 03.05.11 11:59, Maciej Sobczak wrote:

> Another angle: the fact that the lack of controlled types in HI
> profiles can be considered as a problem is entirely a result of the
> fact that Ada completely screwed this aspect at the beginning.
> Controlledness should not be based on tags - it should be a completely
> orthogonal property of the type,

Actually, in non-flat languages like Ada, scope exit
actions should be based on scopes, not (just) types,
as types can effectively span multiple scopes.

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Tue, 03 May 2011 13:28:12 +0200, Georg Bauhaus wrote:

> On 03.05.11 11:59, Maciej Sobczak wrote:
> 
>> Another angle: the fact that the lack of controlled types in HI
>> profiles can be considered as a problem is entirely a result of the
>> fact that Ada completely screwed this aspect at the beginning.
>> Controlledness should not be based on tags - it should be a completely
>> orthogonal property of the type,
> 
> Actually, in non-flat languages like Ada, scope exit
> actions should be based on scopes, not (just) types,
> as types can effectively span multiple scopes.

But typed languages tend to consider actions as operations defined on
types, with certain contracts, reusable, clearly bound effects etc.

Actions as amorphous chunks of code tossed here and there depending on
scope is a way different ["anisotropic"] approach. In particular it does
not fit into safe modular software design, because of this "anisotropy".

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Georg Bauhaus]

On 03.05.11 14:27, Dmitry A. Kazakov wrote:
> On Tue, 03 May 2011 13:28:12 +0200, Georg Bauhaus wrote:
> 
>> On 03.05.11 11:59, Maciej Sobczak wrote:
>>
>>> Another angle: the fact that the lack of controlled types in HI
>>> profiles can be considered as a problem is entirely a result of the
>>> fact that Ada completely screwed this aspect at the beginning.
>>> Controlledness should not be based on tags - it should be a completely
>>> orthogonal property of the type,
>>
>> Actually, in non-flat languages like Ada, scope exit
>> actions should be based on scopes, not (just) types,
>> as types can effectively span multiple scopes.
> 
> But typed languages tend to consider actions as operations defined on
> types, with certain contracts, reusable, clearly bound effects etc.
> 
> Actions as amorphous chunks of code tossed here and there depending on
> scope is a way different ["anisotropic"] approach. In particular it does
> not fit into safe modular software design, because of this "anisotropy".

What will type-object/module code look like if it is equivalent
to its nested analog?  Better?

My guess is that to achieve the necessary linking, one passes
Italian food handles to constructors and/or established registries
that receive "events" like "a scope X has been left".

In general, would the type-object/module approach work
better?  For example, assuming something like the naturally nested
Integrate function.

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Tue, 03 May 2011 17:22:50 +0200, Georg Bauhaus wrote:

> On 03.05.11 14:27, Dmitry A. Kazakov wrote:
>> On Tue, 03 May 2011 13:28:12 +0200, Georg Bauhaus wrote:
>> 
>>> On 03.05.11 11:59, Maciej Sobczak wrote:
>>>
>>>> Another angle: the fact that the lack of controlled types in HI
>>>> profiles can be considered as a problem is entirely a result of the
>>>> fact that Ada completely screwed this aspect at the beginning.
>>>> Controlledness should not be based on tags - it should be a completely
>>>> orthogonal property of the type,
>>>
>>> Actually, in non-flat languages like Ada, scope exit
>>> actions should be based on scopes, not (just) types,
>>> as types can effectively span multiple scopes.
>> 
>> But typed languages tend to consider actions as operations defined on
>> types, with certain contracts, reusable, clearly bound effects etc.
>> 
>> Actions as amorphous chunks of code tossed here and there depending on
>> scope is a way different ["anisotropic"] approach. In particular it does
>> not fit into safe modular software design, because of this "anisotropy".
> 
> What will type-object/module code look like if it is equivalent
> to its nested analog?  Better?

Analogue of what? The point is that "finally" cannot replace initialization
and finalization of objects, specific or class-wide.

The opposite is wrong. Any example where "finally" might be useful is
motivated by improperly designed types, e.g. File_Type, which does not
close itself upon destruction.

> My guess is that to achieve the necessary linking, one passes
> Italian food handles to constructors and/or established registries
> that receive "events" like "a scope X has been left".

See above, you need not to handle scopes. Scopes are ad-hoc, used for the
purpose of defining the lifespan of some objects. Leaving scope is as event
as leaving loop, leaving the else alternative of an if etc. If you need
such events re-design!

> For example, assuming something like the naturally nested
> Integrate function.

BTW, integrating function is an object. For this object the compiler
generates finalization, which in particular kills the closure. Care to show
how to do this using "finally"?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Robert A Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> If Unchecked_Deallocation is called on each allocated object controlled or
> with controlled components, that would make keeping the list of allocated
> objects superfluous. I think that restrictions should work in this
> direction.

Yes, it would make sense to have such a feature.  I'm happy to add as
many restrictions as customers need.

>> And it's not just overhead (as in run-time efficiency) -- it's the complexity of
>> the run-time support.
>
> Well, but this applies to compile time support too, e.g. optimization and
> the GENERICS! Pragmatically, yes, certainly more complex the language thing
> is, more likely it is broken. But it is a compiler's property. I, as a
> software designer, am not in the position to decide, if the given compiler
> has bugs and which language features get spoiled. Thus it does not belong
> to a profile.
>
>> And it's not access types per se -- it's heap-allocated objects
>> (i.e. "new") that introduces most of the complexity.
>
> I agree, but that is not specific to controlled types.

Heap-allocation has some complexity.  When controlled types are added,
there's a whole new layer of complexity.

- Bob

Re: High-Integrity OO and controlled types

[Robert A Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> There are three meaning of being controlled:
>
> 1. Ada 83 used it to refer memory allocation (pragma Controlled)
> 2. Since Ada 95 it is both
> 2.a. An ability to influence initialization and finalization
> 2.b. An ability to have a [non-generic] class

I am unaware of 2.b.  I know there are two meanings: 1 and 2.a.

> Yes, things need to be sorted out.

Shrug.  Nobody uses pragma Controlled, so I don't see a huge problem
with the terminology.

- Bob

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Tue, 03 May 2011 12:53:13 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> There are three meaning of being controlled:
>>
>> 1. Ada 83 used it to refer memory allocation (pragma Controlled)
>> 2. Since Ada 95 it is both
>> 2.a. An ability to influence initialization and finalization
>> 2.b. An ability to have a [non-generic] class
> 
> I am unaware of 2.b.  I know there are two meanings: 1 and 2.a.

OK, 2.b (T'Class) is actually allowed for any tagged type.

>> Yes, things need to be sorted out.
> 
> Shrug.  Nobody uses pragma Controlled, so I don't see a huge problem
> with the terminology.

I think that Maciej meant that initialization and finalization is
orthogonal to an ability to form a class (or being tagged as one possible
implementation of this). I agree with that, but in my view both should be
allowed to all types anyway. If Ada reached that level of regularity I
would like you not care about separation, but unfortunately it has not.
Moreover many (not me) think that taggedness should be kept isolated, so
the restriction goes. If this separation is to be maintained, one should
make initialization and finalization independent on that.

So, my opinion depends on path the language roadmap.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Georg Bauhaus]

On 5/3/11 6:28 PM, Dmitry A. Kazakov wrote:

>>> Actions as amorphous chunks of code tossed here and there depending on
>>> scope is a way different ["anisotropic"] approach. In particular it does
>>> not fit into safe modular software design, because of this "anisotropy".
>>
>> What will type-object/module code look like if it is equivalent
>> to its nested analog?  Better?
>
> Analogue of what? The point is that "finally" cannot replace initialization
> and finalization of objects, specific or class-wide.


Could there be a workable design that lifts these two
events (entry, exit) to proper, programmable, abstractions
and how would they be connected to all of the language,
not just the types section?

By analog I meant this: The way a nested object goes out of
scope may influence objects in some less nested scope.
Then, is it (a) possible, (b) feasible, (c) good ROI
to design types that are interconnected to reflect all
possible effects between types, in the types?  Wouldn't this
design mix aspects of operation that should be kept in a different,
yet connected formalisms that makes explicit use of scopes?

As a simple example, I had been considering a relatively global
array or set shared between two procedures or tasks;
each proc/task would be responsible for part of the
elements in the shared data structure.  When one fails,
the the "exit action" is to "reset" its share of slots/
elements.  This sounds like one could design types that
do(!) just this as part of their finalization.  But it does
seem like an awful lot of overhead, and is essentially
a type that is-a procedure.  My question then is whether
or not this overhead is worth it, at least at this fairly
low level of small algorithm writing, not system design.

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Wed, 04 May 2011 10:48:14 +0200, Georg Bauhaus wrote:

> On 5/3/11 6:28 PM, Dmitry A. Kazakov wrote:
> 
>>>> Actions as amorphous chunks of code tossed here and there depending on
>>>> scope is a way different ["anisotropic"] approach. In particular it does
>>>> not fit into safe modular software design, because of this "anisotropy".
>>>
>>> What will type-object/module code look like if it is equivalent
>>> to its nested analog?  Better?
>>
>> Analogue of what? The point is that "finally" cannot replace initialization
>> and finalization of objects, specific or class-wide.
> 
> Could there be a workable design that lifts these two
> events (entry, exit) to proper, programmable, abstractions
> and how would they be connected to all of the language,
> not just the types section?

Yes, these are called constructor and destructor of the type. They are not
bound to any given scope, because:

1. the actions to perform are independent on the scopes;
2  a scope-bound design would mean distributed overhead, being fragile,
non-reusable, non-testable. [In the HI context it is especially bad.]

In its essence it is untyped, because a type meant to maintain its
properties independently on the number of instances and scopes of these
instances (nested to the type's scope of course).

> By analog I meant this: The way a nested object goes out of
> scope may influence objects in some less nested scope.

Which implies some links between objects, which itself is a model breach,
because it introduces references (access types, handles, mix-ins). Such
designs must be avoided in first place, as perpetually repeated in c.l.a.,
don't use pointers if you don't need to.

> Then, is it (a) possible, (b) feasible, (c) good ROI
> to design types that are interconnected to reflect all
> possible effects between types, in the types?  Wouldn't this
> design mix aspects of operation that should be kept in a different,
> yet connected formalisms that makes explicit use of scopes?
> 
> As a simple example, I had been considering a relatively global
> array or set shared between two procedures or tasks;
> each proc/task would be responsible for part of the
> elements in the shared data structure.  When one fails,
> the the "exit action" is to "reset" its share of slots/
> elements.

This does not read as a complete description. In what sense are the parts
of the array shared? If sharing means only independent use of the parts,
then what sense has the array as an object in this design? Independently
used parts must be local to their users. Now, if there is something else
behind this, i.e. that parts are sometimes used independently and sometimes
together, then too little is said about the mechanisms used for the latter,
and most intricate part of design.

> This sounds like one could design types that
> do(!) just this as part of their finalization.  But it does
> seem like an awful lot of overhead, and is essentially
> a type that is-a procedure.

You see that as an overhead only because the picture is incomplete. Once
you fill the gaps, you will see how "exit action" firs there. That would
definitely involve additional objects, e.g. controlled "handles" of which
finalization would deal with "exit" and other operations would serve
interlocking etc.

> My question then is whether
> or not this overhead is worth it, at least at this fairly
> low level of small algorithm writing, not system design.

See, low-level is what "finally" is.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Georg Bauhaus]

On 04.05.11 11:28, Dmitry A. Kazakov wrote:

> This does not read as a complete description. In what sense are the parts
> of the array shared? If sharing means only independent use of the parts,
> then what sense has the array as an object in this design? Independently
> used parts must be local to their users. Now, if there is something else
> behind this, i.e. that parts are sometimes used independently and sometimes
> together, then too little is said about the mechanisms used for the latter,
> and most intricate part of design.
> 
>> This sounds like one could design types that
>> do(!) just this as part of their finalization.  But it does
>> seem like an awful lot of overhead, and is essentially
>> a type that is-a procedure.
> 
> You see that as an overhead only because the picture is incomplete. Once
> you fill the gaps, you will see how "exit action" firs there. That would
> definitely involve additional objects, e.g. controlled "handles" of which
> finalization would deal with "exit" and other operations would serve
> interlocking etc.

A simple example (full source linked, but may not be
necessary); the intention is for it to be fairly low
level data manipulation.  It is not nice, and could be
generalized in several ways, I think.  If there is
justification for doing so.

Array `Central` is manipulated by two tasks A and B.
When these have finished filling `Central`, the env task
computes the final result by counting certain values in `Central`.
Communication uses simple variables and visibility.

The task B is sensitive to a special piece of input
and will restart its work from the beginning when
the input testing function raises Junk_Signal.

I imagine it is possible to redesign, yet I'd like to know
the ROI; the program is almost a Ravenscar program.
There are no pointers.


with Printing;

procedure Shared is

    -- ----------------------------------------------------------------
    --  Outline:
    --
    --  Two tasks will work on a shared array, each task taking care of
    --  its share of slots.  After they have finished, all slots will
    --  have valid values, some of which are interesting.  Count
    --  these.
    -- ----------------------------------------------------------------

    package Stuff is
	--
	--  Items that will be stored in the array.  Each component
	--  will be of type ID_Code.  No value means = No_Code.
	--
	type Digit_Position is range 1 .. 4;
	type Code_Digit is ('U', 'V', 'W', 'X', 'Y', 'Z');
	type ID_Code is array (Digit_Position) of Code_Digit;
	No_Code : constant ID_Code;
	
	function Image (Id : Id_Code) return String;
	
	type Slot_Index is range 1 .. 1023;
	type Work_Item is array (Slot_Index) of ID_Code;
	--  type of the shared array
	
	function Is_Filled (W : Work_Item) return Boolean;
	procedure Init (W : in out Work_Item);
	
	function Interesting_Result (W : Work_Item) return Natural;
	--  number of interesting ID_Code values in `W` (likely `Central`)
	
    private
	No_Code : constant ID_Code := ID_Code'('X', 'X', 'X', 'X');
    end Stuff;

    package body Stuff is separate;

    use Stuff;

    Central : Work_Item;
    Result : Natural := Natural(Slot_Index'Last) + 1;
    --  also used as flag. Set `Result := 0` when the tasks may start
    --  doing their work
    pragma Atomic(Result);

    package Slaves is
	--  Each task will work with its share of slots in `Central`.
	--  A and B try hard to find good ID_Code values from some
	--  external source, B tries especially hard.
	task A;
	task B;
    end Slaves;

    package body Slaves is separate;
		
begin
    Init (Central);
    pragma Assert (not Is_Filled (Central));
    Result := 0;
    -- now poll until A and B have filled Central
    loop
	exit when Is_Filled (Central);
	delay 0.2;
    end loop;
    Result := Interesting_Result(Central);
    Printing.Output.Write  (Natural'Image(Result)
			      & " interesting items",
			    NL => True);
end Shared;

Rest is here:
http://home.arcor.de/bauhaus/Ada/shrd.ada

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Wed, 04 May 2011 16:46:21 +0200, Georg Bauhaus wrote:

> On 04.05.11 11:28, Dmitry A. Kazakov wrote:
> 
>> This does not read as a complete description. In what sense are the parts
>> of the array shared? If sharing means only independent use of the parts,
>> then what sense has the array as an object in this design? Independently
>> used parts must be local to their users. Now, if there is something else
>> behind this, i.e. that parts are sometimes used independently and sometimes
>> together, then too little is said about the mechanisms used for the latter,
>> and most intricate part of design.
>> 
>>> This sounds like one could design types that
>>> do(!) just this as part of their finalization.  But it does
>>> seem like an awful lot of overhead, and is essentially
>>> a type that is-a procedure.
>> 
>> You see that as an overhead only because the picture is incomplete. Once
>> you fill the gaps, you will see how "exit action" firs there. That would
>> definitely involve additional objects, e.g. controlled "handles" of which
>> finalization would deal with "exit" and other operations would serve
>> interlocking etc.
> 
> A simple example (full source linked, but may not be
> necessary); the intention is for it to be fairly low
> level data manipulation.  It is not nice, and could be
> generalized in several ways, I think.  If there is
> justification for doing so.
> 
> Array `Central` is manipulated by two tasks A and B.
> When these have finished filling `Central`, the env task
> computes the final result by counting certain values in `Central`.
> Communication uses simple variables and visibility.
> 
> The task B is sensitive to a special piece of input
> and will restart its work from the beginning when
> the input testing function raises Junk_Signal.

This looks like the "checkpoint synchronization problem".

   http://rosettacode.org/wiki/Checkpoint_synchronization

I would use a protected object to implement an array of events and
distributing jobs among the worker tasks when they join or leave. I would
likely place the array there. I would avoid polling.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Georg Bauhaus]

On 04.05.11 17:01, Dmitry A. Kazakov wrote:

> This looks like the "checkpoint synchronization problem".

That's part of it.

>    http://rosettacode.org/wiki/Checkpoint_synchronization

Try adding pragma Profile (Ravenscar) there ;.)

> I would use a protected object to implement an array of events and
> distributing jobs among the worker tasks when they join or leave. I would
> likely place the array there. I would avoid polling.

The idea is to have two very busy tasks share an array
as efficiently as possible.

I'm trying to weigh all effects of rewriting the following
nest using the type-ized formalism that you have mentioned.

 procedure A is
   X : T;

   procedure B_Opt is
     type T1 is ...;
     Y : T1;
   begin
     Op(X, V);
     Op(Y, V);
   exception
     when ... =>
       Restore(X);  --?
       --  Y cleans up after itself
   end B_Opt;

 begin
   B_Opt;
   Op(X);
 end A;

Is there really little overhead when Restore is replaced
with some objects?

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Wed, 04 May 2011 17:25:43 +0200, Georg Bauhaus wrote:

> On 04.05.11 17:01, Dmitry A. Kazakov wrote:
> 
>> This looks like the "checkpoint synchronization problem".
> 
> That's part of it.
> 
>>    http://rosettacode.org/wiki/Checkpoint_synchronization
> 
> Try adding pragma Profile (Ravenscar) there ;.)

I don't care much about Ravenscar, which is too limiting for almost
anything. There are limitations to make life easier for the readers and
ones for the compiler and prover. They are not same, some contradict to the
goals of each other. I always choose the former over the latter.

> Is there really little overhead when Restore is replaced
> with some objects?

[...]

Negligible since used upon an exception, which I hope is not to propagate
at 100ns rate.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Georg Bauhaus]

On 04.05.11 18:23, Dmitry A. Kazakov wrote:

>> Try adding pragma Profile (Ravenscar) there ;.)
> 
> I don't care much about Ravenscar, which is too limiting for almost
> anything. There are limitations to make life easier for the readers and
> ones for the compiler and prover. They are not same, some contradict to the
> goals of each other. I always choose the former over the latter.

Does it work when systems need to be fast at the lower levels?

>> Is there really little overhead when Restore is replaced
>> with some objects?
> 
> [...]
> 
> Negligible since used upon an exception, which I hope is not to propagate
> at 100ns rate.

Ah, o.K., I should have said source code maintenance overhead, too,
and increased system complexity.  The program now uses nesting, a language
feature. In order to go with types for the same effects, it will have to be
transformed. To replace the Restore procedure, the transformation
would have to add not just objects but also "indirections" that
make up for the effects.  I think that what you said earlier?
If this is the case, then I wonder whether or not this kind of
overhead is worth the effort.

All of this does not address the issue of how to hook "nested rollback".

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Wed, 04 May 2011 19:06:55 +0200, Georg Bauhaus wrote:

> On 04.05.11 18:23, Dmitry A. Kazakov wrote:
> 
>>> Try adding pragma Profile (Ravenscar) there ;.)
>> 
>> I don't care much about Ravenscar, which is too limiting for almost
>> anything. There are limitations to make life easier for the readers and
>> ones for the compiler and prover. They are not same, some contradict to the
>> goals of each other. I always choose the former over the latter.
> 
> Does it work when systems need to be fast at the lower levels?

Performance optimization is a different angle. There is no obvious reason
why following or ignoring Ravenscar's restrictions should result in either
faster or slower program.

The problem with Ravenscar is that in my case it unfortunately does not let
me fulfill the functional requirements I have. Under such circumstances
non-functional niceties play no role. I am not sure if the problem is
fundamental, i.e. no conformant program exists. Even if it did I could not
design or understand it anyway...

>>> Is there really little overhead when Restore is replaced
>>> with some objects?
>> 
>> [...]
>> 
>> Negligible since used upon an exception, which I hope is not to propagate
>> at 100ns rate.
> 
> Ah, o.K., I should have said source code maintenance overhead, too,
> and increased system complexity.

Developing /= maintenance.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: High-Integrity OO and controlled types

[Maciej Sobczak]

On May 4, 10:16 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:

> Performance optimization is a different angle. There is no obvious reason
> why following or ignoring Ravenscar's restrictions should result in either
> faster or slower program.

For one thing, with Ravenscar restrictions the compiler need not
generate abort deferral related code, because without ATC it would be
a dead code anyway. This might reduce the size of generated code and
consequently make it faster.
I have no hard data on what are the actual gains, however.

There are certainly other opportunities as well.

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

Re: High-Integrity OO and controlled types

[Cyrille]

On May 5, 9:13 am, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
> On May 4, 10:16 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>
> > Performance optimization is a different angle. There is no obvious reason
> > why following or ignoring Ravenscar's restrictions should result in either
> > faster or slower program.
>
> For one thing, with Ravenscar restrictions the compiler need not
> generate abort deferral related code, because without ATC it would be
> a dead code anyway. This might reduce the size of generated code and
> consequently make it faster.
> I have no hard data on what are the actual gains, however.

not mentioning that the ravenscar profile has been designed, among
other things, to allow ultra-efficient tasking runtimes (compared to
those having to support all of the Ada tasking model). For instance,
assuming a single core config, one can implement protect objects
without any locking mechanism... and such implementations exist in
several Ada technologies as far as I know...

Re: High-Integrity OO and controlled types

[Dmitry A. Kazakov]

On Thu, 5 May 2011 03:58:26 -0700 (PDT), Cyrille wrote:

> For instance,
> assuming a single core config, one can implement protect objects
> without any locking mechanism... and such implementations exist in
> several Ada technologies as far as I know...

It is difficult to find single cores in these days. Recently we had certain
problems caused by multiple core issues. But we could not find a single
core machine. So we had to fix our software... (:-))

I agree that tasking could be more efficient, but working around
Ravenscar's limitations (on entries, for example) might eat all that gain.
It is not obvious.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de