[Javabdd-checkins] JavaBDD/buddy/src bddop.c,1.4,1.5

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Update of /cvsroot/javabdd/JavaBDD/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7897/buddy/src

Modified Files:
	bddop.c 
Log Message:
For whatever reason, the recursive functions are quite a bit faster than the iterative ones !?

using and_itr, relprod_itr : 248s
using and_rec, relprod_itr : 238s
using and_rec, relprod_rec : 233s

Also introduced a few more prefetch instructions.

Index: bddop.c
===================================================================
RCS file: /cvsroot/javabdd/JavaBDD/buddy/src/bddop.c,v
retrieving revision 1.4
retrieving revision 1.5
diff -C2 -d -r1.4 -r1.5
*** bddop.c	1 Oct 2004 02:17:20 -0000	1.4
--- bddop.c	1 Oct 2004 04:03:23 -0000	1.5
***************
*** 159,162 ****
--- 159,163 ----
  #if defined(SPECIALIZE_AND)
  static BDD    and_rec(BDD, BDD);
+ static BDD    and_itr(BDD, BDD);
  #endif
  #if defined(SPECIALIZE_RELPROD)
***************
*** 774,778 ****
--- 775,782 ----
       return l;

+    /* Prefetch nodes to get some concurrency between cache lookup
+       and node table lookup. */
     _mm_prefetch(&bddnodes[l], 0);
+    _mm_prefetch(&bddnodes[r], 0);

     entry = BddCache_lookup(&andcache, ANDHASH(l,r));
***************
*** 817,820 ****
--- 821,926 ----
     return res;
  }
+ 
+ static BDD and_itr(BDD l0, BDD r0)
+ {
+   BDD res;
+   int* s_top;
+   int* s_ptr;
+   s_top = s_ptr = alloca(bddvarnum * sizeof(int) * 9);
+   *s_ptr++ = l0;
+   *s_ptr++ = r0;
+   
+   while (s_top != s_ptr) {
+     int hash, lev;
+     BDD l1, r1, res1;
+     BddCacheData3 *entry;
+   outer:
+     r1 = *(--s_ptr);
+     l1 = *(--s_ptr);
+     if (l1 == r1  ||  ISONE(r1)) {
+       res1 = l1;
+     } else if (ISZERO(l1)  ||  ISZERO(r1)) {
+       res1 = 0;
+     } else if (ISONE(l1)) {
+       res1 = r1;
+     } else {
+ 
+       /* Prefetch nodes to get some concurrency between cache lookup
+ 	 and node table lookup. */
+       _mm_prefetch(&bddnodes[l1], 0);
+       _mm_prefetch(&bddnodes[r1], 0);
+ 
+       entry = BddCache_lookup(&andcache, ANDHASH(l1,r1));
+       if (entry->a == l1  &&  entry->b == r1) {
+ #ifdef CACHESTATS
+ 	bddcachestats.opHit++;
+ #endif
+ 	res1 = entry->res;
+       } else {
+ #ifdef CACHESTATS
+ 	bddcachestats.opMiss++;
+ #endif
+ 	*s_ptr++ = l1;
+ 	*s_ptr++ = r1;
+ 	*s_ptr++ = (int)(entry - andcache.table);
+ 	if (LEVEL(l1) == LEVEL(r1)) {
+ 	  *s_ptr++ = LEVEL(l1);
+ 	  *s_ptr++ = HIGH(l1);
+ 	  *s_ptr++ = HIGH(r1);
+ 	  *s_ptr++ = -1;
+ 	  *s_ptr++ = LOW(l1);
+ 	  *s_ptr++ = LOW(r1);
+ 	  continue;
+ 	} else if (LEVEL(l1) < LEVEL(r1)) {
+ 	  *s_ptr++ = LEVEL(l1);
+ 	  *s_ptr++ = HIGH(l1);
+ 	  *s_ptr++ = r1;
+ 	  *s_ptr++ = -1;
+ 	  *s_ptr++ = LOW(l1);
+ 	  *s_ptr++ = r1;
+ 	  continue;
+ 	} else {
+ 	  *s_ptr++ = LEVEL(r1);
+ 	  *s_ptr++ = l1;
+ 	  *s_ptr++ = HIGH(r1);
+ 	  *s_ptr++ = -1;
+ 	  *s_ptr++ = l1;
+ 	  *s_ptr++ = LOW(r1);
+ 	  continue;
+ 	}
+       }
+     }
+     if (s_top == s_ptr) {
+       res = res1;
+       goto end;
+     }
+     PUSHREF(res1);
+     for (;;) {
+       lev = *(--s_ptr);
+       if (lev < 0) {
+         goto outer;
+       }
+       hash =  *(--s_ptr);
+       r1 =  *(--s_ptr);
+       l1 =  *(--s_ptr);
+       entry = &andcache.table[hash];
+       res1 = bdd_makenode(lev, READREF(2), READREF(1));
+       POPREF(2);
+       
+       entry->a = l1;
+       entry->b = r1;
+       entry->res = res1;
+       
+       if (s_top == s_ptr) {
+         res = res1;
+         goto end;
+       }
+       
+       PUSHREF(res1);
+     }
+   }
+  end:
+   return res;
+ }
  #endif

***************
*** 835,838 ****
--- 941,949 ----
       return l;

+    /* Prefetch nodes to get some concurrency between cache lookup
+       and node table lookup. */
+    _mm_prefetch(&bddnodes[l], 0);
+    _mm_prefetch(&bddnodes[r], 0);
+ 
     entry = BddCache_lookup(&orcache, ORHASH(l,r));

