2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.listener;
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;
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;
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)
49 * <2do> DeadlockAnalyzer output can be confusing if a reorganizing
50 * ThreadList is used (which reassigns thread ids)
52 public class DeadlockAnalyzer extends ListenerAdapter {
54 enum OpType { block, lock, unlock, wait, notify, notifyAll, started, terminated };
55 static String[] opTypeMnemonic = { "B", "L", "U", "W", "N", "A", "S", "T" };
57 static class ThreadOp {
62 // kind of redundant, but there might be context attributes in addition
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
69 ThreadOp prevTransition;
72 ThreadOp (ThreadInfo ti, ElementInfo ei, OpType type) {
75 insn = getReportInsn(ti); // we haven't had the executeInsn notification yet
81 Instruction getReportInsn(ThreadInfo ti){
82 StackFrame frame = ti.getTopFrame();
84 Instruction insn = frame.getPC();
85 if (insn instanceof EXECUTENATIVE) {
86 frame = frame.getPrevious();
98 void printLocOn (PrintWriter pw) {
99 pw.print(String.format("%6d", new Integer(stateId)));
102 pw.print(String.format(" %18.18s ", insn.getMnemonic()));
103 pw.print(insn.getFileLocation());
104 String line = insn.getSourceLine();
107 pw.print(line.trim());
113 void printOn (PrintWriter pw){
116 pw.print( ti.getName());
118 pw.print( opType.name());
124 public String toString() {
125 StringBuilder sb = new StringBuilder();
128 sb.append( ti.getName());
130 sb.append( opType.name());
133 return sb.toString();
136 void printColumnOn(PrintWriter pw, Collection<ThreadInfo> tlist){
137 for (ThreadInfo t : tlist) {
139 if (opType == OpType.started || opType == OpType.terminated) {
140 pw.print(String.format(" %1$s ", opTypeMnemonic[opType.ordinal()]));
142 pw.print(String.format("%1$s:%2$-5x ", opTypeMnemonic[opType.ordinal()], ei.getObjectRef()));
153 ThreadOp lastTransition;
161 public DeadlockAnalyzer (Config config, JPF jpf){
162 jpf.addPublisherExtension(ConsolePublisher.class, this);
164 maxHistory = config.getInt("deadlock.max_history", Integer.MAX_VALUE);
165 format = config.getString("deadlock.format", "essential");
168 search = jpf.getSearch();
171 boolean requireAllOps() {
172 return (format.equalsIgnoreCase("essential"));
175 void addOp (ThreadInfo ti, ElementInfo ei, OpType opType){
176 ThreadOp op = new ThreadOp(ti, ei, opType);
180 assert lastOp.stateId == 0;
187 void printRawOps (PrintWriter pw) {
190 for (ThreadOp tOp = lastTransition; tOp != null; tOp = tOp.prevTransition){
191 for (ThreadOp op = tOp; op != null; op=op.prevOp) {
192 if (i++ >= maxHistory){
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
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>();
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;
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;
224 map.put(tOp.ei, oti);
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);
232 if (ti != null && ti != oti){
233 if (!threads.contains(oti)){
242 } else if (ot == OpType.unlock) {
246 } else if (ot == OpType.terminated || ot == OpType.started) {
247 ops.add(tOp); // might be removed later-on
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)){
262 // now we are ready to print
263 printHeader(pw,threads);
265 for (ThreadOp tOp : ops) {
266 tOp.printColumnOn(pw,threads);
273 Collection<ThreadInfo> getThreadList() {
274 ArrayList<ThreadInfo> tcol = new ArrayList<ThreadInfo>();
275 boolean allOps = requireAllOps();
279 for (ThreadOp tOp = lastTransition; tOp != null; tOp = tOp.prevTransition){
281 if (!allOps && (i >= maxHistory)){
285 for (ThreadInfo ti : tcol) {
286 if (ti == tOp.ti) continue prevTrans;
294 void printHeader (PrintWriter pw, Collection<ThreadInfo> tlist){
295 for (ThreadInfo ti : tlist){
296 pw.print(String.format(" %1$2d ", ti.getId()));
298 pw.print(" trans insn loc : stmt");
301 for (int i=0; i<tlist.size(); i++){
302 pw.print("------- ");
304 pw.print("---------------------------------------------------");
309 void printColumnOps (PrintWriter pw){
311 Collection<ThreadInfo> tlist = getThreadList();
312 printHeader(pw,tlist);
315 for (ThreadOp tOp = lastTransition; tOp != null; tOp = tOp.prevTransition){
316 for (ThreadOp op = tOp; op != null; op=op.prevOp) {
317 if (i++ >= maxHistory){
322 op.printColumnOn(pw,tlist);
330 * this is the workhorse - filter which ops should be shown, and which
331 * are irrelevant for the deadlock
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;
340 for (idx=0; idx < tlist.length; idx++){
341 if (tlist[idx] == ti) break;
344 // we could delegate this to the enum type, but let's not be too fancy
347 // only report the last one if thread is blocked
348 if (ti.isBlocked()) {
349 if (!blockSeen[idx]) {
350 blockSeen[idx] = true;
357 unlocked[idx].push(ei);
361 // if we had a corresponding unlock, ignore
362 if (!unlocked[idx].isEmpty() && (unlocked[idx].peek() == ei)) {
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)) {
380 if (ti.isWaiting()){ // only show the last one if this is a waiting thread
381 if (!waitSeen[idx]) {
382 waitSeen[idx] = true;
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;
411 void storeLastTransition(){
412 if (lastOp != null) {
413 int stateId = search.getStateId();
414 ThreadInfo ti = lastOp.ti;
416 for (ThreadOp op = lastOp; op != null; op = op.prevOp) {
417 assert op.stateId == 0;
419 op.stateId = stateId;
422 lastOp.prevTransition = lastTransition;
423 lastTransition = lastOp;
429 //--- VM listener interface
432 public void objectLocked (VM vm, ThreadInfo ti, ElementInfo ei) {
433 addOp(ti, ei, OpType.lock);
437 public void objectUnlocked (VM vm, ThreadInfo ti, ElementInfo ei) {
438 addOp(ti, ei, OpType.unlock);
442 public void objectWait (VM vm, ThreadInfo ti, ElementInfo ei) {
443 addOp(ti, ei, OpType.wait);
447 public void objectNotify (VM vm, ThreadInfo ti, ElementInfo ei) {
448 addOp(ti, ei, OpType.notify);
452 public void objectNotifyAll (VM vm, ThreadInfo ti, ElementInfo ei) {
453 addOp(ti, ei, OpType.notifyAll);
457 public void threadBlocked (VM vm, ThreadInfo ti, ElementInfo ei){
458 addOp(ti, ei, OpType.block);
462 public void threadStarted (VM vm, ThreadInfo ti){
463 addOp(ti, null, OpType.started);
467 public void threadTerminated (VM vm, ThreadInfo ti){
468 addOp(ti, null, OpType.terminated);
471 //--- SearchListener interface
474 public void stateAdvanced (Search search){
475 if (search.isNewState()) {
476 storeLastTransition();
481 public void stateBacktracked (Search search){
482 int stateId = search.getStateId();
483 while ((lastTransition != null) && (lastTransition.stateId > stateId)){
484 lastTransition = lastTransition.prevTransition;
489 // for HeuristicSearches. Ok, that's braindead but at least no need for cloning
490 HashMap<Integer,ThreadOp> storedTransition = new HashMap<Integer,ThreadOp>();
493 public void stateStored (Search search) {
494 // always called after stateAdvanced
495 storedTransition.put(search.getStateId(), lastTransition);
499 public void stateRestored (Search search) {
500 int stateId = search.getStateId();
501 ThreadOp op = storedTransition.get(stateId);
504 storedTransition.remove(stateId); // not strictly required, but we don't come back
509 public void publishPropertyViolation (Publisher publisher) {
510 PrintWriter pw = publisher.getOut();
511 publisher.publishTopicStart("thread ops " + publisher.getLastErrorId());
513 if ("column".equalsIgnoreCase(format)){
515 } else if ("essential".equalsIgnoreCase(format)) {
516 printEssentialOps(pw);