Memory management

[treiher]

Context and Problem Statement

The implementation of the session support uses dynamically allocated memory for multiple use cases:

• Declarations of message and sequence variables (global and local)
• Copies of sequences (workaround for limitations of our sequence implementation; cf. O1 in SPARK sequences in protocol sessions #577)

A session specification does (and should) not include the maximum buffer sizes for the allocated message. Currently we assume a buffer of 4KiB for every message. As users obviously need more control, the buffer sizes should be configurable at integration time.

Considered Options

O1 Memory allocator in runtime

+ Simple, generic solution
− Not suitable for certain use cases (e.g., embedded systems)

O2 Application-specific allocator

An application-specific allocator is used on static memory. The allocator could be quite simple and only allow the deallocation of the last allocated memory (stack allocator).

The size of each buffer should be configurable through a generic parameter of the session package. To lower the burden of an instantiation a default value for this parameter should be set depending on a RecordFlux command line parameter.

+ Proving maximum memory consumption by contracts
− Complexity moved into application

O3 Stack memory

+ Simple
− Pointers to stack not supported by SPARK
− Needs additional analysis to prevent stack overflows

Decision Outcome

O2 Implement package with hidden body to allocate memory (idea: ghost stack for pointers, stack-like allocation).

---

Original Issue

Ada.Unchecked_Deallocation is not supported in the Ada runtime, but required for session support (#292).

$ gprbuild -Ptest --RTS=ada-runtime/build/posix/obj -Xaunit=no -Xoptimization=yes
Setup
   [mkdir]        object directory for project Test
Compile
   [Ada]          rflx-udp.ads
   [Ada]          rflx-arrays-inner_message.ads
rflx-arrays-inner_message.ads:4:06: "ADA.UNCHECKED_DEALLOCATION" is not a predefined library unit

[jklmnn]

I would assume that we need new then, too?

[treiher]

Yes, new is also required.

[senier]

Where do we allocate/deallocate in the sessions?

[treiher]

Allocations are used for declarations of message and sequence variables. The memory is deallocated when the scope of such a variable is left. Allocation and deallocation is also used to create copies of sequences. These copies are required to workaround the limitations of our sequence implementation (cf. O1 in #577).

[jklmnn]

For the record: the solution proposed by Yannick for getting general access to package level variables is described in SB28-034.

[kanigsson]

Here is a short summary of my current thought process.

I believe an actual allocator (a subprogram that returns a part of a pre-allocated big chunk in memory) would not be possible to implement in SPARK, due to aliasing rules (one cannot split ownership of an object in several pieces). Also, it would be needlessly complicated.

My current target design simply creates as many global variables as are needed (possible simplification for a first implementation: as many global variables as there are variables in the session). A pointer is then created to one of those variables and used as before.

The idea that I presented in the last meeting was to use general access types (which are allowed to point to global variables and stack variables) instead of regular access types (which are only allowed to point to the heap). However, general access types are pretty restrictive in SPARK (I missed that initially). As soon as you create a pointer to a stack or global variable, that variable is considered moved and there is no way to move it back.

So there seems to be no way to have code fully in SPARK. So the refined idea is to create the pointer outside of the SPARK boundary. Something like that:

memory.adb:

package Memory with SPARK_Mode is

   Slot_1 : Bytes := (0 .. 4095 => 0);
   Slot_2 : Bytes := (0 .. 4095 => 0);
   ...

   function Get_Slot_1 return Bytes_Ptr with SPARK_Mode => Off
   is 
   begin 
       return Slot_1'Access;
   end Get_Slot_1;
  
  ... same for Get_Slot_2 ...
end Memory;

The spec of that package just contains the specification for Get_Slot_1. Instead of an allocation, the code would just call one of the Get_Slot_NN functions to get the corresponding pointer.

The current Bytes_Ptr type could be changed to a general access type (with access all) to forbid deallocation. This seems to have no other drawback.

One issue with the design is that there is no protection against taking the same memory twice. If code is generated that incorrectly reuses a Slot while it should take a new one, there is no protection for that.

Any comments on that design? I will attempt to implement something like that in the following days.

[treiher]

The overall approach looks good to me. I suppose the proposed approach is also compatible to Community 2021, as access all is not strictly needed?

One issue with the design is that there is no protection against taking the same memory twice. If code is generated that incorrectly reuses a Slot while it should take a new one, there is no protection for that.

That sounds quite risky. If there is no way to ensure that property with SPARK when using the proposed approach, we should at least make it possible to extensively test the correctness of the affected code. Would it be possible to encapsulate the affected code, e.g. by making the allocator a separate generic package which is just used by the generated code? Or do you see any other alternatives?

[senier]

Could we make a single Get_Slot function which receives and array of slots (for which we prove they are disjoint) and which returns and array of pointers?

[kanigsson]

Indeed this newer design should work with SPARK Community.

@senier I think that could work. The idea is that the client code would know that it uses the same memory for different purposes, because it accesses the array of slots directly, right? Though it might add some extra overhead for proof, which has to go through the array all the time. Not sure.

Another idea is to have a single Get_Slot function, and it is up to the Memory package to make sure it returns a new slot. It would fail at runtime if it doesn't have any slots left (could imagine proving absence of RTE I guess) . This scheme would require some release mechanism so that slots can be reused.

[senier]

The memory slots would not be used from user code (at least not in our definition of if ;)) but rather in the code generated for the sessions. Take the DHCP example:

   procedure Send_Discover (State : out Session_State) with                                                             
     Pre =>                                                                                                             
       Initialized,                                                                                                     
     Post =>                                                                                                            
       Initialized                                                                                                      
   is                                                                                                                   
      Options_Ctx : DHCP.Options.Context;                                                                               
      Parameter_Request_List_Ctx : DHCP.Option_Codes.Context;                                                           
      Options_Buffer : RFLX_Types.Bytes_Ptr;                                                                            
      Parameter_Request_List_Buffer : RFLX_Types.Bytes_Ptr;                                                             
   begin                                                                                                                
      Options_Buffer := new RFLX_Types.Bytes'(RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
      DHCP.Options.Initialize (Options_Ctx, Options_Buffer);                                                            
      Parameter_Request_List_Buffer := new RFLX_Types.Bytes'(RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
      DHCP.Option_Codes.Initialize (Parameter_Request_List_Ctx, Parameter_Request_List_Buffer);
      ... -- do stuff
   end Send_Discover;

This would translate into:

   procedure Send_Discover (State : out Session_State) with                                                             
     Pre =>                                                                                                             
       Initialized,                                                                                                     
     Post =>                                                                                                            
       Initialized                                                                                                      
   is                                                                                                                   
      Options_Ctx : DHCP.Options.Context;                                                                               
      Parameter_Request_List_Ctx : DHCP.Option_Codes.Context;
      Buffers : RFLX_Types.Bytes_Ptr_Array := Get_Slots ((1, 7));  --  Bytes_Ptr_Array would be an unconstrained array of Bytes_Ptr. The precondition on Get_Slots states that all array elements are distinct    
   begin                                                                                                                
      DHCP.Options.Initialize (Options_Ctx, Buffers (1));                                                            
      DHCP.Option_Codes.Initialize (Parameter_Request_List_Ctx, Buffers (2));
      ... -- do stuff
   end Send_Discover;

Would that work? The precondition on Get_Slots would avoid requesting the same region twice, borrow checking on the Buffers array should avoid aliasing locally (but that's that part I'm unsure about!).

[kanigsson]

After thinking about it (and trying it out), putting all the pointers in a common array wouldn't work. SPARK borrow checker can't distinguish between the pointers and treats them basically as the same pointer, so you can't use two of them at the same time. I will explore my other idea of the Get_Slot function that always returns a new slot.

[kanigsson]

Here is my new attempt. The allocator (it would actually look like one now) interface is like this (memory.ads):

with Types; use Types;
package Memory with SPARK_Mode, Abstract_State => State is

   Num_Slots : constant := 4;
   type Slot_Range is range 0 .. Num_Slots;

   function Free_Slots return Slot_Range with Ghost;

   procedure Alloc (Ptr : out Byte_Array_Access)
   with Global => (In_Out => State),
        Pre    => Free_Slots /= 0,
        Post   => Free_Slots = Free_Slots'Old - 1 and then Ptr /= null and then Ptr'Length = 1024; 

   procedure Pop
   with Global => (In_Out => State),
        Pre    => Free_Slots /= Num_Slots,
        Post   => Free_Slots = Free_Slots'Old + 1; 

   procedure Init
   with Global => (In_Out => State),
        Post   => Free_Slots = Num_Slots;

end Memory;

and the implementation like this:

package body Memory
with SPARK_Mode,
     Refined_State => (State => (Top_Ptr, Slot_0, Slot_1, Slot_2, Slot_3))
is

   Slot_0 : aliased Byte_Array := (1 .. 1024 => 1);
   Slot_1 : aliased Byte_Array := (1 .. 1024 => 2);
   Slot_2 : aliased Byte_Array := (1 .. 1024 => 2);
   Slot_3 : aliased Byte_Array := (1 .. 1024 => 2);

   Top_Ptr : Slot_Range := 0;

   procedure Alloc (Ptr : out Byte_Array_Access) with SPARK_Mode => Off
   is
   begin
      case Top_Ptr is
         when 0 => Ptr := Slot_0'Unrestricted_Access;
         when 1 => Ptr := Slot_1'Unrestricted_Access;
         when 2 => Ptr := Slot_2'Unrestricted_Access;
         when 3 => Ptr := Slot_3'Unrestricted_Access;
         when 4 => 
            raise Program_Error;
      end case;
      -- possibly zero out the buffer here
      Top_Ptr := Top_Ptr + 1;
   end Alloc;

   procedure Pop is
   begin
      Top_Ptr := Top_Ptr - 1;
   end Pop;

   procedure Init is
   begin
      Top_Ptr := 0;
   end Init;

   function Free_Slots return Slot_Range is (Slot_Range'Last - Top_Ptr);

end Memory;

and the session code could look like this:

   procedure Send_Discover (State : out Session_State) with                                                             
     Pre =>                                                                                                             
       Initialized and then Memory.Free_Slots >= 2,                                                                                                     
     Post =>                                                                                                            
       Initialized and then Memory.Free_Slots = Memory.Free_Slots'Old                                                                                                     
   is                                                                                                                   
      Options_Ctx : DHCP.Options.Context;                                                                               
      Parameter_Request_List_Ctx : DHCP.Option_Codes.Context;
      Options_Buffer : RFLX_Types.Bytes_Ptr;                                                                            
      Parameter_Request_List_Buffer : RFLX_Types.Bytes_Ptr; 
   begin                                                                                                                
      Options_Buffer := Get_Slot;
      DHCP.Options.Initialize (Options_Ctx, Options_Buffer);
      Parameter_Request_List_Buffer := Get_Slot;                                                             
      DHCP.Option_Codes.Initialize (Parameter_Request_List_Parameter_Request_List_Buffer);
      ... -- do stuff
      Memory.Pop;
      Memory.Pop;
   end Send_Discover;

Some comments:

• In any case, the body of Get_Slot needs to be out of SPARK.
• in SPARK Community, the Bytes_Ptr needs to be a regular access type (not general), and we need to use 'Unrestricted_Access inside Get_Slot. I'm unsure of the implications of this.
• This also means in theory code could attempt to call Free on such pointers. We can mitigate this somewhat by not providing a Free function.
• In SPARK Pro, Bytes_Ptr could be a general access type, which would allow us to use 'Access instead of 'Unrestricted_Access. Also, one could not call Free on such objects.
• There is no protection against using a buffer after Popping it. I will try to refine my design to protect against that.
• contracts in memory package and session code (see the pre/post of Send_Discover above) could check proper use of the allocator (no memory leaks, only using the allowed amount of buffers).
• Zeroing memory before returning a buffer could avoid any hidden information leak.

[kanigsson]

In fact if Pop (could be renamed to Free) takes the pointer to be freed as an in out parameter, it would protect against freeing things in the wrong order, as the pointer passed to Pop would be unusable afterwards anyway. So one could still pop things in the wrong order, but it wouldn't lead to any unsoundness AFAICS.

[senier]

I somewhat expected that the pointer idea would not work for some reason ;) Do you think treating elements of pointer arrays independently in the borrow checks would be a feature worth discussing within the SPARK team?

I like the interface and the fact that we don't strictly have to drop CE. If we add an in out parameter to Pop (I'd prefer Free if also have Alloc TBH) we should be also be able to do the memory cleanup there, right? This is the natural place as secrets could remain in memory indefinitely otherwise.

One aspect that we should think about sooner than later is how buffer sizes are determined. Our idea was to let the user chose suitable generic parameters at integration time, but given that we reuse slots for different states this doesn't seem to be straightforward.

[kanigsson]

The borrow checker doesn't know anything about values of variables (e.g. array indices) so it can't distinguish between the array cells. It's similar to flow analysis.
Yes, cleaning up in Free instead of Alloc makes sense.
As for buffer sizes, this approach doesn't care about them as long as they are all the same :-) Different buffer sizes could be accommodated by having a different allocator for each size. The size could be a generic parameter, but we would still need to know statically which buffer will require which size (whether it's a generic parameter or a known quantity).

