src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.SystemAttribute;
  24 import gov.nasa.jpf.util.FieldSpecMatcher;
  25 import gov.nasa.jpf.util.JPFLogger;
  26 import gov.nasa.jpf.util.MethodSpecMatcher;
  27 import gov.nasa.jpf.util.TypeSpecMatcher;
  28 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
  29
  30 /**
  31  * an abstract SharednessPolicy implementation that makes use of both
  32  * shared field access CGs and exposure CGs.
  33  *
  34  * This class is highly configurable, both in terms of using exposure CGs and filters.
  35  * The *never_break filters should be used with care to avoid missing defects, especially
  36  * the (transitive) method filters.
  37  * NOTE - the default settings from jpf-core/jpf.properties include several
  38  * java.util.concurrent* and java.lang.* fields/methods that can in fact contribute to
  39  * concurrency defects, esp. in SUTs that explicitly use Thread/ThreadGroup objects, in
  40  * which case they should be removed.
  41  *
  42  * The *always_break field filter should only be used for white box SUT analysis if JPF
  43  * fails to detect sharedness (e.g. because no exposure is used). This should only
  44  * go into application property files
  45  */
  46 public abstract class GenericSharednessPolicy implements SharednessPolicy, Attributor {
  47
  48   //--- auxiliary types to configure filters
  49   static class NeverBreakIn implements SystemAttribute {
  50     static NeverBreakIn singleton = new NeverBreakIn();
  51   }
  52   static class NeverBreakOn implements SystemAttribute {
  53     static NeverBreakOn singleton = new NeverBreakOn();
  54   }
  55   static class AlwaysBreakOn implements SystemAttribute {
  56     static AlwaysBreakOn singleton = new AlwaysBreakOn();
  57   }
  58
  59   protected static JPFLogger logger = JPF.getLogger("shared");
  60
  61
  62   //--- options used for concurrent field access detection
  63
  64   protected TypeSpecMatcher neverBreakOnTypes;
  65
  66   protected TypeSpecMatcher alwaysBreakOnTypes;
  67
  68   /**
  69    * never break or expose if a matching method is on the stack
  70    */
  71   protected MethodSpecMatcher neverBreakInMethods;
  72
  73   /**
  74    * never break on matching fields
  75    */
  76   protected FieldSpecMatcher neverBreakOnFields;
  77
  78   /**
  79    * always break matching fields, no matter if object is already shared or not
  80    */
  81   protected FieldSpecMatcher alwaysBreakOnFields;
  82
  83
  84   /**
  85    * do we break on final field access
  86    */
  87   protected boolean skipFinals;
  88   protected boolean skipConstructedFinals;
  89   protected boolean skipStaticFinals;
  90
  91   /**
  92    * do we break inside of constructors
  93    * (note that 'this' references could leak from ctors, but
  94    * this is rather unusual)
  95    */
  96   protected boolean skipInits;
  97
  98   /**
  99    * do we add CGs for objects that could become shared, e.g. when storing
 100    * a reference to a non-shared object in a shared object field.
 101    * NOTE: this is a conservative measure since we don't know yet at the
 102    * point of exposure if the object will ever be shared, which means it
 103    * can cause state explosion.
 104    */
 105   protected boolean breakOnExposure;
 106
 107   /**
 108    * options to filter out lock protected field access, which is not
 109    * supposed to cause shared CGs
 110    * (this has no effect on exposure though)
 111    */
 112   protected boolean useSyncDetection;
 113   protected int lockThreshold;
 114
 115   protected VM vm;
 116
 117
 118   protected GenericSharednessPolicy (Config config){
 119     neverBreakInMethods = MethodSpecMatcher.create( config.getStringArray("vm.shared.never_break_methods"));
 120
 121     neverBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.never_break_types"));
 122     alwaysBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.always_break_types"));
 123
 124     neverBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.never_break_fields"));
 125     alwaysBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.always_break_fields"));
 126
 127     skipFinals = config.getBoolean("vm.shared.skip_finals", true);
 128     skipConstructedFinals = config.getBoolean("vm.shared.skip_constructed_finals", false);
 129     skipStaticFinals = config.getBoolean("vm.shared.skip_static_finals", true);
 130     skipInits = config.getBoolean("vm.shared.skip_inits", true);
 131
 132     breakOnExposure = config.getBoolean("vm.shared.break_on_exposure", true);
 133
 134     useSyncDetection = config.getBoolean("vm.shared.sync_detection", true);
 135     lockThreshold = config.getInt("vm.shared.lockthreshold", 5);
 136   }
 137
 138   //--- internal methods (potentially overridden by subclass)
 139
 140
 141   //--- attribute management
 142
 143   protected void setTypeAttributes (TypeSpecMatcher neverMatcher, TypeSpecMatcher alwaysMatcher, ClassInfo ciLoaded){
 144     // we flatten this for performance reasons
 145     for (ClassInfo ci = ciLoaded; ci!= null; ci = ci.getSuperClass()){
 146       if (alwaysMatcher != null && alwaysMatcher.matches(ci)){
 147         ciLoaded.addAttr(AlwaysBreakOn.singleton);
 148         return;
 149       }
 150       if (neverMatcher != null && neverMatcher.matches(ci)){
 151         ciLoaded.addAttr( NeverBreakOn.singleton);
 152         return;
 153       }
 154     }
 155   }
 156
 157   protected void setFieldAttributes (FieldSpecMatcher neverMatcher, FieldSpecMatcher alwaysMatcher, ClassInfo ci){
 158     for (FieldInfo fi : ci.getDeclaredInstanceFields()) {
 159       // invisible fields (created by compiler)
 160       if (fi.getName().startsWith("this$")) {
 161         fi.addAttr( NeverBreakOn.singleton);
 162         continue;
 163       }
 164
 165       // configuration
 166       if (neverMatcher != null && neverMatcher.matches(fi)) {
 167         fi.addAttr( NeverBreakOn.singleton);
 168       }
 169       if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
 170         fi.addAttr( AlwaysBreakOn.singleton);
 171       }
 172
 173       // annotation
 174       if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
 175         fi.addAttr( NeverBreakOn.singleton);
 176       }
 177     }
 178
 179     for (FieldInfo fi : ci.getDeclaredStaticFields()) {
 180       // invisible fields (created by compiler)
 181       if ("$assertionsDisabled".equals(fi.getName())) {
 182         fi.addAttr( NeverBreakOn.singleton);
 183         continue;
 184       }
 185
 186       // configuration
 187       if (neverMatcher != null && neverMatcher.matches(fi)) {
 188         fi.addAttr( NeverBreakOn.singleton);
 189       }
 190       if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
 191         fi.addAttr( AlwaysBreakOn.singleton);
 192       }
 193
 194       // annotation
 195       if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
 196         fi.addAttr( NeverBreakOn.singleton);
 197       }
 198     }
 199   }
 200
 201   protected boolean isInNeverBreakMethod (ThreadInfo ti){
 202     for (StackFrame frame = ti.getTopFrame(); frame != null; frame=frame.getPrevious()){
 203       MethodInfo mi = frame.getMethodInfo();
 204       if (mi.hasAttr( NeverBreakIn.class)){
 205         return true;
 206       }
 207     }
 208
 209     return false;
 210   }
 211
 212   protected abstract boolean checkOtherRunnables (ThreadInfo ti);
 213
 214   // this needs a three-way return value, hence Boolean
 215   protected Boolean canHaveSharednessCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
 216     //--- thread
 217     if (ti.isFirstStepInsn()){ // no empty transitions
 218       return Boolean.FALSE;
 219     }
 220
 221     if (!checkOtherRunnables(ti)){ // nothing to reschedule
 222       return Boolean.FALSE;
 223     }
 224
 225     if (ti.hasAttr( NeverBreakIn.class)){
 226       return Boolean.FALSE;
 227     }
 228
 229     //--- method
 230     if (isInNeverBreakMethod(ti)){
 231       return false;
 232     }
 233
 234     //--- type
 235     ClassInfo ciFieldOwner = eiFieldOwner.getClassInfo();
 236     if (ciFieldOwner.hasAttr(NeverBreakOn.class)){
 237       return Boolean.FALSE;
 238     }
 239     if (ciFieldOwner.hasAttr(AlwaysBreakOn.class)){
 240       return Boolean.TRUE;
 241     }
 242
 243     //--- field
 244     if (fi != null){
 245       if (fi.hasAttr(AlwaysBreakOn.class)) {
 246         return Boolean.TRUE;
 247       }
 248       if (fi.hasAttr(NeverBreakOn.class)) {
 249         return Boolean.FALSE;
 250       }
 251     }
 252
 253     return null;
 254   }
 255
 256   //--- FieldLockInfo management
 257
 258   /**
 259    * static attribute filters that determine if the check..Access() and check..Exposure() methods should be called.
 260    * This is only called once per instruction execution since it filters all cases that would set a CG.
 261    * Filter conditions have to apply to both field access and object exposure.
 262    */
 263   protected abstract FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
 264
 265
 266   /**
 267    * generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine
 268    * if ElementInfo needs to be cloned
 269    */
 270   protected ElementInfo updateFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
 271     FieldLockInfo fli = ei.getFieldLockInfo(fi);
 272     if (fli == null){
 273       fli = createFieldLockInfo(ti, ei, fi);
 274       ei = ei.getModifiableInstance();
 275       ei.setFieldLockInfo(fi, fli);
 276
 277     } else {
 278       FieldLockInfo newFli = fli.checkProtection(ti, ei, fi);
 279       if (newFli != fli) {
 280         ei = ei.getModifiableInstance();
 281         ei.setFieldLockInfo(fi,newFli);
 282       }
 283     }
 284
 285     return ei;
 286   }
 287
 288
 289   //--- runnable computation & CG creation
 290
 291   // NOTE - we don't schedule threads outside this process since field access if process local
 292
 293   protected ThreadInfo[] getRunnables (ApplicationContext appCtx){
 294     return vm.getThreadList().getProcessTimeoutRunnables(appCtx);
 295   }
 296
 297   protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
 298     if (vm.getSystemState().isAtomic()){ // no CG if we are in a atomic section
 299       return null;
 300     }
 301
 302     ThreadInfo[] choices = getRunnables(tiCurrent.getApplicationContext());
 303     if (choices.length <= 1){ // field access doesn't block, i.e. the current thread is always runnable
 304       return null;
 305     }
 306
 307     return new ThreadChoiceFromSet( id, choices, true);
 308   }
 309
 310   protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
 311     if (cg != null){
 312       return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
 313     }
 314
 315     return false;
 316   }
 317
 318
 319   //--- internal policy methods that can be overridden by subclasses
 320
 321   protected ElementInfo updateSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
 322     ThreadInfoSet tis = ei.getReferencingThreads();
 323     ThreadInfoSet newTis = tis.add(ti);
 324
 325     if (tis != newTis){
 326       ei = ei.getModifiableInstance();
 327       ei.setReferencingThreads(newTis);
 328     }
 329
 330     // we only change from non-shared to shared
 331     if (newTis.isShared(ti, ei) && !ei.isShared() && !ei.isSharednessFrozen()) {
 332       ei = ei.getModifiableInstance();
 333       ei.setShared(ti, true);
 334     }
 335
 336     if (ei.isShared() && fi != null){
 337       ei = updateFieldLockInfo(ti,ei,fi);
 338     }
 339
 340     return ei;
 341   }
 342
 343   protected boolean setsExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
 344     if (breakOnExposure){
 345       ClassInfo ciExposed = eiExposed.getClassInfo();
 346
 347       //--- exposed type
 348       if (ciExposed.hasAttr(NeverBreakOn.class)){
 349         return false;
 350       }
 351       if (ciExposed.hasAttr(AlwaysBreakOn.class)){
 352         logger.info("type exposure CG setting field ", fi, " to ", eiExposed);
 353         return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
 354       }
 355
 356       // we can't filter on immutability since the race subject could be a reference
 357       // that is exposed through the exposed object
 358
 359       if (isInNeverBreakMethod(ti)){
 360         return false;
 361       }
 362
 363       if (eiFieldOwner.isExposedOrShared() && isFirstExposure(eiFieldOwner, eiExposed)){
 364         // don't check against the 'old' field value because this might get called after the field was already updated
 365         // we should solely depend on different object sharedness
 366         eiExposed = eiExposed.getExposedInstance(ti, eiFieldOwner);
 367         logger.info("exposure CG setting field ", fi, " to ", eiExposed);
 368         return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
 369       }
 370     }
 371
 372     return false;
 373   }
 374
 375   protected boolean isFirstExposure (ElementInfo eiFieldOwner, ElementInfo eiExposed){
 376     if (!eiExposed.isImmutable()){
 377       if (!eiExposed.isExposedOrShared()) {
 378          return (eiFieldOwner.isExposedOrShared());
 379       }
 380     }
 381
 382     return false;
 383   }
 384
 385
 386   //------------------------------------------------ Attributor interface
 387
 388   /**
 389    * this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution
 390    */
 391   @Override
 392   public void initializeSharednessPolicy (VM vm, ApplicationContext appCtx){
 393     this.vm = vm;
 394
 395     SystemClassLoaderInfo sysCl = appCtx.getSystemClassLoader();
 396     sysCl.addAttributor(this);
 397   }
 398
 399
 400   @Override
 401   public void setAttributes (ClassInfo ci){
 402     setTypeAttributes( neverBreakOnTypes, alwaysBreakOnTypes, ci);
 403
 404     setFieldAttributes( neverBreakOnFields, alwaysBreakOnFields, ci);
 405
 406     // this one is more expensive to iterate over and should be avoided
 407     if (neverBreakInMethods != null){
 408       for (MethodInfo mi : ci.getDeclaredMethods().values()){
 409         if (neverBreakInMethods.matches(mi)){
 410           mi.setAttr( NeverBreakIn.singleton);
 411         }
 412       }
 413     }
 414
 415   }
 416
 417   //------------------------------------------------ SharednessPolicy interface
 418
 419   @Override
 420   public ElementInfo updateObjectSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
 421     return updateSharedness(ti, ei, fi);
 422   }
 423   @Override
 424   public ElementInfo updateClassSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
 425     return updateSharedness(ti, ei, fi);
 426   }
 427   @Override
 428   public ElementInfo updateArraySharedness (ThreadInfo ti, ElementInfo ei, int idx){
 429     // NOTE - we don't support per-element FieldLockInfos (yet)
 430     return updateSharedness(ti, ei, null);
 431   }
 432
 433
 434   /**
 435    * check to determine if call site, object/class attributes and thread execution state
 436    * could cause CGs. This is called before sharedness is updated, i.e. can be used to
 437    * filter objects/classes that should not be sharedness tracked
 438    */
 439   @Override
 440   public boolean canHaveSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
 441     Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
 442     if (ret != null){
 443       return ret;
 444     }
 445
 446     if  (eiFieldOwner.isImmutable()){
 447       return false;
 448     }
 449
 450     if (skipFinals && fi.isFinal()){
 451       return false;
 452     }
 453
 454     //--- mixed (dynamic) attributes
 455     if (skipConstructedFinals && fi.isFinal() && eiFieldOwner.isConstructed()){
 456       return false;
 457     }
 458
 459     if (skipInits && insn.getMethodInfo().isInit()){
 460       return false;
 461     }
 462
 463     return true;
 464   }
 465
 466   @Override
 467   public boolean canHaveSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
 468     Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
 469     if (ret != null){
 470       return ret;
 471     }
 472
 473     if  (eiFieldOwner.isImmutable()){
 474       return false;
 475     }
 476
 477     if (skipStaticFinals && fi.isFinal()){
 478       return false;
 479     }
 480
 481     // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
 482     MethodInfo mi = insn.getMethodInfo();
 483     if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
 484       // clinits are all synchronized, so they are lock protected per se
 485       return false;
 486     }
 487
 488     return true;
 489   }
 490
 491   @Override
 492   public boolean canHaveSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx){
 493     Boolean ret = canHaveSharednessCG( ti, insn, eiArray, null);
 494     if (ret != null){
 495       return ret;
 496     }
 497
 498     // more array specific checks here
 499
 500     return true;
 501   }
 502
 503
 504   /**
 505    * <2do> explain why not transitive
 506    *
 507    * these are the public interfaces towards FieldInstructions. Callers have to be aware this will
 508    * change the /referenced/ ElementInfo in case the respective object becomes exposed
 509    */
 510   @Override
 511   public boolean setsSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
 512     if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
 513             (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
 514       logger.info("CG accessing shared instance field ", fi);
 515       return setNextChoiceGenerator( getRunnableCG("SHARED_OBJECT", ti));
 516     }
 517
 518     return false;
 519   }
 520
 521   @Override
 522   public boolean setsSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
 523     if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
 524             (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
 525       logger.info("CG accessing shared static field ", fi);
 526       return setNextChoiceGenerator( getRunnableCG("SHARED_CLASS", ti));
 527     }
 528
 529     return false;
 530   }
 531
 532   @Override
 533   public boolean setsSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int index){
 534     if (eiArray.isShared()){
 535       // <2do> we should check lock protection for the whole array here
 536       logger.info("CG accessing shared array ", eiArray);
 537       return setNextChoiceGenerator( getRunnableCG("SHARED_ARRAY", ti));
 538     }
 539
 540     return false;
 541   }
 542
 543
 544   //--- internal policy methods that can be overridden by subclasses
 545
 546   protected boolean isRelevantStaticFieldAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, FieldInfo fi){
 547     if (!ei.isShared()){
 548       return false;
 549     }
 550
 551     if  (ei.isImmutable()){
 552       return false;
 553     }
 554
 555     if (skipStaticFinals && fi.isFinal()){
 556       return false;
 557     }
 558
 559     if (!ti.hasOtherRunnables()){ // nothing to break for
 560       return false;
 561     }
 562
 563     // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
 564     MethodInfo mi = insn.getMethodInfo();
 565     if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
 566       // clinits are all synchronized, so they are lock protected per se
 567       return false;
 568     }
 569
 570     return true;
 571   }
 572
 573
 574   protected boolean isRelevantArrayAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, int index){
 575     // <2do> this is too simplistic, we should support filters for array objects
 576
 577     if (!ti.hasOtherRunnables()){
 578       return false;
 579     }
 580
 581     if (!ei.isShared()){
 582       return false;
 583     }
 584
 585     if (ti.isFirstStepInsn()){ // we already did break
 586       return false;
 587     }
 588
 589     return true;
 590   }
 591
 592   //--- object exposure
 593
 594   // <2do> explain why not transitive
 595
 596   @Override
 597   public boolean setsSharedObjectExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
 598     return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
 599   }
 600
 601   @Override
 602   public boolean setsSharedClassExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
 603     return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
 604   }
 605
 606   // since exposure is about the object being exposed (the element), there is no separate setsSharedArrayExposureCG
 607
 608
 609   @Override
 610   public void cleanupThreadTermination(ThreadInfo ti) {
 611     // default action is to do nothing
 612   }
 613
 614 }