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

[Shark8 <onewingedshark@gmail.com>]

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 )