[Tests] Use AspectJ to obtain the Worker thread results checked by JUnit tests

to not clutter TLC code with test-only API.

tlatools/.classpath

@@ -3,7 +3,7 @@
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
 	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
 	<classpathentry kind="src" path="src"/>
-	<classpathentry excluding="tlc2/tool/distributed/TLCServerMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/TLCServerMonitorAspect.aj" kind="src" path="src-aj"/>
+	<classpathentry excluding="tlc2/tool/WorkerMonitorAspect.aj|tlc2/tool/distributed/TLCServerMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/TLCServerMonitorAspect.aj" kind="src" path="src-aj"/>
 	<classpathentry kind="src" path="test"/>
 	<classpathentry kind="src" path="test-long"/>
 	<classpathentry kind="src" path="test-concurrent"/>

tlatools/build.ajproperties

-src.includes = src-aj/tlc2/tool/distributed/RMIMethodMonitorAspect.aj,\
+src.includes = src-aj/tlc2/tool/WorkerMonitorAspect.aj,\
+			   src-aj/tlc2/tool/distributed/RMIMethodMonitorAspect.aj,\
 			   src-aj/tlc2/tool/distributed/TLCServerMonitorAspect.aj

tlatools/customBuild.xml

@@ -63,6 +63,14 @@
 	</target>
 
 	<target name="compile" depends="clean" description="Compile">
+		<echo>
+			================================================================
+			= The following warnings about sun.misc.Unsafe can be ignored. = 
+			= OffHeapDiskFPSet has been written using Unsafe to best use   =
+			= a computer's memory. If Unsafe is removed from the JVM,      =
+			= OffHeapDiskFPSet won't work anymore.                         =
+			================================================================
+		</echo>
 		<!-- compile -->
 		<mkdir dir="${class.dir}" />
 		<javac srcdir="${src.dir}" destdir="${class.dir}" debug="true" verbose="false" source="1.5" target="1.5">
@@ -85,6 +93,13 @@
 	</target>
 	
 	<target name="compile-aj" depends="compile" if="withaj">
+		<echo>
+			====================================================================
+			= The following warnings (Xlint:adviceDidNotMatch) can be ignored. =
+			= We are doing load time weaving that kicks in when TLC gets       = 
+			= started, not when it is compiled.                                =
+			====================================================================
+		</echo>
 		<!-- compile aspectj related class files -->
 		<iajc destdir="${class.dir}" sourceRoots="${src-aj.dir}" debug="true" source="1.5" target="1.5">
 			<classpath refid="project.classpath" />
@@ -217,7 +232,7 @@
 		</javac>
 		<!-- copy class.dir to path with whitespace -->
 		<!-- this is required by some tests to make sense -->
-		<!-- even throw a non digit in -->
+		<!-- even throw a "+" and whitespace into the mix -->
 		<property name="ws.class.dir" value="TLA+ Tools" />
 		<copy todir="${ws.class.dir}">
 			<fileset dir="${class.dir}" />
@@ -277,6 +292,9 @@
 		<!-- run junit tests on tlatools.jar -->
 		<mkdir dir="${test.reports}/onJarLong" />
 		<junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="4096m" forkmode="perTest" fork="yes">
+			<jvmarg value="-javaagent:lib/aspectjweaver-1.8.5.jar" />
+			<sysproperty key="org.aspectj.weaver.showWeaveInfo" value="false"/>
+			<sysproperty key="aj.weaving.verbose" value="false"/>
 			<classpath refid="project.classpath" />
 			<classpath>
 				<pathelement location="lib/junit-4.8.2.jar" />
@@ -290,8 +308,8 @@
 				<fileset dir="${test.dir}-long">
 					<exclude name="**/MultiThreadedSpecTest.java"/>
 					
-					<!-- The following tests take way too long (hours) -->
-					<!-- Reactivate when you start working on the fingerprint sets -->
+					<!-- The following tests take way too long (hours). -->
+					<!-- Reactivate when you start working on the fingerprint sets! -->
 					<exclude name="**/DiskFPSetTest.java"/>
 					<exclude name="**/FPSetTest.java"/>
 					<exclude name="**/MSBDiskFPSetTest.java"/>

tlatools/src-aj/META-INF/aop-ajc.xml

@@ -2,6 +2,7 @@
 <aspectj>
 
 	<aspects>
+		<aspect name="tlc2.tool.WorkerMonitorAspect"/>
 		<aspect name="tlc2.tool.distributed.RMIMethodMonitorAspect"/>
 		<aspect name="tlc2.tool.distributed.TLCServerMonitorAspect"/>
 	</aspects>

tlatools/src-aj/META-INF/aop.xml

@@ -2,6 +2,7 @@
 <aspectj>
 
 	<aspects>
+		<aspect name="tlc2.tool.WorkerMonitorAspect"/>
 		<aspect name="tlc2.tool.distributed.RMIMethodMonitorAspect"/>
 		<aspect name="tlc2.tool.distributed.TLCServerMonitorAspect"/>
 	</aspects>

tlatools/src-aj/tlc2/tool/WorkerMonitor.java

+package tlc2.tool;
+
+import java.util.HashSet;
+import java.util.Set;
+
+public class WorkerMonitor {
+
+	private static final Set<ThreadListener> listeners = new HashSet<ThreadListener>();
+	
+	public static void addPerformanceResult(final Thread thread, final long runningTime) {
+		for (ThreadListener threadListener : listeners) {
+			threadListener.terminated(thread, runningTime);
+		}
+	}
+
+	public static void addThreadListener(ThreadListener threadListener) {
+		listeners.add(threadListener);
+	}
+	
+	
+	/**
+	 * A ThreadListener is notified of when the Worker thread terminates. The
+	 * notification includes the execution time of the thread.
+	 */
+	public static interface ThreadListener {
+
+		void terminated(final Thread thread, final long runningTime);
+	}
+}

tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj

+package tlc2.tool;
+
+
+public aspect WorkerMonitorAspect perthis(callToRunMethod()) {
+	
+	private long threadStartTime, threadEndTime;
+	
+	pointcut callToRunMethod() : 
+		   execution(* tlc2.tool.Worker.run(..));
+	
+	before(): (callToRunMethod()) {
+		threadStartTime = System.currentTimeMillis();
+	}
+
+	after(): (callToRunMethod()) {
+		threadEndTime = System.currentTimeMillis();
+		WorkerMonitor.addPerformanceResult((Worker) thisJoinPoint.getTarget(), (threadEndTime - threadStartTime));
+	}
+//	
+//	pointcut callToSetUpMethod() :
+//		execution(* tlc2.tool.liveness.MultiThreadedSpecTest.setUp());
+//	
+//	before(): (callToSetUpMethod()) {
+//		Object target = thisJoinPoint.getTarget();
+//		System.out.println("SetUp pc: " + target);
+//	}
+}

tlatools/src/tlc2/tool/Worker.java

@@ -5,9 +5,6 @@
 
 package tlc2.tool;
 
-import java.util.HashSet;
-import java.util.Set;
-
 import tlc2.output.EC;
 import tlc2.output.MP;
 import tlc2.tool.queue.IStateQueue;
@@ -17,12 +14,6 @@ import tlc2.value.Value;
 
 public class Worker extends IdThread implements IWorker {
 	
-	private static final Set<ThreadListener> THREAD_LISTENERS = new HashSet<ThreadListener>();
-	
-	public static void addThreadListener(ThreadListener listener) {
-		THREAD_LISTENERS.add(listener);
-	}
-	
 	/**
 	 * Multi-threading helps only when running on multiprocessors. TLC can
 	 * pretty much eat up all the cycles of a processor running single threaded.
@@ -69,7 +60,6 @@ public class Worker extends IdThread implements IWorker {
    * updates the state set and state queue.
 	 */
 	public final void run() {
-		final long startTime = System.currentTimeMillis();
 		TLCState curState = null;
 		try {
 			while (true) {
@@ -97,19 +87,6 @@ public class Worker extends IdThread implements IWorker {
 				this.tlc.notify();
 			}
 			return;
-		} finally {
-			for (ThreadListener listener : THREAD_LISTENERS) {
-				listener.terminated(this, System.currentTimeMillis() - startTime);
-			}
 		}
 	}
-	
-	/**
-	 * A ThreadListener is notified of when the Worker thread terminates. The
-	 * notification includes the execution time of the thread.
-	 */
-	public static interface ThreadListener {
-
-		void terminated(final Thread thread, final long runningTime);
-	}
 }

tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java

@@ -38,7 +38,7 @@ import java.util.concurrent.TimeoutException;
 
 import tlc2.output.EC;
 import tlc2.tool.AbstractChecker;
-import tlc2.tool.Worker;
+import tlc2.tool.WorkerMonitor;
 
 /**
  * This test takes about four minutes with 32 cores on an EC2 cr1.8xlarge instance.
@@ -94,7 +94,29 @@ public abstract class MultiThreadedSpecTest extends ModelCheckerTestCase {
 		latch.await(10, TimeUnit.SECONDS);
 
 		// Except as many results as we have started worker threads.
-		assertEquals(getNumberOfThreads(), performanceResults.size());
+		//
+		// If this assert fails, make sure that AspectJ is loaded and the
+		// WorkerMonitorAspect is woven. This is done automatically by the ant
+		// build (customBuild.xml) but not when this test is executed inside
+		// Eclipse. AJDT (the AspectJ development tools) should not be a general
+		// requirement to compile the tlatools/ project in Eclipse.
+		//
+		// If you ask why it uses AspectJ the first place... Rather than adding
+		// API to the TLC code making in more and more complex just to test its
+		// performance behavior, I deemed the extra test complexity caused by
+		// AspectJ acceptable. We trade less complexity in program code with
+		// higher complexity in test code.
+		//
+		// To run this test in Eclipse, install AJDT (http://eclipse.org/ajdt/),
+		// convert the tlatools/ project into an AspectJ project via the 
+		// Package Explorers context menu and add 
+		// "-javaagent:${project_loc:tlatools}/lib/aspectjweaver-1.8.5.jar" 
+		// as a program argument to your JUnit launch config.
+		//
+		// If you get some but not all results, it's most certainly unrelated to
+		// AspectJ and indicates a programming bug.
+		assertEquals("PerfResult size is 0? => Is AspectJ load time weaving enabled?", getNumberOfThreads(),
+				performanceResults.size());
 		
 		// None of the workers threads should have been blocked or waiting for
 		// more than 25%
@@ -121,10 +143,10 @@ public abstract class MultiThreadedSpecTest extends ModelCheckerTestCase {
 
 		// Register a listener hot for the termination of the TLC worker
 		// threads. 
-		// Using ThreadMXBean to lookup all threads after TLC has
-		// finished has the potential that the JVM deleted the worker threads
+		// Using ThreadMXBean directly to lookup all threads after TLC has
+		// finished has the potential that the JVM deletes the worker threads
 		// before this test gets a chance to collect statistics.
-		Worker.addThreadListener(new Worker.ThreadListener() {
+		WorkerMonitor.addThreadListener(new WorkerMonitor.ThreadListener() {
 			public synchronized void terminated(final Thread thread, final long runningTime) {
 				final ThreadInfo threadInfo = threadBean.getThreadInfo(thread.getId());
 				double d = threadInfo.getBlockedTime() / (runningTime * 1.0d);