[senier]

Memory Sizes

Configuration

Regarding the configuration of memory sizes, we decided to separate those integration aspects into an independent file. For every specification there can be an .rfi (RecordFlux Integration) file which (for now) defines the minimum sizes of all memory regions. For easy human and machine readability we settled on YAML as the format. As there may be multiple such sets of files (e.g. for different system architectures), we'll add a switch to rflx to specify a search path.

The file format looks like this:

Buffer_Sizes:
    default: <default_minimum_size>
    global:
        Global_Variable_1_Name: <minimum_size>
        ...
        Glocal_Variable_n_Name: <minimum_size>
    State_1:
        Local_Variable_1_Name: <minimum_size>
        ...
        Local_Variable_n_Name: <minimum_size>
    ...
    State_m:
        Local_Variable_1_Name: <minimum_size>
        ...
        Local_Variable_n_Name: <minimum_size>

The default size is used for all memory regions for which no explicit size is specified.

Calculation

Calculation of the required buffer sizes should be simple. The number of required buffers obviously is the maximum number of local variables used in any state. For every state we sort the required variable sizes in descending order and extend the resulting list to have the maximum length (by adding 0 size values). To calculate the required slot sizes, we simply take the maximum value for every position in every list across all states. The allocation for a local variable in a state simply is the position in the (state-specific) list referring to that local variable.

