Is there a reason System.Storage_Pools isn't Pure?

Is there a reason System.Storage_Pools isn't Pure?

[Shark8]

Looking at the specification for System.Storage_Pools [RM 13.11(5)] there doesn't seem to be anything that requires the Preelaborate pragma... is there any real reason that it wasn't made a Pure unit?

Re: Is there a reason System.Storage_Pools isn't Pure?

[Randy Brukardt]

Originally, it was not Pure because it was a child of System, which was not 
Pure. So I can't find any discussion of the merits.

However, Pure packages are automatically Remote_Types packages (that is, 
values of the type can be transmitted between partitions). We'd never want 
that to be the case with a storage pool, so there doesn't seem to be any 
point in it being Pure.

Additionally, the Pure package rules assume that no storage pools can be 
specified for access types (because there aren't rules banning that at 
library-level, and there need to be such rules to prevent hidden state). 
That could be changed, I suppose, but given that a Pure storage pool could 
only be used for a local access type in a Pure package(something that mainly 
exists in ACATS tests), it would be close to useless (or get used for 
back-door state). Note that state has to be strictly prohibited as Pure 
packages are replicated when used in a distributed system (thus each 
partition would have different state, which wouldn't make sense).

IMHO, Pure packages are too restricted to be useful (and not restricted 
enough to be useful when synchronization is involved); it makes sense for 
individual subprograms but not for an entire package. So I recommend only 
trying to make packages Preelaborated. (That's especially true in Ada 2012, 
where limited I/O is possible.) [Distribution might change this thinking; 
I'm only considering stand-alone programs that don't use Annex E.]

                                  Randy.

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:178b6fbc-229b-49fc-8ffb-a5797bfc335f@googlegroups.com...
> Looking at the specification for System.Storage_Pools [RM 13.11(5)] there 
> doesn't seem to be anything that requires the Preelaborate pragma... is 
> there any real reason that it wasn't made a Pure unit? 

Re: Is there a reason System.Storage_Pools isn't Pure?

[Shark8]

On Tuesday, April 18, 2017 at 12:32:34 PM UTC-6, Randy Brukardt wrote:
> Originally, it was not Pure because it was a child of System, which was not 
> Pure. So I can't find any discussion of the merits.
> 
> However, Pure packages are automatically Remote_Types packages (that is, 
> values of the type can be transmitted between partitions). We'd never want 
> that to be the case with a storage pool, so there doesn't seem to be any 
> point in it being Pure.

Are we sure we'd never want that?
I imagine that would be an interesting way to do VMs -- essentially transmitting the [contained] memory directly between partitions, right? -- so we could essentially solve the problems plaguing JavaScript/backend development (in theory) with this, right?


> Additionally, the Pure package rules assume that no storage pools can be 
> specified for access types (because there aren't rules banning that at 
> library-level, and there need to be such rules to prevent hidden state). 
> That could be changed, I suppose, but given that a Pure storage pool could 
> only be used for a local access type in a Pure package(something that mainly 
> exists in ACATS tests), it would be close to useless (or get used for 
> back-door state). Note that state has to be strictly prohibited as Pure 
> packages are replicated when used in a distributed system (thus each 
> partition would have different state, which wouldn't make sense).

What about a usable-for-anything holder? (In particular, I think that Ada.Containers.Indefinite_Holders ought to be less restrictive than they are.) We could have a Pure Indefinite_Holder with:

    Generic
      Type Element_Type(<>) is limited private;
      -- Pure storage-pool as a parameter? a dependency?
    Package Example with Pure, Spark_Mode => On is
      Type Holder is private;
      Function Has_Element( Container : Holder ) return Boolean;
      Function Element( Container : Holder ) return Element_Type
        with Pre => Has_Element( Container );
      Procedure Clear( Container : in out Holder )
        with Post => not Has_Element( Container );
    Private
      Pragma SPARK_Mode( Off );
      
      Type is access Element_Type
        with Storage_Size => 0; -- Pure pool storage to allow non-zero?
      
      Function Has_Element( Container : Holder ) return Boolean is
        (Container /= Null);
      Function Has_Element( Container : Holder ) return Boolean is
        (Container.All);
    End Example;

Or am I misunderstanding?

> IMHO, Pure packages are too restricted to be useful (and not restricted 
> enough to be useful when synchronization is involved); it makes sense for 
> individual subprograms but not for an entire package. So I recommend only 
> trying to make packages Preelaborated. (That's especially true in Ada 2012, 
> where limited I/O is possible.) [Distribution might change this thinking; 
> I'm only considering stand-alone programs that don't use Annex E.]

That's probably truer than I'd like -- but I guess the question was borne out of playing around w/ pure units and seeing how far I could push the style-guide's instruction "Use pragma Pure where allowed."
( https://en.wikibooks.org/wiki/Ada_Style_Guide/Print_version#Pragma_Pure )

Re: Is there a reason System.Storage_Pools isn't Pure?

[Dmitry A. Kazakov]

On 19/04/2017 01:42, Shark8 wrote:
> On Tuesday, April 18, 2017 at 12:32:34 PM UTC-6, Randy Brukardt wrote:
>> Originally, it was not Pure because it was a child of System, which was not
>> Pure. So I can't find any discussion of the merits.
>>
>> However, Pure packages are automatically Remote_Types packages (that is,
>> values of the type can be transmitted between partitions). We'd never want
>> that to be the case with a storage pool, so there doesn't seem to be any
>> point in it being Pure.
>
> Are we sure we'd never want that?
> I imagine that would be an interesting way to do VMs -- essentially
> transmitting the [contained] memory directly between partitions, right?

No, so long you don't know what is in the memory. Even considering the 
case of a shared [distributed] memory pool it cannot be pure. E.g. 
initialization of an object in the shared memory must be done only once, 
which does not preclude binding of each shared copy/view, like mapping 
pointers since copies may be located in different virtual address spaces.

> What about a usable-for-anything holder?

Huh, what about fixing initialization/fixed in the first place. We would 
not need kludges like holders if any type could have proper constructor 
and destructor, access types included.

>> IMHO, Pure packages are too restricted to be useful (and not restricted
>> enough to be useful when synchronization is involved); it makes sense for
>> individual subprograms but not for an entire package. So I recommend only
>> trying to make packages Preelaborated. (That's especially true in Ada 2012,
>> where limited I/O is possible.) [Distribution might change this thinking;
>> I'm only considering stand-alone programs that don't use Annex E.]
>
> That's probably truer than I'd like -- but I guess the question was
> borne out of playing around w/ pure units and seeing how far I could
> push the style-guide's instruction "Use pragma Pure where allowed."

A lot of use cases conflated into single pragma Pure:

1. Value/object identity
2. Elaboration
3. Early evaluation (e.g. compile time, elaboration time)

It must be reworked from the start, IMO.

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

Re: Is there a reason System.Storage_Pools isn't Pure?

[Shark8]

On Wednesday, April 19, 2017 at 1:37:33 AM UTC-6, Dmitry A. Kazakov wrote:
> On 19/04/2017 01:42, Shark8 wrote:
> > On Tuesday, April 18, 2017 at 12:32:34 PM UTC-6, Randy Brukardt wrote:
> >> Originally, it was not Pure because it was a child of System, which was not
> >> Pure. So I can't find any discussion of the merits.
> >>
> >> However, Pure packages are automatically Remote_Types packages (that is,
> >> values of the type can be transmitted between partitions). We'd never want
> >> that to be the case with a storage pool, so there doesn't seem to be any
> >> point in it being Pure.
> >
> > Are we sure we'd never want that?
> > I imagine that would be an interesting way to do VMs -- essentially
> > transmitting the [contained] memory directly between partitions, right?
> 
> No, so long you don't know what is in the memory. Even considering the 
> case of a shared [distributed] memory pool it cannot be pure.

But of course you know what's in that memory: you put it there. [Well, the compiler; and since accesses are typed of course we know what they are.] -- And a pool[-type] obviously can be pure, as it is only a definition, an interface, if you will.

> E.g. 
> initialization of an object in the shared memory must be done only once, 
> which does not preclude binding of each shared copy/view, like mapping 
> pointers since copies may be located in different virtual address spaces.

Huh?
While 'pointer' and 'access' are forms of indirection, and conceptually the same an access is safer as there is no untyped access. Further, if we use the de facto standard that pointers are an integer (thanks C [/sarc]) then we can recognize that an access needn't be so restricted. Indeed there are cases where it *MUST* be more than an integer, like the case of an access to the value of an unconstrained array-type,as we *MUST* have the bounds.


> > What about a usable-for-anything holder?
> 
> Huh, what about fixing initialization/fixed in the first place. We would 
> not need kludges like holders if any type could have proper constructor 
> and destructor, access types included.

Perhaps, though maybe you should explain what a proper constructor/destructor is -- as I'm pretty sure that C++ style *isn't* what you have in mind.

> >> IMHO, Pure packages are too restricted to be useful (and not restricted
> >> enough to be useful when synchronization is involved); it makes sense for
> >> individual subprograms but not for an entire package. So I recommend only
> >> trying to make packages Preelaborated. (That's especially true in Ada 2012,
> >> where limited I/O is possible.) [Distribution might change this thinking;
> >> I'm only considering stand-alone programs that don't use Annex E.]
> >
> > That's probably truer than I'd like -- but I guess the question was
> > borne out of playing around w/ pure units and seeing how far I could
> > push the style-guide's instruction "Use pragma Pure where allowed."
> 
> A lot of use cases conflated into single pragma Pure:
> 
> 1. Value/object identity
> 2. Elaboration
> 3. Early evaluation (e.g. compile time, elaboration time)

1. Value/object identity? I'm not sure where you're getting that from., could you elaborate/explain?

3. This is true; it would be nice to have a clear compile-time and elaboration-time distinction.

> It must be reworked from the start, IMO.

Perhaps, though it does quite well in enforcing a lack of state upon the compilation-unit; taken in that manner Pure does a good job as an indicator.

Re: Is there a reason System.Storage_Pools isn't Pure?

[Dmitry A. Kazakov]

On 2017-04-19 20:50, Shark8 wrote:
> On Wednesday, April 19, 2017 at 1:37:33 AM UTC-6, Dmitry A. Kazakov wrote:

>> No, so long you don't know what is in the memory. Even considering the
>> case of a shared [distributed] memory pool it cannot be pure.
>
> But of course you know what's in that memory: you put it there.
> [Well,  the compiler; and since accesses are typed of course we know what they
> are.] -- And a pool[-type] obviously can be pure, as it is only a
> definition, an interface, if you will.

OK, theoretically a pool type can be static. But instances cannot be, so 
it is not much use anyway.

>> E.g.
>> initialization of an object in the shared memory must be done only once,
>> which does not preclude binding of each shared copy/view, like mapping
>> pointers since copies may be located in different virtual address spaces.
>
> Huh?
> While 'pointer' and 'access' are forms of indirection, and
> conceptually the same an access is safer as there is no untyped access.
> Further, if we use the de facto standard that pointers are an integer
> (thanks C [/sarc]) then we can recognize that an access needn't be so
> restricted. Indeed there are cases where it *MUST* be more than an
> integer, like the case of an access to the value of an unconstrained
> array-type,as we *MUST* have the bounds.

I meant that you must relocate access types pointing inside the 
shared/distributed memory. It is no different to load-time relocation of 
shared libraries.

>>> What about a usable-for-anything holder?
>>
>> Huh, what about fixing initialization/fixed in the first place. We would
>> not need kludges like holders if any type could have proper constructor
>> and destructor, access types included.
>
> Perhaps, though maybe you should explain what a proper
> constructor/destructor is -- as I'm pretty sure that C++ style *isn't*
> what you have in mind.

In fact I do. C++ has constructors almost right. Ada has nothing but an 
ugly Ada.Finalization hack.

A user-defined constructor is an anonymous subroutine hooked at a 
definite stage of object's initialization. It cannot be called 
explicitly. It cannot be overridden. It is not a primitive operation. It 
can be safely rolled back on exception propagation.

> 1. Value/object identity? I'm not sure where you're getting that
> from., could you elaborate/explain?

There are things with and without identity. E.g. integer value has no 
identity. A task type value has. Stateful objects you refer below 
require identity, obviously. In "X has state S" X is the identity.

> 3. This is true; it would be nice to have a clear compile-time and
> elaboration-time distinction.
>
>> It must be reworked from the start, IMO.
>
> Perhaps, though it does quite well in enforcing a lack of state upon
> the compilation-unit; taken in that manner Pure does a good job as an
> indicator.

You mean immutability. Consider a generic unit parametrized by a 
constant value declaring things dependent on the constant. It has 
instances in different states which are pure (not in Ada sense AFAIK) 
but in the sense of being immutable.

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

Re: Is there a reason System.Storage_Pools isn't Pure?

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:od743q$p4n$1@gioia.aioe.org...
...
> A lot of use cases conflated into single pragma Pure:
>
> 1. Value/object identity
> 2. Elaboration
> 3. Early evaluation (e.g. compile time, elaboration time)
>
> It must be reworked from the start, IMO.

More like abandoned. Our current thinking is to essentially replace it by 
specifications of the Global aspect (which is stricter, so the result can be 
usefully used in parallelism applications) and finer grained (so individual 
subprograms can each have appropriate settings, no more "everything in the 
package has to be the same").

That would leave the only real purposes of Pure to be distribution and 
elaboration; the former uses don't want access types at all, and the latter 
can be handled just using Preelaborate does the job. (Ergo: most of what was 
done to Pure in Ada 2005 was a mistake, an attempt to fix the muddled mess 
resulting in a bigger muddled mess.)

                                       Randy.

Re: Is there a reason System.Storage_Pools isn't Pure?

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:61e151c1-9fe6-4d32-8f13-d425bc41a616@googlegroups.com...
...
> What about a usable-for-anything holder? (In particular, I think that 
> Ada.Containers.Indefinite_Holders ought to be less restrictive than they 
> are.) We could have a Pure Indefinite_Holder with:
>
>    Generic
>      Type Element_Type(<>) is limited private;
>      -- Pure storage-pool as a parameter? a dependency?
>    Package Example with Pure, Spark_Mode => On is
>      Type Holder is private;
>      Function Has_Element( Container : Holder ) return Boolean;
>      Function Element( Container : Holder ) return Element_Type
>        with Pre => Has_Element( Container );
>      Procedure Clear( Container : in out Holder )
>        with Post => not Has_Element( Container );
>    Private
>      Pragma SPARK_Mode( Off );
>
>      Type is access Element_Type
>        with Storage_Size => 0; -- Pure pool storage to allow non-zero?
>
>      Function Has_Element( Container : Holder ) return Boolean is
>        (Container /= Null);
>      Function Has_Element( Container : Holder ) return Boolean is
>        (Container.All);
>    End Example;
>
> Or am I misunderstanding?

Your spec here doesn't have any way to put an element into the holder. And 
that's where the trouble comes (especially for limited types!). Perhaps you 
can figure it out (I haven't been able to). As it stands, your holder 
objects would have to have Has_Element = False. Not very useful. ;-)

                              Randy.
 

Re: Is there a reason System.Storage_Pools isn't Pure?

[Shark8]

On Wednesday, April 19, 2017 at 2:36:28 PM UTC-6, Randy Brukardt wrote:
> 
> Your spec here doesn't have any way to put an element into the holder. And 
> that's where the trouble comes (especially for limited types!). Perhaps you 
> can figure it out (I haven't been able to). As it stands, your holder 
> objects would have to have Has_Element = False. Not very useful. ;-)
> 
>                               Randy.

I should have known better than to type it on-the-fly.
Here's a different spec that actually does compile under GNAT, even though [AFACT] it shouldn't:

Pragma Ada_2012;
Pragma Assertion_Policy( Check );
Pragma SPARK_Mode( On );

Generic
    Type Element_Type(<>) is limited private;
Package Forth.Pure_Types.Pure_Holders with Pure, SPARK_Mode => On is
    Pragma Pure(Forth.Pure_Types.Pure_Holders);

    Type Holder is private;

    Function Has_Element (Container : Holder) return Boolean
      with Inline;

    Procedure Clear (Container : in out Holder)
      with Inline;

    Function Element (Container : Holder) return Element_Type
      with Inline,
	Pre     => Has_Element(Container)
		   or else raise Constraint_Error with "Container is empty.";

    Function To_Holder (Item : Element_Type) return Holder
      with Inline,
	Post    => Has_Element(To_Holder'Result);

    Procedure Replace_Element(Container : in out Holder; Item : Element_Type)
      with Inline;


Private
--      Pragma SPARK_Mode( OFF );

    Type Holder is access all Element_Type;
--      with Storage_Size => 0;

End Forth.Pure_Types.Pure_Holders;

---------------------------------------------------------------

Pragma Ada_2012;
Pragma Assertion_Policy( Check );

Package Body Forth.Pure_Types.Pure_Holders is

    Function Has_Element (Container : Holder) return Boolean is
      (Container /= Null);

    Procedure Clear (Container : in out Holder) is
	Procedure Unchecked_Deallocation(X : in out Holder)
	  with Import, Convention => Intrinsic;
    Begin
	Unchecked_Deallocation( Container );
    End Clear;

    Function Element (Container : Holder) return Element_Type is
      ( Container.All );

    Function To_Holder (Item : Element_Type) return Holder is
      ( New Element_Type'(Item) );

    Procedure Replace_Element(Container : in out Holder; Item : Element_Type) is
    Begin
	Clear( Container );
	Container:= To_Holder( Item );
    End Replace_Element;

End Forth.Pure_Types.Pure_Holders;

--------------

I've already got a Pure version of Storage_Pools (and Subpools) compiling too. (!) -- Of course I can't use an instance of them in a pure unit



----------------

Pragma Ada_2012;
Pragma Assertion_Policy( Check );

With
System.Storage_Pools;

Generic
    Type K(<>) is limited private;
    Pool : in out System.Storage_Pools.Root_Storage_Pool'Class;
Package Pool_Test with Pure is
    
    Type J is access all K
      with Storage_Pool => Pool;
    
End Pool_Test;

Re: Is there a reason System.Storage_Pools isn't Pure?

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:a498c0f6-11ae-4050-ade0-bc35c686dc1c@googlegroups.com...
> On Wednesday, April 19, 2017 at 2:36:28 PM UTC-6, Randy Brukardt wrote:
>>
>> Your spec here doesn't have any way to put an element into the holder. 
>> And
>> that's where the trouble comes (especially for limited types!). Perhaps 
>> you
>> can figure it out (I haven't been able to). As it stands, your holder
>> objects would have to have Has_Element = False. Not very useful. ;-)
>
> I should have known better than to type it on-the-fly.
> Here's a different spec that actually does compile under GNAT, even though 
> [AFACT] it shouldn't:

Right; it contains an assignment of a limited private type, which is, ummm, 
surprising. :-)

You probably could use a constructor allocator to do that in limited (pun 
not intended) cases, but that would be a new object which couldn't exist 
outside of the container. Might be useful in some cases...

                       Randy.

Re: Is there a reason System.Storage_Pools isn't Pure?

[Shark8]

On Friday, April 21, 2017 at 11:02:52 PM UTC-6, Randy Brukardt wrote:
> "Shark8" wrote in message 
> news:a498c0f6-11ae-4050-ade0-bc35c686dc1c...
> > On Wednesday, April 19, 2017 at 2:36:28 PM UTC-6, Randy Brukardt wrote:
> >>
> >> Your spec here doesn't have any way to put an element into the holder. 
> >> And
> >> that's where the trouble comes (especially for limited types!). Perhaps 
> >> you
> >> can figure it out (I haven't been able to). As it stands, your holder
> >> objects would have to have Has_Element = False. Not very useful. ;-)
> >
> > I should have known better than to type it on-the-fly.
> > Here's a different spec that actually does compile under GNAT, even though 
> > [AFACT] it shouldn't:
> 
> Right; it contains an assignment of a limited private type, which is, ummm, 
> surprising. :-)

For Replace_Element?
There's no assignment of a limited private type there, it's an assignment replacing the whole parameter "container", which is in this case an access type.
(Or do you mean in To_Holder?)

> 
> You probably could use a constructor allocator to do that in limited (pun 
> not intended) cases, but that would be a new object which couldn't exist 
> outside of the container. Might be useful in some cases...

Sounds like a good way to (e.g.) bind a value to a particular storage [sub]pool, IIUC.