© 2007 Carnegie Mellon UniversityIntroduction to JavaPathfinderPart 2Software Engineering InstituteCarnegie Mellon UniversityPittsburgh, PA 15213Sagar Chaki27 November 20072Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityOutlineSearch StrategiesPartial-Order ReductionExercisesSome slides borrowed from JavaPathFinder tutorial at ASE conference 2006•http://www.visserhome.com/willem/presentations/ase06jpftut.ppt3Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversitySearch Strategies4Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityUnder the Hood - Search5Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityExtending JPF - ListenersPreferred way of extending JPF: ‘Listener’ variant of the Observer pattern•Keep extensions out of the core classesListeners can subscribe to Search and VM events6Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityExtending JPF - SearchListenerpublic interface SearchListener {/* got the next state */void stateAdvanced (Search search);/* state was backtracked one step */void stateBacktracked (Search search);/* a previously generated state was restored(can be on a completely different path) */void stateRestored (Search search);/* JPF encountered a property violation */void propertyViolated (Search search);/* we get this after we enter the search loop, but BEFORE the firstforward */void searchStarted (Search search);/* there was some contraint hit in the search, we back out could havebeen turned into a property, but usually is an attribute of the search, notthe application */void searchConstraintHit (Search search);/* we're done, either with or without a preceeding error */void searchFinished (Search search);}7Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityExtending JPF - VMListenerpublic interface VMListener {void instructionExecuted (JVM vm); // VM has executed next instructionvoid threadStarted (JVM vm); // new Thread entered run() methodvoid threadTerminated (JVM vm); // Thread exited run() methodvoid classLoaded (JVM vm); // new class was loadedvoid objectCreated (JVM vm); // new object was createdvoid objectReleased (JVM vm); // object was garbage collectedvoid gcBegin (JVM vm); // garbage collection mark phase startedvoid gcEnd (JVM vm); // garbage collection sweep phase terminatedvoid exceptionThrown (JVM vm); // exception was thrownvoid nextChoice (JVM vm); // choice generator returned new value}8Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityExtending JPF - Listener Examplepublic class HeapTracker extends GenericProperty implements VMListener, SearchListener {class PathStat { .. int heapSize = 0; .. } // helper to store additional state infoPathStat stat = new PathStat();Stack pathStats = new Stack();public boolean check (JVM vm, Object arg) { // GenericPropertyreturn (stat.heapSize <= maxHeapSizeLimit);}public void stateAdvanced (Search search) { // SearchListenerif (search.isNewState()) {..pathStats.push(stat);stat = (PathStat)stat.clone(); ..}public void stateBacktracked (Search search) { // SearchListener.. if (!pathStats.isEmpty()) stat = (PathStat) pathStats.pop();}public void objectCreated (JVM vm) {.. // VMListenerElementInfo ei = vm.getLastElementInfo();..stat.heapSize += ei.getHeapSize(); ..}public void objectReleased (JVM vm) { // VMListenerElementInfo ei = vm.getLastElementInfo();..stat.heapSize -= ei.getHeapSize(); ..}}9Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityExtending JPF - Listener ConfigurationListeners are usually configured, not hard codedPer configuration file:search.listener = MySearchListenervm.listener = MyVMListenerjpf.listener = MyCombinedListener:MySecondListener...Per command line:jpf ... +jpf.listener=MyCombinedListener ...Hard coded:MyListener listener= new MyListener(..);..Config config = JPF.createConfig( args);JPF jpf = new JPF( config);jpf. addSearchListener (listener);jpf. addVMListener ( listener);jpf.run();..10Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityPartial-Order Reduction11Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityPartial-Order Reduction (POR)The number of different scheduling combinations is the prevalent factor for the state space size of concurrent programs.Fortunately, for most practical purposes it is not necessary to explore all possible instruction interleavings for all threads.The number of scheduling induced states can be significantly reduced by grouping all instruction sequences in a thread that cannot have effects outside this thread itself, collapsing them into a single transition.This technique is called Partial Order Reduction (POR), and typically results in more than 70% reduction of state spaces.12Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityOn-the-Fly POR in JPFJPF employs an on-the-fly POR that does not rely on user instrumentation or static analysis. JPF automatically determines at runtime which instructions have to be treated as state transition boundaries.If POR is enabled (configured via vm.por property), a forward request to the VM executes all instructions in the current thread until one of the following conditions is met:1.the next instruction is scheduling relevant 2.the next instruction yields a "nondeterministic" result (i.e. simulates random value data acquisition) Detection of both conditions are delegated to the instruction object itself (Instruction.execute(..)), passing down information about the current VM execution state and threading context.If the instruction is a transition breaker, it creates a ChoiceGenerator and schedules itself for re-execution.13Intro to JPF: Part 2Sagar Chaki, 27 Nov 07© 2007 Carnegie Mellon UniversityDetermining Scheduling Relevance (1)Each bytecode instruction type corresponds to a concrete gov.nasa.jpf.Instruction subclass that determines scheduling relevance based on the following factors:Instruction TypeDue to the stack based nature of the JVM, only about 10% of the Java bytecode instructions are scheduling relevant, i.e. can have effects across thread boundaries. The interesting instructions include direct synchronization (monitorEnter, monitorExit, invokeX on synchronized methods), field access (putX, getX), array element access (Xaload, Xastore), and invoke