From c2be2448c618bbc21ecaa35a681b684c2c802c88 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Wed, 11 Jan 2017 01:23:22 +0300 Subject: [PATCH] [LFSC] Fix performance issues, more determinism For certain proofs, the performance was drastically different on different OSes. The cause for this difference was a pointer comparison in the deduplication in `Expr::defeq()`. Depending on how the OS allocated the memory, an expression `a` would get replaced with an equivalent expression `b` or vice versa, which in turn affected performance of `Expr::free_in()` dramatically (sub-second vs. >5 min running times). This commit makes the process more deterministic by using a heuristic that favors symbolic expressions and greedily tries to make small refcounts smaller when replacing, and changes `Expr::free_in()` to not repeatedly explore the same subexpressions. --- proofs/lfsc_checker/expr.cpp | 51 +++++++++++++++++++++--------------- proofs/lfsc_checker/expr.h | 45 ++++++++++++++++++++++++------- 2 files changed, 65 insertions(+), 31 deletions(-) diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index 7bd26db2c..8c8120edb 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -190,7 +190,7 @@ Expr *Expr::clone() { } } } - return 0; // should never be reached + std::abort(); // should never be reached } @@ -281,7 +281,7 @@ Expr *Expr::collect_args(std::vector &args, bool follow_defs) { #endif } -Expr *Expr::get_head(bool follow_defs) { +Expr *Expr::get_head(bool follow_defs) const { CExpr *e = (CExpr *)this; while( e->getop() == APP ) { e = (CExpr *)e->kids[0]; @@ -291,7 +291,7 @@ Expr *Expr::get_head(bool follow_defs) { return e; } -Expr *Expr::get_body(int op, bool follow_defs) { +Expr *Expr::get_body(int op, bool follow_defs) const { CExpr *e = (CExpr *)this; while( e->getop() == op ) { e = (CExpr *)e->kids[2]; @@ -385,7 +385,6 @@ Expr* CExpr::convert_to_flat_app( Expr* e ) } bool Expr::defeq(Expr *e) { - /* we handle a few special cases up front, where this Expr might equal e, even though they have different opclass (i.e., different structure). */ @@ -579,7 +578,12 @@ bool Expr::defeq(Expr *e) { if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) ) return false; //--- optimization : replace child with equivalent pointer if was defeq - if( e1->kids[counter]kids[counter] ){ + // Heuristic: prefer symbolic kids because they may be cheaper to + // deal with (e.g. in free_in()). + if (e2->kids[counter]->isSymbolic() || + (!e1->kids[counter]->isSymbolic() && + e1->kids[counter]->getrefcnt() < + e2->kids[counter]->getrefcnt())) { e1->kids[counter]->dec(); e2->kids[counter]->inc(); e1->kids[counter] = e2->kids[counter]; @@ -601,33 +605,36 @@ bool Expr::defeq(Expr *e) { // already checked that both exprs have the same opclass. return true; } // switch(op1) - - return false; // never reached. + + std::abort(); // never reached. } int Expr::fiCounter = 0; -bool Expr::free_in(Expr *x) { - //fiCounter++; - //if( fiCounter%1==0 ) - // std::cout << fiCounter << std::endl; - switch(getop()) { - case NOT_CEXPR: +bool Expr::_free_in(Expr *x, expr_ptr_set_t *visited) { + // fiCounter++; + // if( fiCounter%1==0 ) + // std::cout << fiCounter << std::endl; + if (visited->find(this) != visited->end()) { + return false; + } + + switch (getop()) { + case NOT_CEXPR: switch (getclass()) { case HOLE_EXPR: { HoleExpr *h = (HoleExpr *)this; - if (h->val) - return h->val->free_in(x); + if (h->val) return h->val->_free_in(x, visited); return (h == x); } case SYMS_EXPR: case SYM_EXPR: { SymExpr *s = (SymExpr *)this; if (s->val && s->val->getclass() == HOLE_EXPR) - /* we do not need to follow the "val" pointer except in this - one case, when x is a hole (which we do not bother to check - here) */ - return s->val->free_in(x); + /* we do not need to follow the "val" pointer except in this + one case, when x is a hole (which we do not bother to check + here) */ + return s->val->_free_in(x, visited); return (s == x); } case INT_EXPR: @@ -641,15 +648,17 @@ bool Expr::free_in(Expr *x) { // fall through default: { // must be a CExpr + assert(this->getclass() == CEXPR); CExpr *e = (CExpr *)this; Expr *tmp; Expr **cur = e->kids; + visited->insert(this); while ((tmp = *cur++)) - if (tmp->free_in(x)) return true; + if (tmp->_free_in(x, visited)) return true; return false; } } - return false; // should not be reached + std::abort(); // should not be reached } void Expr::calc_free_in(){ diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index a461e847c..632aaa18a 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -1,12 +1,14 @@ #ifndef sc2__expr_h #define sc2__expr_h -#include "gmp.h" -#include -#include +#include +#include #include #include +#include +#include #include "chunking_memory_management.h" +#include "gmp.h" #define USE_FLAT_APP //AJR: off deprecated #define MARKVAR_32 @@ -52,8 +54,25 @@ enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR COMPARE }; +class Expr; class SymExpr; +namespace __gnu_cxx { +template <> +struct hash { + size_t operator()(const Expr *x) const { + return reinterpret_cast(x); + } +}; +} + +struct eqExprPtr { + bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; } +}; + +typedef __gnu_cxx::hash_set, eqExprPtr> + expr_ptr_set_t; + class Expr { protected: /* bits 0-2: Expr class @@ -62,8 +81,6 @@ protected: bits 9-31: ref count*/ int data; - void destroy(bool dec_kids); - enum { INC, DEC, CREATE }; void debugrefcnt(int ref, int what) { std::cout << "["; @@ -88,6 +105,8 @@ protected: : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) { } + bool _free_in(Expr *x, expr_ptr_set_t *visited); + public: virtual ~Expr() {} @@ -138,6 +157,9 @@ protected: inline bool isArithTerm() const { return getop() == ADD || getop() == NEG; } + inline bool isSymbolic() const { + return getclass() == SYM_EXPR || getclass() == SYMS_EXPR; + } static Expr *build_app(Expr *hd, const std::vector &args, int start = 0); @@ -149,9 +171,9 @@ protected: otherwise not. */ Expr *collect_args(std::vector &args, bool follow_defs = true); - Expr *get_head(bool follow_defs = true); + Expr *get_head(bool follow_defs = true) const; - Expr *get_body(int op = PI, bool follow_defs = true); + Expr *get_body(int op = PI, bool follow_defs = true) const; std::string toString(); @@ -167,11 +189,14 @@ protected: /* return a clone of this expr. All abstractions are really duplicated in memory. Other expressions may not actually be duplicated in memory, but their refcounts will be incremented. */ - Expr *clone(); + Expr *clone(); // x can be a SymExpr or a HoleExpr. - bool free_in(Expr *x); - bool get_free_in() { return data & 256; } + bool free_in(Expr *x) { + expr_ptr_set_t visited; + return _free_in(x, &visited); + } + bool get_free_in() const { return data & 256; } void calc_free_in(); static int cargCount; -- 2.30.2