***************
*** 2314,2318 ****
         return bdd_error(BDD_MEMORY);
  #endif
!     return relprod_itr(l, r);
    }
  #endif
--- 2425,2429 ----
         return bdd_error(BDD_MEMORY);
  #endif
!     return relprod_rec(l, r);
    }
  #endif
***************
*** 2445,2448 ****
--- 2556,2562 ----
       return quant_rec(r);

+    /* Prefetch LOW(l) to get some concurrency between cache lookup
+       and node table lookup.  LOW(l) is not that expensive because we
+       need to load LEVEL(l) right after this anyway. */
     _mm_prefetch(&bddnodes[LOW(l)], 0);

***************
*** 2532,2580 ****
      } else if (l1 == 1) {
        res1 = quant_rec(r1);
!     } else if (LEVEL(l1) > quantlast  &&  LEVEL(r1) > quantlast) {
!       applyop = bddop_and;
  #if defined(SPECIALIZE_AND)
!       res1 = and_rec(l1,r1);
  #else
!       res1 = apply_rec(l1,r1);
  #endif
!       applyop = bddop_or;
!     } else {
!       entry = BddCache_lookup(&appexcache, APPEXHASH(l1,r1,bddop_and));
!       if (entry->a == l1  &&  entry->b == r1  &&  entry->r.c == appexid) {
!         res1 = entry->r.res;
!       } else if (LEVEL(l1) == LEVEL(r1)) {
!         *s_ptr++ = l1;
!         *s_ptr++ = r1;
!         *s_ptr++ = (int)(entry - appexcache.table);
!         *s_ptr++ = LEVEL(l1);
!         *s_ptr++ = HIGH(l1);
!         *s_ptr++ = HIGH(r1);
!         *s_ptr++ = -1;
!         *s_ptr++ = LOW(l1);
!         *s_ptr++ = LOW(r1);
!         continue;
!       } else if (LEVEL(l1) < LEVEL(r1)) {
!         *s_ptr++ = l1;
!         *s_ptr++ = r1;
!         *s_ptr++ = (int)(entry - appexcache.table);
!         *s_ptr++ = LEVEL(l1);
!         *s_ptr++ = HIGH(l1);
!         *s_ptr++ = r1;
!         *s_ptr++ = -1;
!         *s_ptr++ = LOW(l1);
!         *s_ptr++ = r1;
!         continue;
        } else {
!         *s_ptr++ = l1;
!         *s_ptr++ = r1;
!         *s_ptr++ = (int)(entry - appexcache.table);
!         *s_ptr++ = LEVEL(r1);
!         *s_ptr++ = l1;
!         *s_ptr++ = HIGH(r1);
!         *s_ptr++ = -1;
!         *s_ptr++ = l1;
!         *s_ptr++ = LOW(r1);
!         continue;
        }
      }
--- 2646,2704 ----
      } else if (l1 == 1) {
        res1 = quant_rec(r1);
!     } else {
! 
!       /* Prefetch LOW(l1) to get some concurrency between cache lookup
! 	 and node table lookup.  LOW(l1) is not that expensive because we
! 	 need to load LEVEL(l1) right after this anyway. */
!       _mm_prefetch(&bddnodes[LOW(l1)], 0);
! 
!       if (LEVEL(l1) > quantlast  &&  LEVEL(r1) > quantlast) {
! 	applyop = bddop_and;
  #if defined(SPECIALIZE_AND)
! 	res1 = and_rec(l1,r1);
  #else
! 	res1 = apply_rec(l1,r1);
  #endif
! 	applyop = bddop_or;
        } else {
! 	entry = BddCache_lookup(&appexcache, APPEXHASH(l1,r1,bddop_and));
! 	if (entry->a == l1  &&  entry->b == r1  &&  entry->r.c == appexid) {
! #ifdef CACHESTATS
! 	  bddcachestats.opHit++;
! #endif
! 	  res1 = entry->r.res;
! 	} else {
! #ifdef CACHESTATS
! 	  bddcachestats.opMiss++;
! #endif
! 	  *s_ptr++ = l1;
! 	  *s_ptr++ = r1;
! 	  *s_ptr++ = (int)(entry - appexcache.table);
! 	  if (LEVEL(l1) == LEVEL(r1)) {
! 	    *s_ptr++ = LEVEL(l1);
! 	    *s_ptr++ = HIGH(l1);
! 	    *s_ptr++ = HIGH(r1);
! 	    *s_ptr++ = -1;
! 	    *s_ptr++ = LOW(l1);
! 	    *s_ptr++ = LOW(r1);
! 	    continue;
! 	  } else if (LEVEL(l1) < LEVEL(r1)) {
! 	    *s_ptr++ = LEVEL(l1);
! 	    *s_ptr++ = HIGH(l1);
! 	    *s_ptr++ = r1;
! 	    *s_ptr++ = -1;
! 	    *s_ptr++ = LOW(l1);
! 	    *s_ptr++ = r1;
! 	    continue;
! 	  } else {
! 	    *s_ptr++ = LEVEL(r1);
! 	    *s_ptr++ = l1;
! 	    *s_ptr++ = HIGH(r1);
! 	    *s_ptr++ = -1;
! 	    *s_ptr++ = l1;
! 	    *s_ptr++ = LOW(r1);
! 	    continue;
! 	  }
! 	}
        }
      }