diff --git a/tlatools/.classpath b/tlatools/.classpath index fd9cc77553e8417275d5c6a865aa7a5ac1a1d297..291e0fbfbba1d9cf4b93def65b357039d1bc9269 100644 --- a/tlatools/.classpath +++ b/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"/> diff --git a/tlatools/build.ajproperties b/tlatools/build.ajproperties index 720d23e719c760ed2bf639c20b76a167a95344a3..f81d23bbe290c85cac34a298e066f4d4fd6dddfd 100644 --- a/tlatools/build.ajproperties +++ b/tlatools/build.ajproperties @@ -1,2 +1,3 @@ -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 diff --git a/tlatools/customBuild.xml b/tlatools/customBuild.xml index 4b995b7bdceb8b4f51d9faa041354923eb4d4257..6abfe89dc05bef5fe57f68955b508426e5232502 100644 --- a/tlatools/customBuild.xml +++ b/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"> @@ -83,13 +91,20 @@ </fileset> </copy> </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" /> <classpath> - <pathelement location="lib/aspectjrt-1.8.5.jar" /> + <pathelement location="lib/aspectjrt-1.8.5.jar" /> <pathelement location="lib/aspectjtools-1.8.5.jar" /> <pathelement path="${class.dir}" /> </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"/> diff --git a/tlatools/src-aj/META-INF/aop-ajc.xml b/tlatools/src-aj/META-INF/aop-ajc.xml index efef8819df18c47c2226043f838929db52c92a08..c425d69c2e85a51b25349b374bea97f310a8b088 100644 --- a/tlatools/src-aj/META-INF/aop-ajc.xml +++ b/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> diff --git a/tlatools/src-aj/META-INF/aop.xml b/tlatools/src-aj/META-INF/aop.xml index efef8819df18c47c2226043f838929db52c92a08..c425d69c2e85a51b25349b374bea97f310a8b088 100644 --- a/tlatools/src-aj/META-INF/aop.xml +++ b/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> diff --git a/tlatools/src-aj/tlc2/tool/WorkerMonitor.java b/tlatools/src-aj/tlc2/tool/WorkerMonitor.java new file mode 100644 index 0000000000000000000000000000000000000000..e8e57d5c41fe2846c05894110faebee9e967eb7d --- /dev/null +++ b/tlatools/src-aj/tlc2/tool/WorkerMonitor.java @@ -0,0 +1,29 @@ +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); + } +} diff --git a/tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj b/tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj new file mode 100644 index 0000000000000000000000000000000000000000..7835e4a074a32e54fc1b7866c37b32f8afec3a4a --- /dev/null +++ b/tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj @@ -0,0 +1,27 @@ +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); +// } +} diff --git a/tlatools/src/tlc2/tool/Worker.java b/tlatools/src/tlc2/tool/Worker.java index b655ad27aeffae4d645445d01331d158b3d40194..3b98529ead182a74fc13c6b90bf1f0f5fc473a86 100644 --- a/tlatools/src/tlc2/tool/Worker.java +++ b/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); - } } diff --git a/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java b/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java index d45289d056d938633c4e5ccbedac59366892448b..f8cc0af6a178a955ea4e401a05867256e82361f4 100644 --- a/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java +++ b/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);