prove global state of memory server

ref #164

src/memory/gneiss-memory.ads

@@ -73,6 +73,14 @@ is
    --  @return         Index option that can be invalid
    function Index (Session : Dispatcher_Session) return Session_Index_Option;
 
+   --  Proof property that the dispatcher is registered on the platform
+   --
+   --  @param Session  Dispatcher session instance
+   --  @return         Dispatcher is registered on the platform
+   function Registered (Session : Dispatcher_Session) return Boolean with
+      Ghost,
+      Pre => Initialized (Session);
+
 private
 
    type Client_Session is new Gneiss_Internal.Memory.Client_Session;

src/memory/linux/gneiss-memory.adb

@@ -22,8 +22,7 @@ is
    function Initialized (Session : Dispatcher_Session) return Boolean is
       (Session.Index.Valid
        and then Gneiss_Internal.Valid (Session.Efd)
-       and then Gneiss_Internal.Valid (Session.Broker_Fd)
-       and then (if Session.Registered then Gneiss_Internal.Valid (Session.Dispatch_Fd)));
+       and then Gneiss_Internal.Valid (Session.Broker_Fd));
 
    function Index (Session : Client_Session) return Session_Index_Option is
       (Session.Index);
@@ -34,4 +33,7 @@ is
    function Index (Session : Dispatcher_Session) return Session_Index_Option is
       (Session.Index);
 
+   function Registered (Session : Dispatcher_Session) return Boolean is
+      (Gneiss_Internal.Valid (Session.Dispatch_Fd));
+
 end Gneiss.Memory;

src/memory/linux/gneiss_internal-memory.ads

@@ -27,7 +27,6 @@ is
       Efd         : Epoll_Fd                    := -1;
       Dispatch_Fd : File_Descriptor             := -1;
       Accepted    : Boolean                     := False;
-      Registered  : Boolean                     := False;
       E_Cap       : Event_Cap                   := Invalid_Event_Cap;
    end record;
 

src/memory/server/gneiss-memory-dispatcher.ads

@@ -10,6 +10,7 @@
 --
 
 with Gneiss.Memory.Server;
+with Gneiss_Internal;
 
 generic
    pragma Warnings (Off, "* is not referenced");
@@ -40,14 +41,16 @@ is
    --  @param Idx      Session index
    procedure Initialize (Session : in out Dispatcher_Session;
                          Cap     :        Capability;
-                         Idx     :        Session_Index := 1);
+                         Idx     :        Session_Index := 1) with
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Register service to the platform, should be called when the component initialization is finished
    --
    --  @param Session  Dispatcher session
    procedure Register (Session : in out Dispatcher_Session) with
-      Pre  => Initialized (Session),
-      Post => Initialized (Session);
+      Pre    => Initialized (Session),
+      Post   => Initialized (Session),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Checks if a session request/dispatcher capability is valid
    --
@@ -56,7 +59,8 @@ is
    --  @return         True indicates that a client requested a connection
    function Valid_Session_Request (Session : Dispatcher_Session;
                                    Cap     : Dispatcher_Capability) return Boolean with
-      Pre => Initialized (Session);
+      Pre    => Initialized (Session),
+      Global => null;
 
    --  Initialize server session
    --  @param Session   Dispatcher session
@@ -68,12 +72,15 @@ is
                                  Server_S : in out Server_Session;
                                  Ctx      : in out Server_Instance.Context;
                                  Idx      :        Session_Index := 1) with
-      Pre  => Initialized (Session)
-              and then Valid_Session_Request (Session, Cap)
-              and then not Server_Instance.Ready (Server_S, Ctx)
-              and then not Initialized (Server_S),
-      Post => Initialized (Session)
-              and then Valid_Session_Request (Session, Cap);
+      Pre    => Initialized (Session)
+                and then Registered (Session)
+                and then Valid_Session_Request (Session, Cap)
+                and then not Server_Instance.Ready (Server_S, Ctx)
+                and then not Initialized (Server_S),
+      Post   => Initialized (Session)
+                and then Registered (Session)
+                and then Valid_Session_Request (Session, Cap),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Accept initialized server session
    --  @param Session   Dispatcher session
