[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.

diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 7bd26db2cde89ae7a40d1da226bb51cd5a33ec42..8c8120edb3e374aeadcf529d38fe8bc03bbf7fae 100644 (file)
--- 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<Expr *> &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]<e2->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 a461e847c0bdb1e21abf436c070b64a81c21c07c..632aaa18afc859601a190b3eee90f0382529ceba 100644 (file)
--- 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 <string>
-#include <vector>
+#include <stdint.h>
+#include <ext/hash_set>
 #include <iostream>
 #include <map>
+#include <string>
+#include <vector>
 #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<Expr *> {
+  size_t operator()(const Expr *x) const {
+    return reinterpret_cast<uintptr_t>(x);
+  }
+};
+}
+
+struct eqExprPtr {
+  bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; }
+};
+
+typedef __gnu_cxx::hash_set<Expr *, __gnu_cxx::hash<Expr *>, 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<Expr *> &args, 
                         int start = 0);
@@ -149,9 +171,9 @@ protected:
      otherwise not. */
   Expr *collect_args(std::vector<Expr *> &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;