src/main/gov/nasa/jpf/listener/DeadlockAnalyzer.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 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.ListenerAdapter;
  23 import gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE;
  24 import gov.nasa.jpf.report.ConsolePublisher;
  25 import gov.nasa.jpf.report.Publisher;
  26 import gov.nasa.jpf.search.Search;
  27 import gov.nasa.jpf.vm.ElementInfo;
  28 import gov.nasa.jpf.vm.Instruction;
  29 import gov.nasa.jpf.vm.VM;
  30 import gov.nasa.jpf.vm.StackFrame;
  31 import gov.nasa.jpf.vm.ThreadInfo;
  32
  33 import java.io.PrintWriter;
  34 import java.util.ArrayList;
  35 import java.util.Collection;
  36 import java.util.HashMap;
  37 import java.util.HashSet;
  38 import java.util.LinkedHashSet;
  39 import java.util.ListIterator;
  40 import java.util.Stack;
  41
  42 /**
  43  * example of a listener that creates property specific traces. The interesting
  44  * thing is that it does so without the need to store steps, i.e. it maintains
  45  * it's own transition stack.
  46  * this is still work in progress, analyzing the trace can be much more
  47  * elaborate (we just dump up to a max history size for now)
  48  *
  49  * <2do> DeadlockAnalyzer output can be confusing if a reorganizing
  50  * ThreadList is used (which reassigns thread ids)
  51  */
  52 public class DeadlockAnalyzer extends ListenerAdapter {
  53
  54   enum OpType { block, lock, unlock, wait, notify, notifyAll, started, terminated };
  55   static String[] opTypeMnemonic = { "B", "L", "U", "W", "N", "A", "S", "T" };
  56
  57   static class ThreadOp {
  58     ThreadInfo ti;
  59     ElementInfo ei;
  60     Instruction insn;
  61
  62     // kind of redundant, but there might be context attributes in addition
  63     // to the insn itself
  64     OpType opType;
  65
  66     // we could identify this with the insn, but only in case this is
  67     // a transition boundary, which is far less general than we can be
  68     int stateId;
  69     ThreadOp prevTransition;
  70     ThreadOp prevOp;
  71
  72     ThreadOp (ThreadInfo ti, ElementInfo ei, OpType type) {
  73       this.ti = ti;
  74       this.ei = ei;
  75       insn = getReportInsn(ti); // we haven't had the executeInsn notification yet
  76       opType = type;
  77
  78       prevOp = null;
  79     }
  80
  81     Instruction getReportInsn(ThreadInfo ti){
  82       StackFrame frame = ti.getTopFrame();
  83       if (frame != null) {
  84         Instruction insn = frame.getPC();
  85         if (insn instanceof EXECUTENATIVE) {
  86           frame = frame.getPrevious();
  87           if (frame != null) {
  88             insn = frame.getPC();
  89           }
  90         }
  91
  92         return insn;
  93       } else {
  94         return null;
  95       }
  96     }
  97
  98     void printLocOn (PrintWriter pw) {
  99       pw.print(String.format("%6d", new Integer(stateId)));
 100
 101       if (insn != null) {
 102         pw.print(String.format(" %18.18s ", insn.getMnemonic()));
 103         pw.print(insn.getFileLocation());
 104         String line = insn.getSourceLine();
 105         if (line != null){
 106           pw.print( " : ");
 107           pw.print(line.trim());
 108           //pw.print(insn);
 109         }
 110       }
 111     }
 112
 113     void printOn (PrintWriter pw){
 114       pw.print( stateId);
 115       pw.print( " : ");
 116       pw.print( ti.getName());
 117       pw.print( " : ");
 118       pw.print( opType.name());
 119       pw.print( " : ");
 120       pw.println(ei);
 121     }
 122
 123     @Override
 124         public String toString() {
 125       StringBuilder sb = new StringBuilder();
 126       sb.append( stateId);
 127       sb.append( " : ");
 128       sb.append( ti.getName());
 129       sb.append( " : ");
 130       sb.append( opType.name());
 131       sb.append( " : ");
 132       sb.append(ei);
 133       return sb.toString();
 134     }
 135
 136     void printColumnOn(PrintWriter pw, Collection<ThreadInfo> tlist){
 137       for (ThreadInfo t : tlist) {
 138         if (ti == t) {
 139           if (opType == OpType.started || opType == OpType.terminated) {
 140             pw.print(String.format("   %1$s    ", opTypeMnemonic[opType.ordinal()]));
 141           } else {
 142             pw.print(String.format("%1$s:%2$-5x ", opTypeMnemonic[opType.ordinal()], ei.getObjectRef()));
 143           }
 144           //break;
 145         } else {
 146           pw.print("   |    ");
 147         }
 148       }
 149     }
 150   }
 151
 152   ThreadOp lastOp;
 153   ThreadOp lastTransition;
 154
 155   int maxHistory;
 156   String format;
 157
 158   VM vm;
 159   Search search;
 160
 161   public DeadlockAnalyzer (Config config, JPF jpf){
 162     jpf.addPublisherExtension(ConsolePublisher.class, this);
 163
 164     maxHistory = config.getInt("deadlock.max_history", Integer.MAX_VALUE);
 165     format = config.getString("deadlock.format", "essential");
 166
 167     vm = jpf.getVM();
 168     search = jpf.getSearch();
 169   }
 170
 171   boolean requireAllOps() {
 172     return (format.equalsIgnoreCase("essential"));
 173   }
 174
 175   void addOp (ThreadInfo ti, ElementInfo ei, OpType opType){
 176     ThreadOp op = new ThreadOp(ti, ei, opType);
 177     if (lastOp == null){
 178       lastOp = op;
 179     } else {
 180       assert lastOp.stateId == 0;
 181
 182       op.prevOp = lastOp;
 183       lastOp = op;
 184     }
 185   }
 186
 187   void printRawOps (PrintWriter pw) {
 188     int i=0;
 189
 190     for (ThreadOp tOp = lastTransition; tOp != null; tOp = tOp.prevTransition){
 191       for (ThreadOp op = tOp; op != null; op=op.prevOp) {
 192         if (i++ >= maxHistory){
 193           pw.println("...");
 194           return;
 195         }
 196         op.printOn(pw);
 197       }
 198     }
 199   }
 200
 201   /**
 202    * include all threads that are currently blocked or waiting, and
 203    * all the threads that had the last interaction with them. Note that
 204    * we do this completely on the basis of the recorded ThreadOps, i.e.
 205    * don't rely on when this is called
 206    */
 207   void printEssentialOps(PrintWriter pw) {
 208     LinkedHashSet<ThreadInfo> threads = new LinkedHashSet<ThreadInfo>();
 209     ArrayList<ThreadOp> ops = new ArrayList<ThreadOp>();
 210     HashMap<ElementInfo,ThreadInfo> waits = new HashMap<ElementInfo,ThreadInfo>();
 211     HashMap<ElementInfo,ThreadInfo> blocks = new HashMap<ElementInfo,ThreadInfo>();
 212     HashSet<ThreadInfo> runnables = new HashSet<ThreadInfo>();
 213
 214     // collect all relevant threads and ops
 215     for (ThreadOp trans = lastTransition; trans != null; trans = trans.prevTransition){
 216       for (ThreadOp tOp = trans; tOp != null; tOp = tOp.prevOp) {
 217         OpType ot = tOp.opType;
 218         ThreadInfo oti = tOp.ti;
 219
 220         if (ot == OpType.wait || ot == OpType.block) {
 221           if (!runnables.contains(oti) && !threads.contains(oti)){
 222             HashMap<ElementInfo, ThreadInfo> map = (ot == OpType.block) ? blocks : waits;
 223             threads.add(oti);
 224             map.put(tOp.ei, oti);
 225             ops.add(tOp);
 226           }
 227
 228         } else if (ot == OpType.notify || ot == OpType.notifyAll || ot == OpType.lock) {
 229           HashMap<ElementInfo, ThreadInfo> map = (ot == OpType.lock) ? blocks : waits;
 230           ThreadInfo ti = map.get(tOp.ei);
 231
 232           if (ti != null && ti != oti){
 233             if (!threads.contains(oti)){
 234               threads.add(oti);
 235             }
 236             map.remove(tOp.ei);
 237             ops.add(tOp);
 238           }
 239
 240           runnables.add(oti);
 241
 242         } else if (ot == OpType.unlock) {
 243           // not relevant
 244           runnables.add(oti);
 245
 246         } else if (ot == OpType.terminated || ot == OpType.started) {
 247           ops.add(tOp); // might be removed later-on
 248         }
 249       }
 250     }
 251
 252     // remove all starts/terminates of irrelevant threads
 253     for (ListIterator<ThreadOp> it = ops.listIterator(); it.hasNext(); ){
 254       ThreadOp tOp = it.next();
 255       if (tOp.opType == OpType.terminated || tOp.opType == OpType.started) {
 256         if (!threads.contains(tOp.ti)){
 257           it.remove();
 258         }
 259       }
 260     }
 261
 262     // now we are ready to print
 263     printHeader(pw,threads);
 264
 265     for (ThreadOp tOp : ops) {
 266       tOp.printColumnOn(pw,threads);
 267       tOp.printLocOn(pw);
 268       pw.println();
 269     }
 270   }
 271
 272
 273   Collection<ThreadInfo> getThreadList() {
 274     ArrayList<ThreadInfo> tcol = new ArrayList<ThreadInfo>();
 275     boolean allOps = requireAllOps();
 276     int i=0;
 277
 278     prevTrans:
 279     for (ThreadOp tOp = lastTransition; tOp != null; tOp = tOp.prevTransition){
 280       i++;
 281       if (!allOps && (i >= maxHistory)){
 282         break;
 283       }
 284
 285       for (ThreadInfo ti : tcol) {
 286         if (ti == tOp.ti) continue prevTrans;
 287       }
 288       tcol.add(tOp.ti);
 289     }
 290
 291     return tcol;
 292   }
 293
 294   void printHeader (PrintWriter pw, Collection<ThreadInfo> tlist){
 295     for (ThreadInfo ti : tlist){
 296       pw.print(String.format("  %1$2d    ", ti.getId()));
 297     }
 298     pw.print(" trans      insn          loc                : stmt");
 299     pw.println();
 300
 301     for (int i=0; i<tlist.size(); i++){
 302       pw.print("------- ");
 303     }
 304     pw.print("---------------------------------------------------");
 305     pw.println();
 306   }
 307
 308
 309   void printColumnOps (PrintWriter pw){
 310     int i = 0;
 311     Collection<ThreadInfo> tlist = getThreadList();
 312     printHeader(pw,tlist);
 313
 314     // and now the data
 315     for (ThreadOp tOp = lastTransition; tOp != null; tOp = tOp.prevTransition){
 316       for (ThreadOp op = tOp; op != null; op=op.prevOp) {
 317         if (i++ >= maxHistory){
 318           pw.println("...");
 319           return;
 320         }
 321
 322         op.printColumnOn(pw,tlist);
 323         op.printLocOn(pw);
 324         pw.println();
 325       }
 326     }
 327   }
 328
 329   /**
 330    * this is the workhorse - filter which ops should be shown, and which
 331    * are irrelevant for the deadlock
 332    */
 333   boolean showOp (ThreadOp op, ThreadInfo[] tlist,
 334                   boolean[] waitSeen, boolean[] notifySeen,
 335                   boolean[] blockSeen, boolean[] lockSeen,
 336                   Stack<ElementInfo>[] unlocked) {
 337     ThreadInfo ti = op.ti;
 338     ElementInfo ei = op.ei;
 339     int idx;
 340     for (idx=0; idx < tlist.length; idx++){
 341       if (tlist[idx] == ti) break;
 342     }
 343
 344     // we could delegate this to the enum type, but let's not be too fancy
 345     switch (op.opType) {
 346     case block:
 347       // only report the last one if thread is blocked
 348       if (ti.isBlocked()) {
 349         if (!blockSeen[idx]) {
 350           blockSeen[idx] = true;
 351           return true;
 352         }
 353       }
 354       return false;
 355
 356     case unlock:
 357       unlocked[idx].push(ei);
 358       return false;
 359
 360     case lock:
 361       // if we had a corresponding unlock, ignore
 362       if (!unlocked[idx].isEmpty() && (unlocked[idx].peek() == ei)) {
 363         unlocked[idx].pop();
 364         return false;
 365       }
 366
 367       // only report the last one if there is a thread that's currently blocked on it
 368       for (int i=0; i<tlist.length; i++){
 369         if ((i != idx) && tlist[i].isBlocked() && (tlist[i].getLockObject() == ei)) {
 370           if (!lockSeen[i]){
 371             lockSeen[i] = true;
 372             return true;
 373           }
 374         }
 375       }
 376
 377       return false;
 378
 379     case wait:
 380       if (ti.isWaiting()){ // only show the last one if this is a waiting thread
 381         if (!waitSeen[idx]) {
 382           waitSeen[idx] = true;
 383           return true;
 384         }
 385       }
 386
 387       return false;
 388
 389     case notify:
 390     case notifyAll:
 391       // only report the last one if there's a thread waiting on it
 392       for (int i=0; i<tlist.length; i++){
 393         if ((i != idx) && tlist[i].isWaiting() && (tlist[i].getLockObject() == ei)) {
 394           if (!notifySeen[i]) {
 395             notifySeen[i] = true;
 396             return true;
 397           }
 398         }
 399       }
 400
 401       return false;
 402
 403     case started:
 404     case terminated:
 405       return true;
 406     }
 407
 408     return false;
 409   }
 410
 411   void storeLastTransition(){
 412     if (lastOp != null) {
 413       int stateId = search.getStateId();
 414       ThreadInfo ti = lastOp.ti;
 415
 416       for (ThreadOp op = lastOp; op != null; op = op.prevOp) {
 417         assert op.stateId == 0;
 418
 419         op.stateId = stateId;
 420       }
 421
 422       lastOp.prevTransition = lastTransition;
 423       lastTransition = lastOp;
 424
 425       lastOp = null;
 426     }
 427   }
 428
 429   //--- VM listener interface
 430
 431   @Override
 432   public void objectLocked (VM vm, ThreadInfo ti, ElementInfo ei) {
 433     addOp(ti, ei, OpType.lock);
 434   }
 435
 436   @Override
 437   public void objectUnlocked (VM vm, ThreadInfo ti, ElementInfo ei) {
 438     addOp(ti, ei, OpType.unlock);
 439   }
 440
 441   @Override
 442   public void objectWait (VM vm, ThreadInfo ti, ElementInfo ei) {
 443     addOp(ti, ei, OpType.wait);
 444   }
 445
 446   @Override
 447   public void objectNotify (VM vm, ThreadInfo ti, ElementInfo ei) {
 448     addOp(ti, ei, OpType.notify);
 449   }
 450
 451   @Override
 452   public void objectNotifyAll (VM vm, ThreadInfo ti, ElementInfo ei) {
 453     addOp(ti, ei, OpType.notifyAll);
 454   }
 455
 456   @Override
 457   public void threadBlocked (VM vm, ThreadInfo ti, ElementInfo ei){
 458     addOp(ti, ei, OpType.block);
 459   }
 460
 461   @Override
 462   public void threadStarted (VM vm, ThreadInfo ti){
 463     addOp(ti, null, OpType.started);
 464   }
 465
 466   @Override
 467   public void threadTerminated (VM vm, ThreadInfo ti){
 468     addOp(ti, null, OpType.terminated);
 469   }
 470
 471   //--- SearchListener interface
 472
 473   @Override
 474   public void stateAdvanced (Search search){
 475     if (search.isNewState()) {
 476       storeLastTransition();
 477     }
 478   }
 479
 480   @Override
 481   public void stateBacktracked (Search search){
 482     int stateId = search.getStateId();
 483     while ((lastTransition != null) && (lastTransition.stateId > stateId)){
 484       lastTransition = lastTransition.prevTransition;
 485     }
 486     lastOp = null;
 487   }
 488
 489   // for HeuristicSearches. Ok, that's braindead but at least no need for cloning
 490   HashMap<Integer,ThreadOp> storedTransition = new HashMap<Integer,ThreadOp>();
 491
 492   @Override
 493   public void stateStored (Search search) {
 494     // always called after stateAdvanced
 495     storedTransition.put(search.getStateId(), lastTransition);
 496   }
 497
 498   @Override
 499   public void stateRestored (Search search) {
 500     int stateId = search.getStateId();
 501     ThreadOp op = storedTransition.get(stateId);
 502     if (op != null) {
 503       lastTransition = op;
 504       storedTransition.remove(stateId);  // not strictly required, but we don't come back
 505     }
 506   }
 507
 508   @Override
 509   public void publishPropertyViolation (Publisher publisher) {
 510     PrintWriter pw = publisher.getOut();
 511     publisher.publishTopicStart("thread ops " + publisher.getLastErrorId());
 512
 513     if ("column".equalsIgnoreCase(format)){
 514       printColumnOps(pw);
 515     } else if ("essential".equalsIgnoreCase(format)) {
 516       printEssentialOps(pw);
 517     } else {
 518       printRawOps(pw);
 519     }
 520   }
 521 }