[LLVMdev] Symbolic Loop Analysis Pass

[Sebastian Dreßler]

Hi,

I'm currently working on a pass for symbolic loop analysis and like to
start a small discussion.

The goal is to get an expression for the loop enabling calculation of
e.g. the trip count. Furthermore, inter-loop-dependencies should be
regarded. I'm currently testing with Livermore loops.

For instance, the following code (Livermore kernel 2)

  for (l = 1; l <= loop; l++) {

    ii = n;
    ipntp = 0;

    do {

      ipnt = ipntp;
      ipntp += ii;
      ii /= 2;
      i = ipntp - 1;

      for (k = ipnt + 1; k < ipnpt; k = k + 2) {
        [...]
      }

    } while (ii > 0);

  }

currently leads to this analysis result:

  L0: l[Init: 1] <= ConstExpr by l += 1
  L1: ii[Init: ConstExpr] > 0 by ii /= 2
  L2: k[Init: ipnt + 1] < ipntp[Init: 0, Inc: ipntp + ii] by k += 2

plus the info, that L2 is contained in L1 is contained in L0:

  L0 -> L1 -> L2

SCEV for such a case results in "unpredictable backedge-taken count".
The "init" and "inc" at "ipntp" for L2 also contain the information,
that "init" occurs on every L0 and "inc" occurs on every L1.

Based on the evaluation of the loop properties and the generated
formulas, one could for instance pre-calculate the values for l, ii and
k, of course only if the needed parameters are known.


What do you think? Would this pass be useful for others except for me?
Is there any related work? I've found [1], but they do not use LLVM and
it seems to specialized to me.


Cheers,
Sebastian



[1]: Knoop, J., Kovács, L., & Zwirchmayr, J. (2012). Symbolic loop bound
computation for wcet analysis. In Perspectives of Systems Informatics
(pp. 227-242). Springer Berlin, Heidelberg.
http://www.complang.tuwien.ac.at/lkovacs/pub/PSI11_Kovacs.pdf

-- 
Mit freundlichen Grüßen / Kind regards

Sebastian Dreßler

Zuse Institute Berlin (ZIB)
Takustraße 7
D-14195 Berlin-Dahlem
Germany

dressler at zib.de
Phone: +49 30 84185-261

http://www.zib.de/