@@ -83,13 +90,16 @@ is
                              Cap      :        Dispatcher_Capability;
                              Server_S : in out Server_Session;
                              Ctx      :        Server_Instance.Context) with
-      Pre  => Initialized (Session)
-              and then Valid_Session_Request (Session, Cap)
-              and then Server_Instance.Ready (Server_S, Ctx)
-              and then Initialized (Server_S),
-      Post => Initialized (Session)
-              and then Server_Instance.Ready (Server_S, Ctx)
-              and then Initialized (Server_S);
+      Pre    => Initialized (Session)
+                and then Registered (Session)
+                and then Valid_Session_Request (Session, Cap)
+                and then Server_Instance.Ready (Server_S, Ctx)
+                and then Initialized (Server_S),
+      Post   => Initialized (Session)
+                and then Registered (Session)
+                and then Server_Instance.Ready (Server_S, Ctx)
+                and then Initialized (Server_S),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Garbage collects disconnected sessions
    --
@@ -104,7 +114,10 @@ is
                               Cap      :        Dispatcher_Capability;
                               Server_S : in out Server_Session;
                               Ctx      : in out Server_Instance.Context) with
-      Pre  => Initialized (Session),
-      Post => Initialized (Session);
+      Pre    => Initialized (Session)
+                and then Registered (Session),
+      Post   => Initialized (Session)
+                and then Registered (Session),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
 end Gneiss.Memory.Dispatcher;

src/memory/server/linux/gneiss-memory-dispatcher.adb

@@ -1,6 +1,5 @@
 
 with System;
-with Gneiss_Internal;
 with Gneiss_Internal.Epoll;
 with Gneiss_Internal.Client;
 with Gneiss_Internal.Syscall;
@@ -50,7 +49,7 @@ is
       Name  : Gneiss_Internal.Session_Label;
       Label : Gneiss_Internal.Session_Label;
    begin
-      if not Initialized (Session) then
+      if not Initialized (Session) or else not Gneiss_Internal.Valid (Session.Dispatch_Fd) then
          return;
       end if;
       if Fd = Session.Dispatch_Fd then
@@ -93,7 +92,7 @@ is
       if not Initialized (Session) then
          return;
       end if;
-      if Fd = Session.Dispatch_Fd and then Session.Registered then
+      if Fd = Session.Dispatch_Fd and then Gneiss_Internal.Valid (Session.Dispatch_Fd) then
          Gneiss_Internal.Epoll.Remove (Session.Efd, Session.Dispatch_Fd, Ignore_Success);
       end if;
    end Dispatch_Error;
@@ -103,21 +102,24 @@ is
                          Idx     :        Session_Index := 1)
    is
    begin
+      if Initialized (Session) then
+         return;
+      end if;
       Session.Broker_Fd := Cap.Broker_Fd;
       Session.Efd  := Cap.Efd;
       Session.Index     := Session_Index_Option'(Valid => True, Value => Idx);
+      Gneiss_Internal.Syscall.Modify_Platform;
    end Initialize;
 
    procedure Register (Session : in out Dispatcher_Session)
    is
       Ignore_Success : Boolean;
    begin
-      if Session.Registered then
+      if Gneiss_Internal.Valid (Session.Dispatch_Fd) then
          return;
       end if;
       Gneiss_Internal.Client.Register (Session.Broker_Fd, Gneiss_Protocol.Session.Memory, Session.Dispatch_Fd);
       if Gneiss_Internal.Valid (Session.Dispatch_Fd) then
-         Session.Registered := True;
          Session.E_Cap      := Dispatch_Cap (Session, Session, Session.Dispatch_Fd);
          Gneiss_Internal.Epoll.Add (Session.Efd, Session.Dispatch_Fd,
                                     Dispatch_Event_Address (Session), Ignore_Success);

