Q: compiler generated timing checks

Q: compiler generated timing checks

[Georg Bauhaus]

The time a sequential subprogram takes to compute its results
is sometimes known to be within certain bounds.
It is known, for example, when someone has shown that
subprogram P will need no more than K * N**2 clock ticks.
I was wondering whether it might make any sense to
provide standard means of informing an Ada tool
of the expected running time of a subprogram. Either

(1) just assert certain O(f(n)) properties via a pragma

(2) in addition, have the compiler inject some timing checks
    (via instrumentation or via rewriting)

I have left out CPU task switches and used Real_Time in what
follows, just to show the general idea. If this is an idea.
I have also ignored Time <-> Space interactions, caches, etc..

I am *not* suggesting that these annotations will magically
turn into a proof system.


By assumption, a package Complexity pre-defines functions that
can be used in pragmas to express O(n**2) and the like. 

with [System.]Complexity; use [System.]Complexity;
package Tempus_Fugit is

   -- demonstrating pragma Complexity on procedure `compute`

   type T is range 1 .. 99;

   procedure compute(X: in out T);
     -- uses a weird algorithm in "TIME(3 * X**2)" and "SPACE(X*log(X))"

   pragma Complexity
      (Space,
       On => compute,
       Order => Square,
       Input => (1 => X),
       Factor => (1 => 1));

   pragma Complexity
      (Time,
       On => compute,
       Order => N_Log_N,
       Input => (1 => 10_000), -- should be magic_of(X)?
       Factor => (1 => 3));

end Tempus_Fugit;


with Ada.Real_Time;
package Complexity is

   use Ada.Real_Time;

   -- Permit complexity annotations on subprograms using the
   -- tentative
   -- pragma Complexity(Time | Space,
   --                   Input => ..., [Factor => ...]);

   type Count is new Natural;
      -- number of elements in one argument

   type Inputs is array (Positive range <>) of Count;
      -- for each argument, its number of elements

   type Factors is array (Positive range <>) of Natural;
      -- for each argument, its weight

   type Order is private;

   function Takes(O: Order) return Time_Span;
     -- the time it takes to compute a subprogram

   type Measurement_Function is access function
      (Sizes: Inputs;
       Weights: Factors) return Order;


   -- predefined

   Square: constant Measurement_Function;

   -- ...

private
   pragma inline(Takes);

   type Order is
      record
         -- leaving out Space for now...
         Worst: Measurement_Function;
         Ready: Time_Span;
      end record;

   function O_2 (Sizes: Inputs;
                 Weights: Factors) return Order;

   Square: constant Measurement_Function := O_2'access;
end Complexity;


package body Complexity is

   function O_2 (Sizes: Inputs;
                 Weights: Factors) return Order
   is
      pragma assert(Sizes'length = 1);
      pragma assert(Weights'length = 1);

      n: Count renames Sizes(Sizes'first);
      k: Natural renames Weights(Weights'First);
   begin
      return Order'(Worst => Square,
                    Ready => k * Natural(n * n) * tick);
   end O_2;

   function Takes(O: Order) return Time_Span is
   begin
      return O.Ready;
   end Takes;

end Complexity;


with Ada.Real_Time;
package body Tempus_Fugit is

   use Ada.Real_Time;

   -- BEGIN compiler generated code (for compute)
   order_c_gen: constant Order :=
      Square(Sizes => (1 => 10_000), Weights => (1 => 1));
     -- on behalf of the Complexity pragma on compute

   comp_lang_ada: constant Duration := 0.001;
     -- forcing the assumptions :-)

   procedure compute_c_gen(x: in out T) is
      start_c_gen : constant Time := Clock;
      y: T := T'first;
   begin
      while x > y loop
         while y < T'last loop
            y := T'succ(y);
            delay comp_lang_ada;  -- for demo, pretend to work
         end loop;
         x := T'pred(x);
         y := T'first;
      end loop;
      pragma assert
         (Clock >= start_c_gen + Takes(order_c_gen),
          "timing error in compute_c_gen");
   end compute_c_gen;

   procedure compute(x: in out T) renames compute_c_gen;
   -- END compiler generated code
--C    procedure compute(x: in out T) is
--C       y: T := T'first;
--C    begin
--C       while x > y loop
--C          while y < T'last loop
--C             y := T'succ(y);
--C          end loop;
--C          x := T'pred(x);
--C          y := T'first;
--C       end loop;
--C    end compute;


end Tempus_Fugit;


with Tempus_Fugit;
procedure test_complexity is
   X: Tempus_Fugit.T := 17;
begin
   Tempus_Fugit.compute(X);
end test_complexity;

Re: Q: compiler generated timing checks

[Georg Bauhaus]

On Tue, 2007-02-06 at 23:27 +0100, Georg Bauhaus wrote:

>    procedure compute(X: in out T);
>      -- uses a weird algorithm in "TIME(3 * X**2)" and "SPACE(X*log(X))"
> 
>    pragma Complexity
>       (Space,
>        On => compute,
>        Order => Square,
>        Input => (1 => X),
>        Factor => (1 => 1));
> 
>    pragma Complexity
>       (Time,
>        On => compute,
>        Order => N_Log_N,
>        Input => (1 => 10_000), -- should be magic_of(X)?
>        Factor => (1 => 3));
> 
> end Tempus_Fugit;
> 
--- foo.ada     2007-02-06 23:37:03.000000000 +0100
+++ foo-new.ada 2007-02-06 23:38:49.000000000 +0100
@@ -11,14 +11,14 @@
    pragma Complexity
       (Space,
        On => compute,
-       Order => Square,
+       Order => N_Log_N,
        Input => (1 => X),
        Factor => (1 => 1));

    pragma Complexity
       (Time,
        On => compute,
-       Order => N_Log_N,
+       Order => Square,
        Input => (1 => 10_000), -- should be magic_of(X)?
        Factor => (1 => 3));

Sorry.