[treiher]

The proposed file format could lead to name conflicts between state names and global and default. This could be prevented by using a separate mapping for the states. IMHO, keywords should have a consistent casing (Buffer_Size, Default, Global).

Buffer_Size:
    Default: <default_minimum_size>
    Global:
        Global_Variable_1_Name: <minimum_size>
        ...
        Glocal_Variable_n_Name: <minimum_size>
    State:
        State_1:
            Local_Variable_1_Name: <minimum_size>
            ...
            Local_Variable_n_Name: <minimum_size>
        ...
        State_m:
            Local_Variable_1_Name: <minimum_size>
            ...
            Local_Variable_n_Name: <minimum_size>

[senier]

I agree. IMHO it should be States (plural).

[senier]

FWIW I am currently using source locations to identify such allocation points. It seems to work.

We discussed some alternative approaches, e.g. using a combination of the target variable and other properties of the expression to identify the allocation. While these approaches would allow a user to specify the size of those implicit allocations, they are far more complex than just using the location. We should stick with your location-based approach until the need for sth. more advanced arises.

[kanigsson]

I just discussed the allocation issue with Claire, and she proposed a small variation, which has much nicer properties. I'm recording the scheme here.

The idea is that instead of Get_Slot_* functions, we have global Slot_*_Ptr variables. These variables are initialized at some point, possibly at elaboration (this needs to be in SPARK_Mode => Off, similar to the body of the Get_Slot_* functions). The main advantage is that SPARK can track ownership for those pointers. This automatically avoids taking the same slot twice, or not giving back a slot, etc.
In this scheme, instead of calling Free, one has to move the pointer back to the Slot_Ptr variable. So the generated session code would look something like this:

      Options_Buffer := Slot_1_Ptr;
      DHCP.Options.Initialize (Options_Ctx, Options_Buffer);
      Parameter_Request_List_Buffer := Slot_2_Ptr;
      DHCP.Option_Codes.Initialize (Parameter_Request_List_Parameter_Request_List_Buffer);
      ... -- do stuff
      Slot_1_Ptr := Options_Buffer;
      Slot_2_Ptr := Parameter_Request_List_Buffer;

SPARK would detect aliasing in the code if Slot_1_Ptr was incorrectly replaced by Slot_2_Ptr, while the same kind of detection would require heavy contracts on the Get_Slot_* functions. Also it protects against using a buffer after having "freed" it.

I will change my local implementation to this scheme.

All of this is orthogonal to the allocation/buffer size issue.

[senier]

Neat! Have you validated this idea works?

We still have the issue that Slot_1_Ptr and Slot_2_Ptr could be swapped at the end invalidating all size assumptions in subsequent uses, right?

[kanigsson]

Not yet validated.
Your remark about the size assumptions are interesting, we haven't really discussed this yet. I guess that if we find a way to express that Slot_1_Ptr points to a buffer of (at least) a certain size, then we will solve the issue.

[senier]

Your remark about the size assumptions are interesting, we haven't really discussed this yet. I guess that if we find a way to express that Slot_1_Ptr points to a buffer of (at least) a certain size, then we will solve the issue.

Having the size formally stated would be nice. However, showing that Slot_1_Ptr is pointing to the same memory after a state is done may be a simpler first step. Could we just use a postcondition of the form Post => Slot_1_Ptr = Slot_1_Ptr'Old for every slot used in a state?