Mercurial > hg > Members > kono > jpf-core
changeset 24:6774e2e08d37
the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up
In the wake of nested locks, there were a number of cases to fix that implicitly relied on absent clinits because clients were not properly checking for re-execution (most notably java.util.Exchanger). This mostly came in through MJIEnv.newObject/ElementInfo. We might turn ClinitRequired into a handled exception at some point, to catch such cases during compilation.
Added a UnknownJPFClass exception (in analogy to ClinitRequired), to make clients aware of failed class load attempts/reasons.
fixed Exchanger peer, which was not giving up the lock when timing out. This is an example of a lockfree wait op that can time out. Basically, ThreadInfo.isWaiting() needs to be complemented by a isWaitingOrTimedOut(), and ElementInfo.notifies0() has to be aware of it
fixed NPE when setting report.probe_interval in tests, which was missing that it had to create a stat object
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/.idea/codeStyleSettings.xml Tue Apr 21 00:34:15 2015 -0700 @@ -0,0 +1,13 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project version="4"> + <component name="ProjectCodeStyleSettingsManager"> + <option name="PER_PROJECT_SETTINGS"> + <value> + <XML> + <option name="XML_LEGACY_SETTINGS_IMPORTED" value="true" /> + </XML> + </value> + </option> + <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default (1)" /> + </component> +</project> \ No newline at end of file
--- a/jpf.properties Wed Apr 15 22:40:21 2015 -0700 +++ b/jpf.properties Tue Apr 21 00:34:15 2015 -0700 @@ -301,6 +301,17 @@ # if this is set to true, overriden finalize() methods execute upon objects garbage collections vm.process_finalizers = false + +### jvm specifics + +# di=o we model nested locks during class init (to detect possible hotspot dealocks during init) +# (off by default since it can cause state explosion) +jvm.nested_init=false + +# if so, for which classes (default is to exclude system classes) +jvm.nested_init.exclude=java.*,javax.*,sun.misc.* + + ############################### 3. CG part ############################### # choice randomization policy in effect:
--- a/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/JVMClassInfo.java Tue Apr 21 00:34:15 2015 -0700 @@ -18,34 +18,11 @@ package gov.nasa.jpf.jvm; +import gov.nasa.jpf.Config; import gov.nasa.jpf.util.Misc; -import gov.nasa.jpf.vm.AbstractTypeAnnotationInfo; -import gov.nasa.jpf.vm.AnnotationInfo; -import gov.nasa.jpf.vm.BootstrapMethodInfo; -import gov.nasa.jpf.vm.BytecodeAnnotationInfo; -import gov.nasa.jpf.vm.BytecodeTypeParameterAnnotationInfo; -import gov.nasa.jpf.vm.ClassInfo; -import gov.nasa.jpf.vm.ClassLoaderInfo; -import gov.nasa.jpf.vm.ClassParseException; -import gov.nasa.jpf.vm.DirectCallStackFrame; -import gov.nasa.jpf.vm.ExceptionHandler; -import gov.nasa.jpf.vm.ExceptionParameterAnnotationInfo; -import gov.nasa.jpf.vm.FieldInfo; -import gov.nasa.jpf.vm.FormalParameterAnnotationInfo; -import gov.nasa.jpf.vm.GenericSignatureHolder; -import gov.nasa.jpf.vm.InfoObject; -import gov.nasa.jpf.vm.LocalVarInfo; -import gov.nasa.jpf.vm.MethodInfo; -import gov.nasa.jpf.vm.NativeMethodInfo; -import gov.nasa.jpf.vm.StackFrame; -import gov.nasa.jpf.vm.SuperTypeAnnotationInfo; -import gov.nasa.jpf.vm.ThreadInfo; -import gov.nasa.jpf.vm.ThrowsAnnotationInfo; -import gov.nasa.jpf.vm.TypeAnnotationInfo; -import gov.nasa.jpf.vm.TypeParameterAnnotationInfo; -import gov.nasa.jpf.vm.TypeParameterBoundAnnotationInfo; -import gov.nasa.jpf.vm.Types; -import gov.nasa.jpf.vm.VariableAnnotationInfo; +import gov.nasa.jpf.util.StringSetMatcher; +import gov.nasa.jpf.vm.*; + import java.lang.reflect.Modifier; import java.util.HashMap; import java.util.LinkedHashMap; @@ -610,7 +587,22 @@ } } } - + + // since nested class init locking can explode the state space, we make it optional and controllable + protected static boolean nestedInit; + protected static StringSetMatcher includeNestedInit; + protected static StringSetMatcher excludeNestedInit; + + protected static boolean init (Config config){ + nestedInit = config.getBoolean("jvm.nested_init", false); + if (nestedInit){ + includeNestedInit = StringSetMatcher.getNonEmpty(config.getStringArray("jvm.nested_init.include")); + excludeNestedInit = StringSetMatcher.getNonEmpty(config.getStringArray("jvm.nested_init.exclude")); + } + + return true; + } + JVMClassInfo (String name, ClassLoaderInfo cli, ClassFile cf, String srcUrl, JVMCodeBuilder cb) throws ClassParseException { super( name, cli, srcUrl); @@ -668,7 +660,79 @@ // the interfaces are already loaded. } } - + + /** + * perform initialization of this class and its not-yet-initialized superclasses (top down), + * which includes calling clinit() methods + * + * This is overridden here to model a questionable yet consequential behavior of hotspot, which + * is holding derived class locks when initializing base classes. The generic implementation in + * ClassInfo uses non-nested locks (i.e. A.clinit() only synchronizes on A.class) and hence cannot + * produce the same static init deadlocks as hotspot. In order to catch such defects we implement + * nested locking here. + * + * The main difference is that the generic implementation only pushes DCSFs for required clinits + * and otherwise doesn't lock anything. Here, we create one static init specific DCSF which wraps + * all clinits in nested monitorenter/exits. We create this even if there is no clinit so that we + * mimic hotspot locking. + * + * Note this scheme also enables us to get rid of the automatic clinit sync (they don't have + * a 0x20 sync modifier in classfiles) + * + * @return true if client needs to re-execute because we pushed DirectCallStackFrames + */ + @Override + public boolean initializeClass(ThreadInfo ti) { + if (needsInitialization(ti)) { + if (nestedInit && StringSetMatcher.isMatch(name, includeNestedInit, excludeNestedInit)) { + registerClass(ti); // this is recursively upwards + int nOps = 2 * (getNumberOfSuperClasses() + 1); // this is just an upper bound for the number of operands we need + + MethodInfo miInitialize = new MethodInfo("[initializeClass]", "()V", Modifier.STATIC, 0, nOps); + JVMDirectCallStackFrame frame = new JVMDirectCallStackFrame(miInitialize, null); + JVMCodeBuilder cb = getSystemCodeBuilder(null, miInitialize); + + addClassInit(ti, frame, cb); // this is recursively upwards until we hit a initialized superclass + cb.directcallreturn(); + cb.installCode(); + + // this is normally initialized in the ctor, but at that point we don't have the code yet + frame.setPC(miInitialize.getFirstInsn()); + + ti.pushFrame(frame); + return true; // client has to re-execute, we pushed a stackframe + + + } else { // use generic initialization without nested locks (directly calling clinits) + return super.initializeClass(ti); + } + + } else { + return false; // nothing to do + } + } + + protected void addClassInit (ThreadInfo ti, JVMDirectCallStackFrame frame, JVMCodeBuilder cb){ + int clsObjRef = getClassObjectRef(); + + frame.pushRef(clsObjRef); + cb.monitorenter(); + + if (superClass != null && superClass.needsInitialization(ti)) { + ((JVMClassInfo) superClass).addClassInit(ti, frame, cb); // go recursive + } + + if (getMethod("<clinit>()V", false) != null) { // do we have a clinit + cb.invokeclinit(this); + } else { + cb.finishclinit(this); + // we can't just do call ci.setInitialized() since that has to be deferred + } + + frame.pushRef(clsObjRef); + cb.monitorexit(); + } + //--- call processing protected JVMCodeBuilder getSystemCodeBuilder (ClassFile cf, MethodInfo mi){
--- a/src/main/gov/nasa/jpf/jvm/JVMCodeBuilder.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/JVMCodeBuilder.java Tue Apr 21 00:34:15 2015 -0700 @@ -88,7 +88,11 @@ Instruction[] a = code.toArray( new Instruction[code.size()]); mi.setCode(a); } - + + public int getCodeSize(){ + return code.size(); + } + //--- the factory methods @Override public void aconst_null() { @@ -996,13 +1000,13 @@ Object v = cf.getCpValue(cpIntOrFloatOrStringOrClassIndex); switch (cf.getCpTag(cpIntOrFloatOrStringOrClassIndex)){ case ClassFile.CONSTANT_INTEGER: - add( insnFactory.ldc_w((Integer)v)); break; + add( insnFactory.ldc_w((Integer) v)); break; case ClassFile.CONSTANT_FLOAT: - add( insnFactory.ldc_w((Float)v)); break; + add( insnFactory.ldc_w((Float) v)); break; case ClassFile.CONSTANT_STRING: - add( insnFactory.ldc_w((String)v, false)); break; + add( insnFactory.ldc_w((String) v, false)); break; case ClassFile.CONSTANT_CLASS: - add( insnFactory.ldc_w((String)v, true)); break; + add( insnFactory.ldc_w((String) v, true)); break; } pc+=3; } @@ -1290,6 +1294,11 @@ pc++; } + public void finishclinit (ClassInfo ci){ + add (insnFactory.finishclinit(ci)); + pc++; + } + public void directcallreturn(){ add( insnFactory.directcallreturn()); pc++; @@ -1309,5 +1318,5 @@ add( insnFactory.runstart(mi)); pc++; } - + }
--- a/src/main/gov/nasa/jpf/jvm/JVMInstructionFactory.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/JVMInstructionFactory.java Tue Apr 21 00:34:15 2015 -0700 @@ -480,4 +480,6 @@ // this is never part of MethodInfo stored code abstract public Instruction runstart (MethodInfo miRun); + + abstract public Instruction finishclinit (ClassInfo ci); }
--- a/src/main/gov/nasa/jpf/jvm/JVMSystemClassLoaderInfo.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/JVMSystemClassLoaderInfo.java Tue Apr 21 00:34:15 2015 -0700 @@ -44,6 +44,8 @@ defaultCodeBuilder = createDefaultCodeBuilder(config, appId); + JVMClassInfo.init(config); + // now we can notify vm.registerClassLoader(this); }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/FINISHCLINIT.java Tue Apr 21 00:34:15 2015 -0700 @@ -0,0 +1,54 @@ +/* + * Copyright (C) 2015, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.jvm.bytecode; + +import gov.nasa.jpf.vm.ClassInfo; +import gov.nasa.jpf.vm.Instruction; +import gov.nasa.jpf.vm.ThreadInfo; + +/** + * artificial bytecode to defer class status changes of classes that don't have + * a <clinit>(), simulating native VM specific behavior that involves nested locking + * during class init + */ +public class FINISHCLINIT extends Instruction { + + protected ClassInfo ciInit; + + public FINISHCLINIT (ClassInfo ci){ + ciInit = ci; + } + + @Override + public Instruction execute (ThreadInfo ti) { + ciInit.setInitialized(); + return getNext(ti); + } + + @Override + public boolean isExtendedInstruction() { + return true; + } + + public static final int OPCODE = 262; + + @Override + public int getByteCode () { + return OPCODE; + } +}
--- a/src/main/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java Tue Apr 21 00:34:15 2015 -0700 @@ -64,6 +64,7 @@ // if we get here we still have to execute the clinit method setupCallee( ti, callee); // this creates, initializes & pushes the callee StackFrame, then acquires the lock + ciClsObj.setInitializing(ti); return ti.getPC(); // we can't just return the first callee insn if a listener throws an exception }
--- a/src/main/gov/nasa/jpf/jvm/bytecode/InstructionFactory.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/InstructionFactory.java Tue Apr 21 00:34:15 2015 -0700 @@ -1112,4 +1112,9 @@ return new RUNSTART(); } + @Override + public Instruction finishclinit(ClassInfo ci) { + return new FINISHCLINIT(ci); + } + }
--- a/src/main/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java Tue Apr 21 00:34:15 2015 -0700 @@ -69,7 +69,6 @@ frame.pop(); ei.lock(ti); // mark object as locked, increment the lockCount, and set the thread as owner - return getNext(ti); }
--- a/src/main/gov/nasa/jpf/jvm/bytecode/RETURN.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/jvm/bytecode/RETURN.java Tue Apr 21 00:34:15 2015 -0700 @@ -33,12 +33,7 @@ @Override public Instruction execute (ThreadInfo ti) { - // Constructors don't return anything so this is the only instruction that can be used to return from a constructor. - - //MethodInfo mi = ti.getMethod(); // Get the current method being executed (e.g. returned from). - if (mi.isInit()) { // Check to see if this method is a constructor. - int objref = ti.getThis(); ElementInfo ei = ti.getElementInfo(objref); // Get the object. @@ -52,6 +47,9 @@ ei.setConstructed(); } } + + } else if (mi.isClinit()) { + mi.getClassInfo().setInitialized(); } return super.execute(ti);
--- a/src/main/gov/nasa/jpf/report/ConsolePublisher.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/report/ConsolePublisher.java Tue Apr 21 00:34:15 2015 -0700 @@ -364,7 +364,7 @@ // this can be used outside a publisher, to show the same info public static void printStatistics (PrintWriter pw, Reporter reporter){ Statistics stat = reporter.getStatistics(); - + pw.println("elapsed time: " + formatHMS(reporter.getElapsedTime())); pw.println("states: new=" + stat.newStates + ",visited=" + stat.visitedStates + ",backtracked=" + stat.backtracked + ",end=" + stat.endStates);
--- a/src/main/gov/nasa/jpf/report/Reporter.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/report/Reporter.java Tue Apr 21 00:34:15 2015 -0700 @@ -62,7 +62,8 @@ this.jpf = jpf; search = jpf.getSearch(); vm = jpf.getVM(); - boolean reportStats = conf.getBoolean("report.statistics", false); + int probeInterval = conf.getInt("report.probe_interval"); + boolean reportStats = conf.getBoolean("report.statistics", false) || (probeInterval > 0); started = new Date(); @@ -82,7 +83,6 @@ getRegisteredStatistics(); } - int probeInterval = conf.getInt("report.probe_interval"); if (probeInterval > 0){ probeTimer = createProbeIntervalTimer(probeInterval); }
--- a/src/main/gov/nasa/jpf/util/json/JSONObject.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/util/json/JSONObject.java Tue Apr 21 00:34:15 2015 -0700 @@ -108,6 +108,12 @@ if (requiresClinitExecution(ciField, ti)){ return true; } + if (ciField.isArray()){ + ClassInfo ciComp = ciField.getComponentClassInfo(); + if (requiresClinitExecution(ciComp, ti)) { + return true; + } + } } ci = ci.getSuperClass();
--- a/src/main/gov/nasa/jpf/vm/ClassInfo.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/ClassInfo.java Tue Apr 21 00:34:15 2015 -0700 @@ -1454,6 +1454,14 @@ return null; } } + + public int getNumberOfSuperClasses(){ + int n = 0; + for (ClassInfo ci = superClass; ci != null; ci = ci.superClass){ + n++; + } + return n; + } /** * beware - this loads (but not yet registers) the enclosing class @@ -1961,13 +1969,13 @@ return false; } + /** + * see getInitializedClassInfo() for restrictions. + */ public static ClassInfo getInitializedSystemClassInfo (String clsName, ThreadInfo ti){ ClassLoaderInfo systemLoader = ClassLoaderInfo.getCurrentSystemClassLoader(); ClassInfo ci = systemLoader.getResolvedClassInfo(clsName); - - if (ci.initializeClass(ti)) { - throw new ClinitRequired(ci); - } + ci.initializeClassAtomic(ti); return ci; } @@ -1979,7 +1987,10 @@ */ public static ClassInfo getInitializedClassInfo (String clsName, ThreadInfo ti){ ClassLoaderInfo cl = ClassLoaderInfo.getCurrentClassLoader(); - return cl.getInitializedClassInfo(clsName, ti); + ClassInfo ci = cl.getResolvedClassInfo(clsName); + ci.initializeClassAtomic(ti); + + return ci; } public boolean isRegistered () { @@ -2131,9 +2142,16 @@ return (!isObjectClassInfo() && superClass != null); } - public boolean needsInitialization () { + public boolean needsInitialization (ThreadInfo ti){ StaticElementInfo sei = getStaticElementInfo(); - return ((sei == null) || (sei.getStatus() > INITIALIZED)); + if (sei != null){ + int status = sei.getStatus(); + if (status == INITIALIZED || status == ti.getId()){ + return false; + } + } + + return true; } public void setInitializing(ThreadInfo ti) { @@ -2193,14 +2211,44 @@ return (pushedFrames > 0); } - + + /** + * use this with care since it will throw a JPFException if we encounter a choice point + * during execution of clinits + * Use this mostly for wrapper exceptions and other system classes that are guaranteed to load + */ + public void initializeClassAtomic (ThreadInfo ti){ + for (ClassInfo ci = this; ci != null; ci = ci.getSuperClass()) { + StaticElementInfo sei = ci.getStaticElementInfo(); + if (sei == null){ + sei = ci.registerClass(ti); + } + + int status = sei.getStatus(); + if (status != INITIALIZED && status != ti.getId()){ + MethodInfo mi = ci.getMethod("<clinit>()V", false); + if (mi != null) { + DirectCallStackFrame frame = ci.createDirectCallStackFrame(ti, mi, 0); + ti.executeMethodAtomic(frame); + } else { + ci.setInitialized(); + } + } else { + break; // if this class is initialized, so are its superclasses + } + } + } + public void setInitialized() { - StaticElementInfo sei = getModifiableStaticElementInfo(); - sei.setStatus(INITIALIZED); + StaticElementInfo sei = getStaticElementInfo(); + if (sei != null && sei.getStatus() != INITIALIZED){ + sei = getModifiableStaticElementInfo(); + sei.setStatus(INITIALIZED); - // we don't emit classLoaded() notifications for non-builtin classes - // here anymore because it would be confusing to get instructionExecuted() - // notifications from the <clinit> execution before the classLoaded() + // we don't emit classLoaded() notifications for non-builtin classes + // here anymore because it would be confusing to get instructionExecuted() + // notifications from the <clinit> execution before the classLoaded() + } } public StaticElementInfo getStaticElementInfo() {
--- a/src/main/gov/nasa/jpf/vm/ClassLoaderInfo.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/ClassLoaderInfo.java Tue Apr 21 00:34:15 2015 -0700 @@ -480,11 +480,7 @@ */ public ClassInfo getInitializedClassInfo (String clsName, ThreadInfo ti){ ClassInfo ci = getResolvedClassInfo(clsName); - - if (ci.initializeClass(ti)) { - throw new ClinitRequired(ci); - } - + ci.initializeClassAtomic(ti); return ci; }
--- a/src/main/gov/nasa/jpf/vm/ElementInfo.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/ElementInfo.java Tue Apr 21 00:34:15 2015 -0700 @@ -1856,7 +1856,7 @@ private void notifies0 (ThreadInfo tiWaiter){ - if (tiWaiter.isWaiting()){ + if (tiWaiter.isWaitingOrTimedOut()){ if (tiWaiter.getLockCount() > 0) { // waiter did hold the lock, but gave it up in the wait, so it can't run yet tiWaiter.setNotifiedState(); @@ -1881,7 +1881,7 @@ int i, nWaiters=0, iWaiter=0; for (i=0; i<locked.length; i++) { - if (locked[i].isWaiting()) { + if (locked[i].isWaitingOrTimedOut() ) { nWaiters++; iWaiter = i; }
--- a/src/main/gov/nasa/jpf/vm/MJIEnv.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/MJIEnv.java Tue Apr 21 00:34:15 2015 -0700 @@ -17,10 +17,12 @@ */ package gov.nasa.jpf.vm; +import com.sun.org.apache.bcel.internal.generic.InstructionConstants; import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.JPFException; import gov.nasa.jpf.JPFListener; +import gov.nasa.jpf.vm.serialize.UnknownJPFClass; import java.util.Date; import java.util.Locale; @@ -698,7 +700,7 @@ public long getStaticLongField (int clsRef, String fname) { ClassInfo ci = getReferredClassInfo(clsRef); - return getStaticLongField(ci,fname); + return getStaticLongField(ci, fname); } public long getStaticLongField (String clsName, String fname) { @@ -1036,12 +1038,12 @@ return heap.newArray(elementClsName, size, ti).getObjectRef(); } - - public ElementInfo newElementInfo (ClassInfo ci){ + + public ElementInfo newElementInfo (ClassInfo ci) throws ClinitRequired { if (ci.initializeClass(ti)){ throw new ClinitRequired(ci); } - + return heap.newObject(ci, ti); } @@ -1050,7 +1052,7 @@ * if yes, create a new instance of it but don't call any ctor * if no, throw a ClinitRequired exception */ - public int newObject (ClassInfo ci) { + public int newObject (ClassInfo ci) throws ClinitRequired { ElementInfo ei = newElementInfo(ci); return ei.getObjectRef(); } @@ -1065,22 +1067,18 @@ return ei.getObjectRef(); } - public ElementInfo newElementInfo (String clsName) { + public ElementInfo newElementInfo (String clsName) throws ClinitRequired, UnknownJPFClass { ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(clsName); if (ci != null){ return newElementInfo(ci); } else { - return null; + throw new UnknownJPFClass(clsName); } } - public int newObject (String clsName) { + public int newObject (String clsName) throws ClinitRequired, UnknownJPFClass { ElementInfo ei = newElementInfo(clsName); - if (ei != null){ - return ei.getObjectRef(); - } else { - return NULL; - } + return (ei != null) ? ei.getObjectRef() : NULL; } public int newString (String s) {
--- a/src/main/gov/nasa/jpf/vm/ThreadInfo.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/main/gov/nasa/jpf/vm/ThreadInfo.java Tue Apr 21 00:34:15 2015 -0700 @@ -819,6 +819,11 @@ return (state == State.WAITING) || (state == State.TIMEOUT_WAITING); } + public boolean isWaitingOrTimedOut (){ + State state = threadData.state; + return (state == State.WAITING) || (state == State.TIMEOUT_WAITING) || (state == State.TIMEDOUT); + } + public boolean isNotified () { return (threadData.state == State.NOTIFIED); } @@ -1775,9 +1780,10 @@ * thrown by the VM (or a listener) */ public Instruction createAndThrowException (ClassInfo ci, String details) { - if (ci.initializeClass(this)) { - return getPC(); - } + //if (ci.initializeClass(this)) { + // return getPC(); + //} + ci.initializeClassAtomic(this); int objref = createException(ci,details, MJIEnv.NULL); return throwException(objref); @@ -1872,40 +1878,6 @@ } } - - protected void _executeTransition (SystemState ss) throws JPFException { - Instruction pc = getPC(); - Instruction nextPc = null; - - currentThread = this; - executedInstructions = 0; - pendingException = null; - - if (isStopped()){ - pc = throwStopException(); - setPC(pc); - } - - // this constitutes the main transition loop. It gobbles up - // insns until someone registered a ChoiceGenerator, there are no insns left, - // the transition was explicitly marked as ignored, or we have reached a - // max insn count and preempt the thread upon the next available backjump - while (pc != null) { - nextPc = executeInstruction(); - - if (ss.breakTransition()) { - if (executedInstructions == 0){ // a CG from a re-executed insn - if (isEmptyTransitionEnabled()){ // treat as a new state if empty transitions are enabled - ss.setForced(true); - } - } - break; - - } else { - pc = nextPc; - } - } - } protected void resetTransientAttributes(){ attributes &= ~(ATTR_SKIP_INSN_EXEC | ATTR_SKIP_INSN_LOG | ATTR_ENABLE_EMPTY_TRANSITION); @@ -2236,10 +2208,6 @@ ElementInfo ei = getModifiableElementInfo( oref); ei.lock(this); - - if (mi.isClinit()) { - mi.getClassInfo().setInitializing(this); - } } vm.notifyMethodEntered(this, mi); @@ -2268,14 +2236,6 @@ ei = ei.getModifiableInstance(); didUnblock = ei.unlock(this); } - - if (mi.isClinit()) { - // we just released the lock on the class object, returning from a clinit - // now we can consider this class to be initialized. - // NOTE this is still part of the RETURN insn of clinit, so ClassInfo.isInitialized - // is protected - mi.getClassInfo().setInitialized(); - } } vm.notifyMethodExited(this, mi); @@ -2875,6 +2835,7 @@ for (StackFrame frame = top; (frame != null) && (handlerFrame == null); frame = frame.getPrevious()) { // that means we have to turn the exception into an InvocationTargetException if (frame.isReflection()) { + // make sure it's in the startup class set since we are not able to re-execute here ciException = ClassInfo.getInitializedSystemClassInfo("java.lang.reflect.InvocationTargetException", this); exceptionObjRef = createException(ciException, exceptionName, exceptionObjRef); exceptionName = ciException.getName();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/main/gov/nasa/jpf/vm/serialize/UnknownJPFClass.java Tue Apr 21 00:34:15 2015 -0700 @@ -0,0 +1,42 @@ +/* + * Copyright (C) 2015, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package gov.nasa.jpf.vm.serialize; + +/** + * exception to indicate that JPF can't find a (model) class of a given name + * For native clients directly or indirectly cause class resolution + * + * <2do> we might turn this into an handled exception at some point + */ +public class UnknownJPFClass extends RuntimeException { + protected String clsName; + + public UnknownJPFClass(String clsName){ + this.clsName = clsName; + } + + String getRequestedClassName() { + return clsName; + } + + @Override + public String getMessage(){ + return clsName; + } +}
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_Exchanger.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_Exchanger.java Tue Apr 21 00:34:15 2015 -0700 @@ -48,7 +48,7 @@ } } - ElementInfo createExchangeObject (MJIEnv env, int waiterDataRef){ + ElementInfo createExchangeObject (MJIEnv env, int waiterDataRef) throws ClinitRequired { ElementInfo ei = env.newElementInfo("java.util.concurrent.Exchanger$Exchange"); ei.setReferenceField("waiterData", waiterDataRef); ei.setReferenceField("waiterThread", env.getThreadInfo().getThreadObjectRef()); @@ -75,26 +75,35 @@ StackFrame frame = ti.getModifiableTopFrame(); ExchangeState state = frame.getFrameAttr(ExchangeState.class); long to = (timeoutMillis <0) ? 0 : timeoutMillis; - + if (state == null){ // first time for waiter or responder int eRef = env.getReferenceField(objRef, "exchange"); if (eRef == MJIEnv.NULL){ // first waiter, this has to block unless there is a timeout value of 0 - ElementInfo ei = createExchangeObject(env, dataRef); - eRef = ei.getObjectRef(); + ElementInfo eiExchanger; + + try { + eiExchanger = createExchangeObject(env, dataRef); + } catch (ClinitRequired x){ + // need to come back after class init + env.repeatInvocation(); + return MJIEnv.NULL; + } + + eRef = eiExchanger.getObjectRef(); env.setReferenceField(objRef, "exchange", eRef); // timeout semantics differ - Object.wait(0) waits indefinitely, whereas here it // should throw immediately. We use -1 as non-timeout value - if (timeoutMillis == 0){ + if (timeoutMillis == 0) { env.throwException("java.util.concurrent.TimeoutException"); return MJIEnv.NULL; } - - ei.wait(ti, to, false); + + eiExchanger.wait(ti, to, false); // lockfree wait if (ti.getScheduler().setsWaitCG(ti, to)) { - return repeatInvocation(env, frame, ei, ExchangeState.createWaiterState(env, eRef)); + return repeatInvocation(env, frame, eiExchanger, ExchangeState.createWaiterState(env, eRef)); } else { throw new JPFException("blocked exchange() waiter without transition break"); } @@ -128,7 +137,7 @@ } } else { // re-execution(s) - ElementInfo ei = env.getElementInfo(state.exchangeRef); + ElementInfo eiExchanger = env.getElementInfo(state.exchangeRef); int retRef = MJIEnv.NULL; @@ -136,20 +145,24 @@ env.throwException("java.lang.InterruptedException"); } else if (ti.isTimedOut()){ - if (state.isWaiter){ - ei = ei.getModifiableInstance(); - ei.setBooleanField("waiterTimedOut", true); + if (state.isWaiter) { + eiExchanger = eiExchanger.getModifiableInstance(); + eiExchanger.setBooleanField("waiterTimedOut", true); + + // we are still lockfree waiting on the exChanger object + eiExchanger.notifies(env.getSystemState(), ti, false); } + env.throwException("java.util.concurrent.TimeoutException"); } else { - retRef = ei.getReferenceField( state.isWaiter ? "responderData" : "waiterData"); + retRef = eiExchanger.getReferenceField( state.isWaiter ? "responderData" : "waiterData"); } //-- processed frame.removeFrameAttr(state); - ei = ei.getModifiableInstance(); - env.releasePinDown(ei); + eiExchanger = eiExchanger.getModifiableInstance(); + env.releasePinDown(eiExchanger); return retRef; } }
--- a/src/tests/gov/nasa/jpf/test/mc/data/JSONTest.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/tests/gov/nasa/jpf/test/mc/data/JSONTest.java Tue Apr 21 00:34:15 2015 -0700 @@ -265,11 +265,11 @@ } } - class IC { + static class IC { int i; } - class ArrayOfObjects { + static class ArrayOfObjects { IC cls[]; }
--- a/src/tests/gov/nasa/jpf/test/mc/threads/ClinitTest.java Wed Apr 15 22:40:21 2015 -0700 +++ b/src/tests/gov/nasa/jpf/test/mc/threads/ClinitTest.java Tue Apr 21 00:34:15 2015 -0700 @@ -29,58 +29,59 @@ static class X { static int x; + static { Verify.threadPrintln("initializing X"); - assertTrue( x == 0); + assertTrue(x == 0); x++; } } - + @Test - public void testNoConcurrentClinit () { + public void testNoConcurrentClinit() { if (verifyNoPropertyViolation()) { - + Runnable r = new Runnable() { @Override - public void run() { + public void run() { int x = X.x; } }; Thread t = new Thread(r); t.start(); - + int x = X.x; - assertTrue( "x = " + x, x == 1); + assertTrue("x = " + x, x == 1); } } - - + + static class Y { static long y; - + static { Thread t = Thread.currentThread(); - Verify.threadPrintln("initializing Y"); + Verify.threadPrintln("initializing Y"); y = t.getId(); } } - + @Test public void testClinitChoices() { if (verifyAssertionErrorDetails("gotcha")) { Runnable r = new Runnable() { @Override - public void run() { + public void run() { long y = Y.y; } }; Thread t = new Thread(r); t.start(); - + long y = Y.y; Thread tCur = Thread.currentThread(); Verify.threadPrintln("testing Y.y"); - assertTrue( "gotcha", y == tCur.getId()); + assertTrue("gotcha", y == tCur.getId()); } } }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/tests/gov/nasa/jpf/test/mc/threads/NestedInitTest.java Tue Apr 21 00:34:15 2015 -0700 @@ -0,0 +1,138 @@ +/* + * Copyright (C) 2015, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.test.mc.threads; + +import gov.nasa.jpf.util.test.TestJPF; +import org.junit.Test; + +/** + * test deadlock detection during concurrent class init. + * + * This models hotspot behavior that can explode the state space + * and hence needs to be explicitly configured to perform + * nested locking during class init + */ +public class NestedInitTest extends TestJPF { + + //------------------------------------------------ check normal clinit execution + static class Root { + static int data; + + static { + System.out.print( Thread.currentThread().getName()); + System.out.println(" in Root.<clinit>()"); + data = 40; + } + } + + static class Base extends Root { + static int data; + + static { + System.out.print( Thread.currentThread().getName()); + System.out.println(" in Base.<clinit>()"); + data = Root.data + 1; + } + } + + static class Derived extends Base { + static int data; + + static { + System.out.print( Thread.currentThread().getName()); + System.out.println(" in Derived.<clinit>()"); + data = Base.data + 1; + } + } + + @Test + public void testNestedInitSingleOk() { + if (verifyNoPropertyViolation("+jvm.nested_init")){ + new Derived(); // force clinit + System.out.print("Derived.data = "); + System.out.println(Derived.data); + assertTrue(Derived.data == 42); + } + } + + @Test + public void testNestedInitConcurrentOk() { + if (verifyNoPropertyViolation("+jvm.nested_init")){ + new Thread( new Runnable(){ + public void run(){ + new Derived(); + System.out.print("t: Derived.data = "); + System.out.println(Derived.data); + assertTrue(Derived.data == 42); + } + }).start(); + + new Derived(); // force clinit + System.out.print("main: Derived.data = "); + System.out.println(Derived.data); + assertTrue(Derived.data == 42); + } + } + + //--- and now the nasty cases + + //------------------------------------------ symmetric case + + static class A { + static final B b = new B(); + } + + static class B { + static final A a = new A(); + } + + @Test + public void testSymmetricDeadlock() { + if (verifyDeadlock("+jvm.nested_init")) { + new Thread() { + public void run() { + new A(); + } + }.start(); + new B(); + } + } + + //------------------------------------------- hierarchical case + public static class CyclicBase { + static CyclicDerived sub = new CyclicDerived(); + } + + public static class CyclicDerived extends CyclicBase { + } + + + @Test + public void testCyclicHierarchyDeadlock (){ + if (verifyDeadlock("+jvm.nested_init")) { + new Thread() { + public void run() { + new CyclicDerived(); // causes class inits via CyclicDerived + } + }.start(); + + Object o = CyclicBase.sub; // causes class inits via CyclicBase + } + } + +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/tests/gov/nasa/jpf/test/vm/basic/ClassInitTest.java Tue Apr 21 00:34:15 2015 -0700 @@ -0,0 +1,59 @@ +/* + * Copyright (C) 2015, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.test.vm.basic; + +import gov.nasa.jpf.util.test.TestJPF; +import org.junit.Test; + +/** + * basic regression test for class initialization + */ +public class ClassInitTest extends TestJPF { + + static class Root { + static int data; + static { + System.out.println("in Root.<clinit>()"); + data = 42; + } + } + + static class Base extends Root { + static int data; + static { + System.out.println("in Base.<clinit>()"); + data = Root.data + 1; + } + } + + static class Derived extends Base { + static int data; + static { + System.out.println("in Derived.<clinit>()"); + data = Base.data + 1; + } + } + + @Test + public void testClinits (){ + if (verifyNoPropertyViolation()){ + int n = Derived.data; + assertTrue(n == 44); + } + } +}