src/memory/server/linux/gneiss-memory-server.adb

@@ -34,6 +34,7 @@ is
          Import,
          Address => Session.Map;
    begin
+      Gneiss_Internal.Syscall.Modify_Platform;
       Generic_Modify (Session, B, Ctx);
    end Modify;
 

test/memory_server/component.adb

@@ -4,7 +4,11 @@ with Gneiss.Memory.Dispatcher;
 with Gneiss.Memory.Server;
 
 package body Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Refined_State => (Component_State => Capability,
+                     Platform_State  => (Dispatcher,
+                                         Servers,
+                                         Server_Data))
 is
 
    package Memory is new Gneiss.Memory (Character, Positive, String);
@@ -28,32 +32,40 @@ is
    procedure Modify (Session : in out Memory.Server_Session;
                      Data    : in out String;
                      Context : in out Server_Meta) with
-      Pre  => Memory.Initialized (Session)
-              and then Ready (Session, Context)
-              and then Contract (Context),
-      Post => Memory.Initialized (Session)
-              and then Ready (Session, Context)
-              and then Contract (Context);
+      Pre    => Memory.Initialized (Session)
+                and then Ready (Session, Context)
+                and then Contract (Context),
+      Post   => Memory.Initialized (Session)
+                and then Ready (Session, Context)
+                and then Contract (Context),
+      Global => null;
 
    procedure Initialize (Session : in out Memory.Server_Session;
                          Context : in out Server_Meta) with
-      Pre  => Memory.Initialized (Session),
-      Post => Memory.Initialized (Session);
+      Pre    => Memory.Initialized (Session),
+      Post   => Memory.Initialized (Session),
+      Global => null;
 
    procedure Finalize (Session : in out Memory.Server_Session;
                        Context : in out Server_Meta) with
-      Pre  => Memory.Initialized (Session),
-      Post => Memory.Initialized (Session);
+      Pre    => Memory.Initialized (Session),
+      Post   => Memory.Initialized (Session),
+      Global => null;
 
    function Ready (Session : Memory.Server_Session;
-                   Context : Server_Meta) return Boolean;
+                   Context : Server_Meta) return Boolean with
+      Global => null;
 
    procedure Dispatch (Session  : in out Memory.Dispatcher_Session;
                        Disp_Cap :        Memory.Dispatcher_Capability;
                        Name     :        String;
                        Label    :        String) with
-      Pre  => Memory.Initialized (Session),
-      Post => Memory.Initialized (Session);
+      Pre    => Memory.Initialized (Session)
+                and then Memory.Registered (Session),
+      Post   => Memory.Initialized (Session)
+                and then Memory.Registered (Session),
+      Global => (In_Out => (Servers, Server_Data,
+                            Gneiss_Internal.Platform_State));
 
    package Memory_Server is new Memory.Server (Server_Meta, Modify, Initialize, Finalize, Ready);
    package Memory_Dispatcher is new Memory.Dispatcher (Memory_Server, Dispatch);

test/memory_server/component.ads

@@ -1,13 +1,22 @@
 
 with Gneiss;
 with Gneiss.Component;
+with Gneiss_Internal;
 
 package Component with
-   SPARK_Mode
+SPARK_Mode,
+   Abstract_State => (Component_State, Platform_State),
+   Initializes    => (Platform_State, Main.Platform)
 is
 
-   procedure Construct (Cap : Gneiss.Capability);
-   procedure Destruct;
+   procedure Construct (Cap : Gneiss.Capability) with
+      Global => (Output => Component_State,
+                 In_Out => (Platform_State,
+                            Main.Platform,
+                            Gneiss_Internal.Platform_State));
+
+   procedure Destruct with
+      Global => null;
 
    package Main is new Gneiss.Component (Construct, Destruct);