Abstract models and refinement in SPARK: allocators example

This program demonstrates how the specification of a SPARK program can be formalized using an abstract model and how the refinement relation between the model an its implementation can be verified using GNATprove. It is described in the article Abstract Software Specifications and Automatic Proof of Refinement” published at RSSRail 2016 conference.

The example contains three versions of an allocator package. They are specified in terms of mathematical structures (sequences and sets). The refinement relation between the mathematical model and the implementation is expressed as a ghost function Is_Valid and enforced through contracts. It can be verified automatically using GNATprove.

Simple_Allocator features a naive implementation of the allocator, storing the status (available or allocated) of each resource in a big array. It is specified using a ghost function Model which always returns a valid refinement of the allocator’s data. The refinement relation is verified only once, as a postcondition of the Model function. List_Allocator introduces a free list to access more efficiently the first available resource. Here not every possible state of the allocator data can be refined into a valid model. To work around this problem, the model is stored in a global ghost variable which is updated along with the allocator’s data and the refinement relation is expressed as an invariant that must be verified as a postcondition of each modifying procedure. The functional contracts on modifying procedures are straightforward but the refinement relation is now more complicated, as it needs to account for the implementation of the free list. List_Mod_Allocator features the same implementation and contracts as List_Allocator, but its model is returned by a ghost function like in Simple_Allocator instead of being stored in a global ghost variable. As not every possible state of the allocator can be refined into a valid model, the refinement relation is not expressed as a postcondition of Model, but as an invariant, as in List_Allocator and must be verified as a postcondition of each modifying procedure. The functional contracts and the refinement relation resemble those of List_Allocator. However, as we don’t construct explicitly the new model after each modification, the proof of the allocator’s functional contracts requires induction, which is beyond the reach of automatic solvers. The induction scheme is given here manually in an auto-active style through calls to ghost procedures.

Auteurs: Claire Dross

Catégories: Ghost code

Outils: SPARK 2014

Références: ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

The full code is in the ZIP archive above. Here are below the specifications of the simple allocator, the others may be found in the archive. The proofs can be replayed using SPARK Community 2018 and invoking the test.cmd script from the archive. simple_allocator.ads

File : simple_allocator.ads

pragma Unevaluated_Use_Of_Old (Allow);
with Ada.Containers.Functional_Sets;
with Ada.Containers;
use type Ada.Containers.Count_Type;

package Simple_Allocator with
  SPARK_Mode,
  Abstract_State    => State,
  Initializes       => State,
  Initial_Condition => All_Available
is
   Capacity : constant := 10_000;

   type Resource is new Integer range 0 .. Capacity;
   subtype Valid_Resource is Resource range 1 .. Capacity;

   No_Resource : constant Resource := 0;

   function Is_Available (Res : Resource) return Boolean;
   function Is_Allocated (Res : Resource) return Boolean;

   function All_Available return Boolean with Ghost;

   package M with Ghost is

      package S is new Ada.Containers.Functional_Sets
        (Element_Type => Resource, Equivalent_Elements => "=");
      use S;

      type T is record
         Available : Set;
         Allocated : Set;
      end record;

      function "=" (X, Y : T) return Boolean is
        (X.Available = Y.Available
           and then
         X.Allocated = Y.Allocated);

      function Is_Add
        (S : Set; E : Resource; Result : Set) return Boolean
      --  Returns True if Result is S plus E.

      is
        (not Contains (S, E)
         and then Contains (Result, E)
         and then Included_Except (Result, S, E)
         and then S <= Result);

      function Is_Valid (M : T) return Boolean;

      function Model return T with Post => Is_Valid (Model'Result);

   end M;

   use M; use M.S;

   procedure Alloc (Res : out Resource) with
     Contract_Cases =>

       --  When no resource is available, return the special value No_Resource
       --  with the allocator unmodified.

       (Is_Empty (Model.Available) =>
          Res = No_Resource
            and then
          Model = Model'Old,

        --  Otherwise, return an available resource which becomes allocated

        others =>
          Is_Add (Model.Available, Res, Result => Model.Available'Old)
            and then
          Is_Add (Model.Allocated'Old, Res, Result => Model.Allocated));

   procedure Free (Res : Resource) with
     Contract_Cases =>

       --  When the resource is allocated, make it available

       (Contains (Model.Allocated, Res) =>
          Is_Add (Model.Available'Old, Res, Result => Model.Available)
            and then
          Is_Add (Model.Allocated, Res, Result => Model.Allocated'Old),

        --  Otherwise, do nothing

        others =>
          Model = Model'Old);

end Simple_Allocator;

Toccata

Formally Verified Programs, Certified Tools and Numerical Computations

Abstract models and refinement in SPARK: allocators example

File : simple_allocator.ads