Members/kono/jpf-core: src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java comparison

comparison src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java @ 0:61d41facf527

initial v8 import (history reset)

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children

comparison

equal deleted inserted replaced

--1:000000000000
+:61d41facf527
+/*
+* Copyright (C) 2014, 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;
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.SystemAttribute;
+import gov.nasa.jpf.util.FieldSpecMatcher;
+import gov.nasa.jpf.util.JPFLogger;
+import gov.nasa.jpf.util.MethodSpecMatcher;
+import gov.nasa.jpf.util.TypeSpecMatcher;
+import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
+/**
+* an abstract SharednessPolicy implementation that makes use of both
+* shared field access CGs and exposure CGs.
+*
+* This class is highly configurable, both in terms of using exposure CGs and filters.
+* The *never_break filters should be used with care to avoid missing defects, especially
+* the (transitive) method filters.
+* NOTE - the default settings from jpf-core/jpf.properties include several
+* java.util.concurrent* and java.lang.* fields/methods that can in fact contribute to
+* concurrency defects, esp. in SUTs that explicitly use Thread/ThreadGroup objects, in
+* which case they should be removed.
+*
+* The *always_break field filter should only be used for white box SUT analysis if JPF
+* fails to detect sharedness (e.g. because no exposure is used). This should only
+* go into application property files
+*/
+public abstract class GenericSharednessPolicy implements SharednessPolicy, Attributor {
+//--- auxiliary types to configure filters
+static class NeverBreakIn implements SystemAttribute {
+static NeverBreakIn singleton = new NeverBreakIn();
+}
+static class NeverBreakOn implements SystemAttribute {
+static NeverBreakOn singleton = new NeverBreakOn();
+}
+static class AlwaysBreakOn implements SystemAttribute {
+static AlwaysBreakOn singleton = new AlwaysBreakOn();
+}
+protected static JPFLogger logger = JPF.getLogger("shared");
+//--- options used for concurrent field access detection
+protected TypeSpecMatcher neverBreakOnTypes;
+protected TypeSpecMatcher alwaysBreakOnTypes;
+/**
+* never break or expose if a matching method is on the stack
+*/
+protected MethodSpecMatcher neverBreakInMethods;
+/**
+* never break on matching fields
+*/
+protected FieldSpecMatcher neverBreakOnFields;
+/**
+* always break matching fields, no matter if object is already shared or not
+*/
+protected FieldSpecMatcher alwaysBreakOnFields;
+/**
+* do we break on final field access
+*/
+protected boolean skipFinals;
+protected boolean skipConstructedFinals;
+protected boolean skipStaticFinals;
+/**
+* do we break inside of constructors
+* (note that 'this' references could leak from ctors, but
+* this is rather unusual)
+*/
+protected boolean skipInits;
+/**
+* do we add CGs for objects that could become shared, e.g. when storing
+* a reference to a non-shared object in a shared object field.
+* NOTE: this is a conservative measure since we don't know yet at the
+* point of exposure if the object will ever be shared, which means it
+* can cause state explosion.
+*/
+protected boolean breakOnExposure;
+/**
+* options to filter out lock protected field access, which is not
+* supposed to cause shared CGs
+* (this has no effect on exposure though)
+*/
+protected boolean useSyncDetection;
+protected int lockThreshold;
+protected VM vm;
+protected GenericSharednessPolicy (Config config){
+neverBreakInMethods = MethodSpecMatcher.create( config.getStringArray("vm.shared.never_break_methods"));
+neverBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.never_break_types"));
+alwaysBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.always_break_types"));
+neverBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.never_break_fields"));
+alwaysBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.always_break_fields"));
+skipFinals = config.getBoolean("vm.shared.skip_finals", true);
+skipConstructedFinals = config.getBoolean("vm.shared.skip_constructed_finals", false);
+skipStaticFinals = config.getBoolean("vm.shared.skip_static_finals", true);
+skipInits = config.getBoolean("vm.shared.skip_inits", true);
+breakOnExposure = config.getBoolean("vm.shared.break_on_exposure", true);
+useSyncDetection = config.getBoolean("vm.shared.sync_detection", true);
+lockThreshold = config.getInt("vm.shared.lockthreshold", 5);
+}
+//--- internal methods (potentially overridden by subclass)
+//--- attribute management
+protected void setTypeAttributes (TypeSpecMatcher neverMatcher, TypeSpecMatcher alwaysMatcher, ClassInfo ciLoaded){
+// we flatten this for performance reasons
+for (ClassInfo ci = ciLoaded; ci!= null; ci = ci.getSuperClass()){
+if (alwaysMatcher != null && alwaysMatcher.matches(ci)){
+ciLoaded.addAttr(AlwaysBreakOn.singleton);
+return;
+}
+if (neverMatcher != null && neverMatcher.matches(ci)){
+ciLoaded.addAttr( NeverBreakOn.singleton);
+return;
+}
+}
+}
+protected void setFieldAttributes (FieldSpecMatcher neverMatcher, FieldSpecMatcher alwaysMatcher, ClassInfo ci){
+for (FieldInfo fi : ci.getDeclaredInstanceFields()) {
+// invisible fields (created by compiler)
+if (fi.getName().startsWith("this$")) {
+fi.addAttr( NeverBreakOn.singleton);
+continue;
+}
+// configuration
+if (neverMatcher != null && neverMatcher.matches(fi)) {
+fi.addAttr( NeverBreakOn.singleton);
+}
+if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
+fi.addAttr( AlwaysBreakOn.singleton);
+}
+// annotation
+if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
+fi.addAttr( NeverBreakOn.singleton);
+}
+}
+for (FieldInfo fi : ci.getDeclaredStaticFields()) {
+// invisible fields (created by compiler)
+if ("$assertionsDisabled".equals(fi.getName())) {
+fi.addAttr( NeverBreakOn.singleton);
+continue;
+}
+// configuration
+if (neverMatcher != null && neverMatcher.matches(fi)) {
+fi.addAttr( NeverBreakOn.singleton);
+}
+if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
+fi.addAttr( AlwaysBreakOn.singleton);
+}
+// annotation
+if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
+fi.addAttr( NeverBreakOn.singleton);
+}
+}
+}
+protected boolean isInNeverBreakMethod (ThreadInfo ti){
+for (StackFrame frame = ti.getTopFrame(); frame != null; frame=frame.getPrevious()){
+MethodInfo mi = frame.getMethodInfo();
+if (mi.hasAttr( NeverBreakIn.class)){
+return true;
+}
+}
+return false;
+}
+protected abstract boolean checkOtherRunnables (ThreadInfo ti);
+// this needs a three-way return value, hence Boolean
+protected Boolean canHaveSharednessCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+//--- thread
+if (ti.isFirstStepInsn()){ // no empty transitions
+return Boolean.FALSE;
+}
+if (!checkOtherRunnables(ti)){ // nothing to reschedule
+return Boolean.FALSE;
+}
+if (ti.hasAttr( NeverBreakIn.class)){
+return Boolean.FALSE;
+}
+//--- method
+if (isInNeverBreakMethod(ti)){
+return false;
+}
+//--- type
+ClassInfo ciFieldOwner = eiFieldOwner.getClassInfo();
+if (ciFieldOwner.hasAttr(NeverBreakOn.class)){
+return Boolean.FALSE;
+}
+if (ciFieldOwner.hasAttr(AlwaysBreakOn.class)){
+return Boolean.TRUE;
+}
+//--- field
+if (fi != null){
+if (fi.hasAttr(AlwaysBreakOn.class)) {
+return Boolean.TRUE;
+}
+if (fi.hasAttr(NeverBreakOn.class)) {
+return Boolean.FALSE;
+}
+}
+return null;
+}
+//--- FieldLockInfo management
+/**
+* static attribute filters that determine if the check..Access() and check..Exposure() methods should be called.
+* This is only called once per instruction execution since it filters all cases that would set a CG.
+* Filter conditions have to apply to both field access and object exposure.
+*/
+protected abstract FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
+/**
+* generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine
+* if ElementInfo needs to be cloned
+*/
+protected ElementInfo updateFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+FieldLockInfo fli = ei.getFieldLockInfo(fi);
+if (fli == null){
+fli = createFieldLockInfo(ti, ei, fi);
+ei = ei.getModifiableInstance();
+ei.setFieldLockInfo(fi, fli);
+} else {
+FieldLockInfo newFli = fli.checkProtection(ti, ei, fi);
+if (newFli != fli) {
+ei = ei.getModifiableInstance();
+ei.setFieldLockInfo(fi,newFli);
+}
+}
+return ei;
+}
+//--- runnable computation & CG creation
+// NOTE - we don't schedule threads outside this process since field access if process local
+protected ThreadInfo[] getRunnables (ApplicationContext appCtx){
+return vm.getThreadList().getProcessTimeoutRunnables(appCtx);
+}
+protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
+if (vm.getSystemState().isAtomic()){ // no CG if we are in a atomic section
+return null;
+}
+ThreadInfo[] choices = getRunnables(tiCurrent.getApplicationContext());
+if (choices.length <= 1){ // field access doesn't block, i.e. the current thread is always runnable
+return null;
+}
+return new ThreadChoiceFromSet( id, choices, true);
+}
+protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
+if (cg != null){
+return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
+}
+return false;
+}
+//--- internal policy methods that can be overridden by subclasses
+protected ElementInfo updateSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+ThreadInfoSet tis = ei.getReferencingThreads();
+ThreadInfoSet newTis = tis.add(ti);
+if (tis != newTis){
+ei = ei.getModifiableInstance();
+ei.setReferencingThreads(newTis);
+}
+// we only change from non-shared to shared
+if (newTis.isShared(ti, ei) && !ei.isShared() && !ei.isSharednessFrozen()) {
+ei = ei.getModifiableInstance();
+ei.setShared(ti, true);
+}
+if (ei.isShared() && fi != null){
+ei = updateFieldLockInfo(ti,ei,fi);
+}
+return ei;
+}
+protected boolean setsExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
+if (breakOnExposure){
+ClassInfo ciExposed = eiExposed.getClassInfo();
+//--- exposed type
+if (ciExposed.hasAttr(NeverBreakOn.class)){
+return false;
+}
+if (ciExposed.hasAttr(AlwaysBreakOn.class)){
+logger.info("type exposure CG setting field ", fi, " to ", eiExposed);
+return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
+}
+// we can't filter on immutability since the race subject could be a reference
+// that is exposed through the exposed object
+if (isInNeverBreakMethod(ti)){
+return false;
+}
+if (eiFieldOwner.isExposedOrShared() && isFirstExposure(eiFieldOwner, eiExposed)){
+// don't check against the 'old' field value because this might get called after the field was already updated
+// we should solely depend on different object sharedness
+eiExposed = eiExposed.getExposedInstance(ti, eiFieldOwner);
+logger.info("exposure CG setting field ", fi, " to ", eiExposed);
+return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
+}
+}
+return false;
+}
+protected boolean isFirstExposure (ElementInfo eiFieldOwner, ElementInfo eiExposed){
+if (!eiExposed.isImmutable()){
+if (!eiExposed.isExposedOrShared()) {
+return (eiFieldOwner.isExposedOrShared());
+}
+}
+return false;
+}
+//------------------------------------------------ Attributor interface
+/**
+* this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution
+*/
+@Override
+public void initializeSharednessPolicy (VM vm, ApplicationContext appCtx){
+this.vm = vm;
+SystemClassLoaderInfo sysCl = appCtx.getSystemClassLoader();
+sysCl.addAttributor(this);
+}
+@Override
+public void setAttributes (ClassInfo ci){
+setTypeAttributes( neverBreakOnTypes, alwaysBreakOnTypes, ci);
+setFieldAttributes( neverBreakOnFields, alwaysBreakOnFields, ci);
+// this one is more expensive to iterate over and should be avoided
+if (neverBreakInMethods != null){
+for (MethodInfo mi : ci.getDeclaredMethods().values()){
+if (neverBreakInMethods.matches(mi)){
+mi.setAttr( NeverBreakIn.singleton);
+}
+}
+}
+}
+//------------------------------------------------ SharednessPolicy interface
+@Override
+public ElementInfo updateObjectSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+return updateSharedness(ti, ei, fi);
+}
+@Override
+public ElementInfo updateClassSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+return updateSharedness(ti, ei, fi);
+}
+@Override
+public ElementInfo updateArraySharedness (ThreadInfo ti, ElementInfo ei, int idx){
+// NOTE - we don't support per-element FieldLockInfos (yet)
+return updateSharedness(ti, ei, null);
+}
+/**
+* check to determine if call site, object/class attributes and thread execution state
+* could cause CGs. This is called before sharedness is updated, i.e. can be used to
+* filter objects/classes that should not be sharedness tracked
+*/
+@Override
+public boolean canHaveSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
+if (ret != null){
+return ret;
+}
+if  (eiFieldOwner.isImmutable()){
+return false;
+}
+if (skipFinals && fi.isFinal()){
+return false;
+}
+//--- mixed (dynamic) attributes
+if (skipConstructedFinals && fi.isFinal() && eiFieldOwner.isConstructed()){
+return false;
+}
+if (skipInits && insn.getMethodInfo().isInit()){
+return false;
+}
+return true;
+}
+@Override
+public boolean canHaveSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
+if (ret != null){
+return ret;
+}
+if  (eiFieldOwner.isImmutable()){
+return false;
+}
+if (skipStaticFinals && fi.isFinal()){
+return false;
+}
+// call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
+MethodInfo mi = insn.getMethodInfo();
+if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
+// clinits are all synchronized, so they are lock protected per se
+return false;
+}
+return true;
+}
+@Override
+public boolean canHaveSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx){
+Boolean ret = canHaveSharednessCG( ti, insn, eiArray, null);
+if (ret != null){
+return ret;
+}
+// more array specific checks here
+return true;
+}
+/**
+* <2do> explain why not transitive
+*
+* these are the public interfaces towards FieldInstructions. Callers have to be aware this will
+* change the /referenced/ ElementInfo in case the respective object becomes exposed
+*/
+@Override
+public boolean setsSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
+(eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
+logger.info("CG accessing shared instance field ", fi);
+return setNextChoiceGenerator( getRunnableCG("SHARED_OBJECT", ti));
+}
+return false;
+}
+@Override
+public boolean setsSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
+(eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
+logger.info("CG accessing shared static field ", fi);
+return setNextChoiceGenerator( getRunnableCG("SHARED_CLASS", ti));
+}
+return false;
+}
+@Override
+public boolean setsSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int index){
+if (eiArray.isShared()){
+// <2do> we should check lock protection for the whole array here
+logger.info("CG accessing shared array ", eiArray);
+return setNextChoiceGenerator( getRunnableCG("SHARED_ARRAY", ti));
+}
+return false;
+}
+//--- internal policy methods that can be overridden by subclasses
+protected boolean isRelevantStaticFieldAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, FieldInfo fi){
+if (!ei.isShared()){
+return false;
+}
+if  (ei.isImmutable()){
+return false;
+}
+if (skipStaticFinals && fi.isFinal()){
+return false;
+}
+if (!ti.hasOtherRunnables()){ // nothing to break for
+return false;
+}
+// call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
+MethodInfo mi = insn.getMethodInfo();
+if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
+// clinits are all synchronized, so they are lock protected per se
+return false;
+}
+return true;
+}
+protected boolean isRelevantArrayAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, int index){
+// <2do> this is too simplistic, we should support filters for array objects
+if (!ti.hasOtherRunnables()){
+return false;
+}
+if (!ei.isShared()){
+return false;
+}
+if (ti.isFirstStepInsn()){ // we already did break
+return false;
+}
+return true;
+}
+//--- object exposure
+// <2do> explain why not transitive
+@Override
+public boolean setsSharedObjectExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
+return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
+}
+@Override
+public boolean setsSharedClassExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
+return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
+}
+// since exposure is about the object being exposed (the element), there is no separate setsSharedArrayExposureCG
+@Override
+public void cleanupThreadTermination(ThreadInfo ti) {
+// default action is to do nothing
+}
+}

Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java @ 0:61d41facf527