[abc] Update on Aprove

Hello.

I have done several more aprove runs tonight and came to the following results:

1.) TM without indexing is infeasibly slow. Usually Aprove proves the first term rewriting system to be terminating after about 28 seconds in the plain version. With TM and indexing on this takesa few seconds longer. With TM and indexing *off*, it does not even manage to do so after over 90 minutes of time! So this is really a difference in several orders of magnitude. Due to this result, I have marked the correspinding cell in the table in the paper with "star".

I used hprof to make sure that not anything weird is going on but it really seemed that the vast majority of time is spent in hashing operations. So it _is_ a huge slowdown but it seems "normal". So really a great argument for indexing, I suppose...

This is the indexing info that is printed when indexing is on:

State machine:
==============
Initial State 0 (needStrongRefs[hashCode], collectableWeakRefs[s, o], weakRefs[], boundVars[])
  -->[add] to State 1
State 1 (needStrongRefs[hashCode], collectableWeakRefs[s, o], weakRefs[], boundVars[s, o, hashCode])
  -->[doesContain] to State 2
  -->[SKIP] to State 1
Final State 2 (needStrongRefs[o, hashCode], collectableWeakRefs[], weakRefs[s], boundVars[s, o, hashCode])

State 1
 - collectable indices: [o, s]
 - primitive indices: []
 - weak indices: []
 - other indices: []

So if I read this correctly, you index first on the object o and then on the set s. But probably the Oxford guys can better comment on this.

2.) When I use indexing but turn off the use of collectable weak refs, Aprove runs to about 900MB memory consumption in less than a minute but then just stalls! This looks really strange: It does not show up in "top", i.e. does not really seem to do a lot. Neither do I get an OutOfMemoryError. Again, I used hprof to find out what's going on and this is the result:

CPU SAMPLES BEGIN (total = 3858) Mon Mar 13 08:00:28 2006
rank self accum count trace method
   1 9.54% 9.54% 368 300559 java.lang.Object.notify
   2 8.63% 18.17% 333 300414 java.lang.Throwable.fillInStackTrace
   3 5.50% 23.67% 212 300265 java.lang.System.identityHashCode
   4 5.00% 28.67% 193 300347 java.lang.System.identityHashCode
   5 3.94% 32.61% 152 300430 aprove.Framework.Algebra.Terms.Term.matches
   6 2.54% 35.15% 98 300427 aprove.Framework.Algebra.Terms.Term.matches
   7 2.28% 37.43% 88 300548 java.lang.Object.notify
   8 1.84% 39.27% 71 300577 java.lang.Object.notify
   9 1.50% 40.77% 58 300557 java.lang.Object.notify
  10 1.50% 42.28% 58 300564 java.lang.Object.notify
  11 1.43% 43.70% 55 300550 java.lang.Object.notify
  12 1.40% 45.10% 54 300366 java.lang.Object.notify
  13 1.35% 46.45% 52 300321 java.lang.System.identityHashCode
  14 1.27% 47.72% 49 300563 java.lang.Object.notify
  15 0.86% 48.57% 33 300343 java.lang.Object.notify
  16 0.86% 49.43% 33 300562 java.lang.Object.notify
  17 0.83% 50.26% 32 300419 java.lang.Thread.currentThread
  18 0.83% 51.09% 32 300715 java.lang.Object.notify
  19 0.75% 51.84% 29 300415 java.lang.Object.notify
  20 0.73% 52.57% 28 300578 java.lang.Object.notify
  21 0.70% 53.27% 27 300800 aprove.Framework.Algebra.Terms.Term.solveUP

As you can see, almost all the time is spent in locking! And this is locking induced by us! More specifically, at this point:

org.aspectbench.tm.runtime.internal.Lock.release(Lock.java:42)

If I understand the conversation on AJHotDraw correctly, this was showing a similar at some point. I really have no clue while this happens, but apparently at some point, it slows down the system to infinity or maybe (given that it does not show up in "top") it even deadlocks it - I am not 100% sure here.

3.) The numbers that I *did* get, are checked in and look as follows:

Plain (no aspect):
345.0s

Native AJ aspect:
485.8s

Tracematch with indexing on:
845.0s

So I guess I will no turn over to Jigsaw / LOR.

Eric

--
Eric Bodden
Sable Research Group
McGill University, Montréal, Canada