isl_tab_basic_set_non_trivial_lexmin: do not add cuts for all variables

We found a test case where adding cuts for all variables can increase
the time of the scheduling algorithm significantly (from ms to never
seen terminating). Even though we did not understand the problem
entirely, the intuition we have is the following:

When using isl_tab_basic_set_non_trivial_lexmin, the ILP problem is
(usually) not empty, but infinite. Adding all cuts, seems to increase
the objective function only in very small steps. Adding only one cut at
a time allows us to increase it with a step as big as possible.

This patch does not change the behaviour when calling
check_integer_feasible.  In case we're calling cut_to_integer_lexmin
from check_integer_feasible, if it takes a long time to compute, then
it's "usually" because the context is empty and it's just taking a long
time for us to discover that it's empty. We believe in that case it
could still make sense to add all cuts.

This patch was tested on polybench 2.0 with Polly and minimal fusion.
On the larger kernels, it could not solve any infinite scheduling time
problems, but it was able to speed up one test case by 2x and did not
yield increased scheduling time for the other test cases.

Signed-off-by: Tobias Grosser <tobias@grosser.es>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index 4764334..dd14fb8 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -1606,6 +1606,9 @@ static int add_cut(struct isl_tab *tab, int row)
        return tab->con[r].index;
 }
 
+#define CUT_ALL 1
+#define CUT_ONE 0
+
 /* Given a non-parametric tableau, add cuts until an integer
  * sample point is obtained or until the tableau is determined
  * to be integer infeasible.
@@ -1617,8 +1620,12 @@ static int add_cut(struct isl_tab *tab, int row)
  * combination of variables/constraints plus a non-integral constant,
  * then there is no way to obtain an integer point and we return
  * a tableau that is marked empty.
+ * The parameter cutting_strategy controls the strategy used when adding cuts
+ * to remove non-integer points. CUT_ALL adds all possible cuts
+ * before continuing the search. CUT_ONE adds only one cut at a time.
  */
-static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
+static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab,
+       int cutting_strategy)
 {
        int var;
        int row;
@@ -1640,6 +1647,8 @@ static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
                        row = add_cut(tab, row);
                        if (row < 0)
                                goto error;
+                       if (cutting_strategy == CUT_ONE)
+                               break;
                } while ((var = next_non_integer_var(tab, var, &flags)) != -1);
                if (restore_lexmin(tab) < 0)
                        goto error;
@@ -1730,7 +1739,7 @@ static struct isl_tab *check_integer_feasible(struct isl_tab *tab)
        if (isl_tab_push_basis(tab) < 0)
                goto error;
 
-       tab = cut_to_integer_lexmin(tab);
+       tab = cut_to_integer_lexmin(tab, CUT_ALL);
        if (!tab)
                goto error;
 
@@ -4958,7 +4967,7 @@ __isl_give isl_vec *isl_tab_basic_set_non_trivial_lexmin(
                int side, base;
 
                if (init) {
-                       tab = cut_to_integer_lexmin(tab);
+                       tab = cut_to_integer_lexmin(tab, CUT_ONE);
                        if (!tab)
                                goto error;
                        if (tab->empty)

diff --git a/isl_test.c b/isl_test.c
index 689f75e..5f1f9dc 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -2239,6 +2239,49 @@ int test_schedule(isl_ctx *ctx)
                return -1;
        ctx->opt->schedule_outer_zero_distance = 0;
 
+       D = "{Stmt_for_body24[i0, i1, i2, i3]:"
+               "i0 >= 0 and i0 <= 1 and i1 >= 0 and i1 <= 6 and i2 >= 2 and "
+               "i2 <= 6 - i1 and i3 >= 0 and i3 <= -1 + i2;"
+            "Stmt_for_body24[i0, i1, 1, 0]:"
+               "i0 >= 0 and i0 <= 1 and i1 >= 0 and i1 <= 5;"
+            "Stmt_for_body7[i0, i1, i2]:"
+               "i0 >= 0 and i0 <= 1 and i1 >= 0 and i1 <= 7 and i2 >= 0 and "
+               "i2 <= 7 }";
+
+       V = "{Stmt_for_body24[0, i1, i2, i3] -> "
+               "Stmt_for_body24[1, i1, i2, i3]:"
+               "i3 >= 0 and i3 <= -1 + i2 and i1 >= 0 and i2 <= 6 - i1 and "
+               "i2 >= 1;"
+            "Stmt_for_body24[0, i1, i2, i3] -> "
+               "Stmt_for_body7[1, 1 + i1 + i3, 1 + i1 + i2]:"
+               "i3 <= -1 + i2 and i2 <= 6 - i1 and i2 >= 1 and i1 >= 0 and "
+               "i3 >= 0;"
+             "Stmt_for_body24[0, i1, i2, i3] ->"
+               "Stmt_for_body7[1, i1, 1 + i1 + i3]:"
+               "i3 >= 0 and i2 <= 6 - i1 and i1 >= 0 and i3 <= -1 + i2;"
+             "Stmt_for_body7[0, i1, i2] -> Stmt_for_body7[1, i1, i2]:"
+               "(i2 >= 1 + i1 and i2 <= 6 and i1 >= 0 and i1 <= 4) or "
+               "(i2 >= 3 and i2 <= 7 and i1 >= 1 and i2 >= 1 + i1) or "
+               "(i2 >= 0 and i2 <= i1 and i2 >= -7 + i1 and i1 <= 7);"
+             "Stmt_for_body7[0, i1, 1 + i1] -> Stmt_for_body7[1, i1, 1 + i1]:"
+               "i1 <= 6 and i1 >= 0;"
+             "Stmt_for_body7[0, 0, 7] -> Stmt_for_body7[1, 0, 7];"
+             "Stmt_for_body7[i0, i1, i2] -> "
+               "Stmt_for_body24[i0, o1, -1 + i2 - o1, -1 + i1 - o1]:"
+               "i0 >= 0 and i0 <= 1 and o1 >= 0 and i2 >= 1 + i1 and "
+               "o1 <= -2 + i2 and i2 <= 7 and o1 <= -1 + i1;"
+             "Stmt_for_body7[i0, i1, i2] -> "
+               "Stmt_for_body24[i0, i1, o2, -1 - i1 + i2]:"
+               "i0 >= 0 and i0 <= 1 and i1 >= 0 and o2 >= -i1 + i2 and "
+               "o2 >= 1 and o2 <= 6 - i1 and i2 >= 1 + i1 }";
+       P = V;
+       S = "{ Stmt_for_body24[i0, i1, i2, i3] -> "
+               "[i0, 5i0 + i1, 6i0 + i1 + i2, 1 + 6i0 + i1 + i2 + i3, 1];"
+           "Stmt_for_body7[i0, i1, i2] -> [0, 5i0, 6i0 + i1, 6i0 + i2, 0] }";
+
+       if (test_special_schedule(ctx, D, V, P, S) < 0)
+               return -1;
+
        D = "{ S_0[i, j] : i >= 1 and i <= 10 and j >= 1 and j <= 8 }";
        V = "{ S_0[i, j] -> S_0[i, 1 + j] : i >= 1 and i <= 10 and "
                                           "j >= 1 and j <= 7;"