Channel interface in SPARK

[jklmnn]

Context and Problem Statement

The current session interface requires channels to provide subprograms as generic parameters to the session. The arguments of these subprograms currently only include the buffer, its size and it data is available. However they do not include any state about the interface being used. This restriction requires the package that provides the implementations to hold package state which is particularly inconvenient if there are multiple connections should be handled.

Requirements

• Interface to run state machine until data needs to be read or written
• Interface to read data from channel into provided buffer
• Interface to write data into channel from provided buffer
• Interface to check if channel has or needs data
• Only channels which have data or need data must be readable or writable

Considered Options

O1

To solve this problem a context argument should be added to the session interface that allows the user of the session to pass external state through the sessions state machine.
The new session interface could look as follows:

generic
   type Context is private;
   with function Context_Invariant (Ctx : Context) return Boolean;
   with function Has_Data (Ctx : Context) return Boolean;
   with procedure Read (Ctx    : in out Context;
                        Buffer :    out RFLX_Types.Bytes;
                        Length :    out RFLX_Types.Length);
   with procedure Write (Ctx    : in out Context;
                         Buffer :        RFLX_Types.Bytes);
package Session
is

   procedure Run (Ctx : in out Context) with
      Pre  => Uninitialized
              and then Context_Invariant (Ctx),
      Post => Uninitialized
              and then Context_Invariant (Ctx);

   procedure Tick (Ctx : in out Context) with
      Pre  => Initialized
              and then Context_Invariant (Ctx),
      Post => Initialized
              and then Context_Invariant (Ctx);

end Session;

The user of this package would then have to implement these properties accordingly:

with Session;

procedure Main
is
   function Initialized (Socket : Integer) return Boolean is (Socket > -1);
   procedure Has_Data (Socket : Integer) return Boolean with
      Pre => Initialized;
   procedure Read (Socket : in out Integer;
                   Buffer :    out RFLX_Types.Bytes;
                   Length :    out RFLX_Types.Length) with
      Pre  => Initialized (Socket),
      Post => Initialized (Socket);
   procedure Write (Socket : in out Integer;
                    Buffer :        RFLX_Types.Bytes) with
      Pre  => Initialized (Socket);
      Post => Initialized (Socket);
   Socket : Integer := Create_Socket;
   package Socket_Session is new Session (Integer, Initialized, Initialized, Has_Data, Read, Write);
begin
   return when not Initialized (Socket);
   Connect (Socket);
   Socket_Session.Run (Socket);
end Main;

It may not be required to have separate post and preconditions for the context.

O2

After some discussion the API design has been significantly changed. A channel is treated as a variable and the Run procedure will stop if data is needed or available.

generic
   --  needed for functions
package Session
is

   type Channel_Type is (Channel_1, Channel_2);

   function Has_Data (Channel : Channel_Type) return Boolean;
   function Needs_Data (Channel : Channel_Type) return Boolean;

   procedure Run (Channel_1_Buffer : in out Buffer_Ptr;
                  Channel_2_Buffer : in out Buffer_Ptr) with
      Pre  => Uninitialized
              and then Channel_1_Buffer /= null,
      Post => Uninitialized
              and then Channel_1_Buffer /= null;

   procedure Run (Channel_1_Read_Buffer  :     Buffer_Ptr;
                  Channel_1_Write_Buffer : out Buffer_Ptr;
                  Channel_2_Read_Buffer  :     Buffer_Ptr;
                  Channel_2_Write_Buffer : out Buffer_Ptr)
      Pre  => Uninitialized
              and then Channel_1_Read_Buffer /= null
              and then Channel_1_Write_Buffer /= null
              and then Channel_2_Read_Buffer /= null
              and then Channel_2_Write_Buffer /= null
              and then Channel_1_Read_Buffer.all'Length
                       <= Channel_1_Write_Buffer.all'Length
              and then Channel_2_Read_Buffer.all'Length
                       <= Channel_2_Write_Buffer.all'Length,
      Post => Uninitialized
              and then Channel_1_Read_Buffer /= null
              and then Channel_1_Write_Buffer /= null
              and then Channel_2_Read_Buffer /= null
              and then Channel_2_Write_Buffer /= null;

end Session;

Both interfaces with one and two pointers are needed. If only a single transport buffer is available the in out variant has to be used. On the other hand a readable buffer might not be writable so a separate read and write pointer are required.
Furthermore the channel is intended to handle as a variable in the session. In the case of a single pointer it's clear that this memory can be used. If two pointers are provided the writable memory needs to be used for that purpose.
To prevent implementing both variants separately the Run with two pointers can implemented as follows (at the expense of at least one copy):

procedure Run (Channel_1_Read_Buffer  :     Buffer_Ptr;
               Channel_1_Write_Buffer : out Buffer_Ptr)
is
begin
   Channel_1_Write_Buffer.all := Channel_1_Read_Buffer.all;
   Run (Channel_1_Write_Buffer);
end Run;

This interface can be used in different settings. Either in a asynchronous interrupt driven environment:

package Session is new Generic_Session;

IO_Buffer : Buffer_Ptr := new Buffer (...);

procedure Init
is
begin
   Session.Run;
   if Session.Has_Data (Channel_1) then
      Driver.Send (IO_Buffer);
   end if;
end Init;

procedure Interrupt_Handler
is
begin
   if Session.Needs_Data (Channel_1) then
      Driver.Receive (IO_Buffer);
   end if;
   Session.Run;
   if Session.Has_Data (Channel_1) then
      Driver.Send (IO_Buffer);
   end if;
end Interrupt_Handler;

