allow the user to impose a bound on the number of low-level operations
authorSven Verdoolaege <skimo@kotnet.org>
Wed, 18 Dec 2013 11:05:32 +0000 (18 12:05 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Sun, 22 Dec 2013 07:16:53 +0000 (22 08:16 +0100)
This should allow the user to deterministically limit the effort
spent on a computation.

Requested-by: Tobias Grosser <tobias@grosser.es>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
doc/user.pod
include/isl/ctx.h
isl_ctx.c
isl_ctx_private.h
isl_options.c
isl_options_private.h
isl_tab.c

index 162dac4..dc295e4 100644 (file)
@@ -339,6 +339,21 @@ before the C<isl_ctx> itself is freed.
        isl_ctx *isl_ctx_alloc();
        void isl_ctx_free(isl_ctx *ctx);
 
+The user can impose a bound on the number of low-level I<operations>
+that can be performed by an C<isl_ctx>.  This bound can be set and
+retrieved using the following functions.  A bound of zero means that
+no bound is imposed.  The number of operations performed can be
+reset using C<isl_ctx_reset_operations>.  Note that the number
+of low-level operations needed to perform a high-level computation
+may differ significantly across different versions
+of C<isl>, but it should be the same across different platforms
+for the same version of C<isl>.
+
+       void isl_ctx_set_max_operations(isl_ctx *ctx,
+               unsigned long max_operations);
+       unsigned long isl_ctx_get_max_operations(isl_ctx *ctx);
+       void isl_ctx_reset_operations(isl_ctx *ctx);
+
 =head2 Values
 
 An C<isl_val> represents an integer value, a rational value
index 917260a..539fa74 100644 (file)
@@ -80,6 +80,7 @@ enum isl_error {
        isl_error_unknown,
        isl_error_internal,
        isl_error_invalid,
+       isl_error_quota,
        isl_error_unsupported
 };
 struct isl_ctx;
@@ -152,6 +153,10 @@ void isl_ctx_abort(isl_ctx *ctx);
 void isl_ctx_resume(isl_ctx *ctx);
 int isl_ctx_aborted(isl_ctx *ctx);
 
+void isl_ctx_set_max_operations(isl_ctx *ctx, unsigned long max_operations);
+unsigned long isl_ctx_get_max_operations(isl_ctx *ctx);
+void isl_ctx_reset_operations(isl_ctx *ctx);
+
 #define ISL_ARG_CTX_DECL(prefix,st,args)                               \
 st *isl_ctx_peek_ ## prefix(isl_ctx *ctx);
 
index 362e052..11537ee 100644 (file)
--- a/isl_ctx.c
+++ b/isl_ctx.c
@@ -168,6 +168,9 @@ isl_ctx *isl_ctx_alloc_with_options(struct isl_args *args, void *user_opt)
 
        ctx->error = isl_error_none;
 
+       ctx->operations = 0;
+       isl_ctx_set_max_operations(ctx, ctx->opt->max_operations);
+
        return ctx;
 error:
        isl_args_free(args, user_opt);
@@ -197,6 +200,13 @@ void isl_ctx_deref(struct isl_ctx *ctx)
        ctx->ref--;
 }
 
+/* Print statistics on usage.
+ */
+static void print_stats(isl_ctx *ctx)
+{
+       fprintf(stderr, "operations: %lu\n", ctx->operations);
+}
+
 void isl_ctx_free(struct isl_ctx *ctx)
 {
        if (!ctx)
@@ -206,6 +216,9 @@ void isl_ctx_free(struct isl_ctx *ctx)
                        "isl_ctx freed, but some objects still reference it",
                        return);
 
+       if (ctx->opt->print_stats)
+               print_stats(ctx);
+
        isl_hash_table_clear(&ctx->id_table);
        isl_blk_clear_cache(ctx);
        isl_int_clear(ctx->zero);
@@ -266,3 +279,28 @@ int isl_ctx_parse_options(isl_ctx *ctx, int argc, char **argv, unsigned flags)
                return -1;
        return isl_args_parse(ctx->user_args, argc, argv, ctx->user_opt, flags);
 }
+
+/* Set the maximal number of iterations of "ctx" to "max_operations".
+ */
+void isl_ctx_set_max_operations(isl_ctx *ctx, unsigned long max_operations)
+{
+       if (!ctx)
+               return;
+       ctx->max_operations = max_operations;
+}
+
+/* Return the maximal number of iterations of "ctx".
+ */
+unsigned long isl_ctx_get_max_operations(isl_ctx *ctx)
+{
+       return ctx ? ctx->max_operations : 0;
+}
+
+/* Reset the number of operations performed by "ctx".
+ */
+void isl_ctx_reset_operations(isl_ctx *ctx)
+{
+       if (!ctx)
+               return;
+       ctx->operations = 0;
+}
index 65e4665..67fb876 100644 (file)
@@ -26,4 +26,7 @@ struct isl_ctx {
        enum isl_error          error;
 
        int                     abort;
+
+       unsigned long           operations;
+       unsigned long           max_operations;
 };
index 7e96712..efeb261 100644 (file)
@@ -172,6 +172,10 @@ ISL_ARG_BOOL(struct isl_options, ast_build_allow_else, 0,
        "ast-build-allow-else", 1, "generate if statements with else branches")
 ISL_ARG_BOOL(struct isl_options, ast_build_allow_or, 0,
        "ast-build-allow-or", 1, "generate if conditions with disjunctions")
+ISL_ARG_BOOL(struct isl_options, print_stats, 0, "print-stats", 0,
+       "print statistics for every isl_ctx")
+ISL_ARG_ULONG(struct isl_options, max_operations, 0,
+       "max-operations", 0, "default number of maximal operations per isl_ctx")
 ISL_ARG_VERSION(print_version)
 ISL_ARGS_END
 
index b63eab0..bb73d68 100644 (file)
@@ -58,6 +58,9 @@ struct isl_options {
        int                     ast_build_scale_strides;
        int                     ast_build_allow_else;
        int                     ast_build_allow_or;
+
+       int                     print_stats;
+       unsigned long           max_operations;
 };
 
 #endif
index ea1f2d5..85afa0b 100644 (file)
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -1102,14 +1102,20 @@ int isl_tab_pivot(struct isl_tab *tab, int row, int col)
        int i, j;
        int sgn;
        int t;
+       isl_ctx *ctx;
        struct isl_mat *mat = tab->mat;
        struct isl_tab_var *var;
        unsigned off = 2 + tab->M;
 
-       if (tab->mat->ctx->abort) {
-               isl_ctx_set_error(tab->mat->ctx, isl_error_abort);
+       ctx = isl_tab_get_ctx(tab);
+       if (ctx->abort) {
+               isl_ctx_set_error(ctx, isl_error_abort);
                return -1;
        }
+       if (ctx->max_operations && ctx->operations >= ctx->max_operations)
+               isl_die(ctx, isl_error_quota,
+                       "maximal number of operations exceeded", return -1);
+       ctx->operations++;
 
        isl_int_swap(mat->row[row][0], mat->row[row][off + col]);
        sgn = isl_int_sgn(mat->row[row][0]);