From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,1a6555c7f36c101c,start
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news4.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!newsfeed.freenet.de!newsfeed01.chello.at!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Newsgroups: comp.lang.ada
Subject: Q: compiler generated timing checks
From: Georg Bauhaus <bauhaus@arcor.de>
Content-Type: text/plain
Content-Transfer-Encoding: 7bit
Organization: #
Message-ID: <1170800847.26019.30.camel@localhost>
Mime-Version: 1.0
X-Mailer: Evolution 2.6.1 
Date: Tue, 06 Feb 2007 23:27:27 +0100
NNTP-Posting-Date: 06 Feb 2007 23:26:36 CET
NNTP-Posting-Host: ac4b2227.newsspool4.arcor-online.net
X-Trace: 
 DXC=T9S65ZNhb@;gP]QSEBQ^d44IUK<Cl32<14Fo<]lROoR14nDHegD_]R50SDWDeFc0i5N[W<lHX`=B4\6BhD5G6\i<I80h=LJ`5j3
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news2.google.com comp.lang.ada:9038
Date: 2007-02-06T23:26:36+01:00
List-Id: <comp.lang.ada>

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;