After some discussion this option has been discarded. The reason is that the session internally assumes that the memory of the pointer doesn't change. This cannot be ensured.
A further problem is that there is no signalling to the session if a pointer has been initialized and is ready to use.

O3

Another option are simple read and write procedures:

generic
   --  needed for functions
package Session
is

   type Channel_Type is (Channel_1, Channel_2);

   function Has_Data (Channel : Channel_Type) return Boolean;
   function Needs_Data (Channel : Channel_Type) return Boolean;

   function Buffer_Size (Channel : Channel_Type) return Positive;

   procedure Run with
      Pre  => Uninitialized,
      Post => Uninitialized;

   procedure Read (Channel : Channel_Type;
                   Buffer  : Buffer_Type;
                   Offset  : Natural := 0) with
      Pre => Buffer'Length + Offset <= Buffer_Size (Channel);

   procedure Write (Channel :     Channel_Type;
                    Buffer  : out Buffer_Type;
                    Offset  :     Natural := 0) with
      Pre => Buffer'Length + Offset <= Buffer_Size (Channel);

end Session;

This interface allows a synchronous use:

procedure Main
is
   package Session is new Generic_Session;
   Buf : Buffer (1 .. 10);
begin
   loop
      for C in Channel'Range loop
         if Session.Has_Data (C) then
            Session.Write (C, Buf);
            Socket.Write (Buf (Buf'First .. Last));
         end if;
         if Session.Needs_Data (C) then
            Socket.Read (Buf);
            Session.Read (C, Buf);
         end;
      end loop;
      Session.Run;
   end loop;
end Main;

Asynchronous interfaces are also supported:

package Session is new Generic_Session;

procedure Handler_1
is
   Buf : Buffer;
begin
   for C in Channel'Range loop
      if Session.Has_Data (C) then
         Session.Write (C, Buf);
         Driver.Write (Buf (Buf'First .. Last));
      end if;
      if Session.Needs_Data (C) then
         Driver.Read (Buf);
         Session.Read (C, Buf);
      end;
   end loop;
   Session.Run;
end Handler_1;

procedure Handler_2 (Data_In  : Buffer;
                     Data_Out : out Buffer)
is
begin
   for C in Channel'Range loop
      if Session.Has_Data (C) then
         Session.Write (C, Data_Out);
      end if;
      if Session.Needs_Data (C) then
         Session.Read (C, Data_In);
      end;
   end loop;
   Session.Run;
end Handler_2;

This interface also allows partial reading and writing:

procedure Handler
is
   Buf : Buffer (1 .. 10);
   Offset : Natural := 0;
begin
   if Session.Needs_Data (Session.Channel_1) then
      while Driver.Has_Data loop
         Driver.Read (Buf);
         Session.Read (Buf, Offset);
         Offset := Offset + 1;
      end;
   Session.Run;
end Handler;

A C API would be analogous:

void session_run(void);

int has_data(channel_t channel);

int needs_data(channel_t channel);

void read(const void *buf, size_t size, size_t offset);

void write(void *buf, size_t *size, size_t offset);

Semantics

• State machine stops before state with channel read/write
• Channel reads/writes must be only statements in state to prevent interference with other actions
• Channel cannot be read and written in same state (i.e., not any X'Read (Y) and X'Write (Y) with same X)
• Variable cannot be read or written in same state (i.e., not any X'Read (Y) or X'Write (Y) with same Y)
• It can be checked if data to channel has been written (by X'Has_Data)
• Buffer size depends on channel and state
• If no data for channel provided, Run continues based on given state transitions

O3A

One of the problems with O3 is that a separate buffer is required if the IO code needs a buffer. To prevent a copy the session can make the internal buffer accessible via a generic callback. The implementation is analogous to the non-callback variant:

package Session is

   generic
      with procedure Read (Buf : out Buffer);
   procedure Generic_Read (Channel : Channel_Type);

   generic
      with procedure Write (Buf : Buffer);
   procedure Generic_Write (Channel : Channel_Type);

end Session;

package body Session is

   procedure Generic_Read (Channel : Channel_Type)
   is
   begin
      Read (Internal_Buffer);
   end Generic_Read;

   procedure Generic_Write (Channel : Channel_Type)
   is
   begin
      Write (Internal_Buffer);
   end Generic_Write;

end Session;

This simplifies the usage with other read/write procedures:

procedure Handler_1
is
   procedure Local_Read (Buf : out Buffer)
   is
   begin
      Driver.Read (Buf);
   end Local_Read;
   procedure Local_Write (Buf : Buffer)
   is
   begin
      Driver.Write (Buf);
   end Local_Write;
   procedure Read is new Session.Read (Local_Read);
   procedure Write is new Session.Write (Local_Write);
begin
   Run;
   for C in Channel'Range loop
      if Session.Has_Data (C) then
         Session.Write (C);
      end if;
      if Session.Needs_Data (C) then
         Session.Read (C);
      end;
   end loop;
end Handler_1;

Since C uses pointers in its API a copy can be done directly with memcpy and the interface conversion done here is not necessary.

Decision Outcome

O3

[treiher]

This probably solves #766. Having a Context_Invariant instead of a separate Context_Precondition and Context_Postcondition could be sufficient.

[jklmnn]

I updated the description.

[treiher]

I have changed the title and the description of the issue and also added the new design options (as O2, O3 and O3a) to keep a better overview of all considered designs.

For the new design options, the session model would probably have to be changed. To enable stopping the state machine before reading or writing to a channel, the read or write action must be performed in a separate state.

[treiher]

I have created a prototypical implementation of O3 based on a simple example session with multiple channels. The code is executable and is completely verified. O3 seems to fulfill our requirements, so that we could start adapting the code generator.