From f3959eac4433f2a37208a28213413b0e9482cd65 Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Fri, 24 Apr 2020 13:39:04 +0200 Subject: [PATCH] prove global state of memory server ref #164 --- src/memory/gneiss-memory.ads | 8 +++ src/memory/linux/gneiss-memory.adb | 6 ++- src/memory/linux/gneiss_internal-memory.ads | 1 - .../server/gneiss-memory-dispatcher.ads | 51 ++++++++++++------- .../server/linux/gneiss-memory-dispatcher.adb | 12 +++-- .../server/linux/gneiss-memory-server.adb | 1 + test/memory_server/component.adb | 40 ++++++++++----- test/memory_server/component.ads | 15 ++++-- 8 files changed, 90 insertions(+), 44 deletions(-) diff --git a/src/memory/gneiss-memory.ads b/src/memory/gneiss-memory.ads index 6090357..a223e31 100644 --- a/src/memory/gneiss-memory.ads +++ b/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; diff --git a/src/memory/linux/gneiss-memory.adb b/src/memory/linux/gneiss-memory.adb index fd4fcd9..eb4a95f 100644 --- a/src/memory/linux/gneiss-memory.adb +++ b/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; diff --git a/src/memory/linux/gneiss_internal-memory.ads b/src/memory/linux/gneiss_internal-memory.ads index f7319d5..e9c49f6 100644 --- a/src/memory/linux/gneiss_internal-memory.ads +++ b/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; diff --git a/src/memory/server/gneiss-memory-dispatcher.ads b/src/memory/server/gneiss-memory-dispatcher.ads index d7a07fa..b960978 100644 --- a/src/memory/server/gneiss-memory-dispatcher.ads +++ b/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; diff --git a/src/memory/server/linux/gneiss-memory-dispatcher.adb b/src/memory/server/linux/gneiss-memory-dispatcher.adb index 82822e9..87525c2 100644 --- a/src/memory/server/linux/gneiss-memory-dispatcher.adb +++ b/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); diff --git a/src/memory/server/linux/gneiss-memory-server.adb b/src/memory/server/linux/gneiss-memory-server.adb index c8cf490..254ab61 100644 --- a/src/memory/server/linux/gneiss-memory-server.adb +++ b/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; diff --git a/test/memory_server/component.adb b/test/memory_server/component.adb index ec23e5e..672cf3e 100644 --- a/test/memory_server/component.adb +++ b/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); diff --git a/test/memory_server/component.ads b/test/memory_server/component.ads index 477cf45..f8b70a2 100644 --- a/test/memory_server/component.ads +++ b/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);