[Javapathfinder-svn] SF.net SVN: javapathfinder:[1544] branches/mango/MangoJPF

[<fra...@us...>]

Revision: 1544
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1544&view=rev
Author:   frankrimlinger
Date:     2009-05-22 17:44:18 +0000 (Fri, 22 May 2009)

Log Message:
-----------

The instructions that potentially fire clinits are called the clinit-4 instructions, defined in JVM 2nd ed, new, getstatic, putstatic, invokestatic.  

The constraints on the problem are like so: if a class has only final data, then it is easy and cheap to punch in these values with rewrite rules.  So the clinit for such a class can be ignored.  On the other hand, if a class has non final data, then the clinit must fire in an order dependent way with respect to the other clinits that must fire.  

Mango detects which clinits must fire by observing, for each modelled class which contains a clinit, if that clinit contains a clinit-4 instruction.  Such modelled classes are said to have "commuting clinits".  

OK, any clinit-4 instruction which potentially may fire a commuting clinit must be preceded by a conditional clinit invocation.  This condition is simply that the clinit is at the "beginning of time".  The idea is that these conditional clinit invocations commute backwards through the flow control and bunch up at the beginning of time, where they then can fire in order.  As a clinit fires, it propagates the beginning of time property to its immediate successor, who then can also fire.

There are two issues here, performance and soundness.  The performance issue is like so: in the old two pass phase1, it was possible to catalogue the classes with commuting clinits during the first pass, so that formal state transition built in the second pass would only have to add the conditional clinit logic to the clinit-4's referencing commuting clinits.  However, now that we only have one pass, we are still building the catalogue when the decision of whether or not to add conditional logic comes up.  We could cheat, and just inspect each class info for evidence of non-final data, but I think this is fraught with danger.  Instead, just go ahead and punch in commuting clinit logic for EVERY clinit-4 instruction.  However, enhance the condition to check the catalogue at evaluation time.  By this means, the unnecessary conditional invocations will evaporate just-in-time.  

As for soundness, the BIG problem is that the survey is only over mango modelled classes, so the procedure is inherently unsound: a clinit-4 that fires an unmodelled commuting clinit will not be modelled correctly.  The outstanding example of this is java.lang.System, whose clinit must fire to produce the popular static field java.lang.System.out.  

Soundness may be addressed as follows:  assume that every mango native method presents an ordered list of clinits which must potentially fire prior to invocation.  Now add the invocation instructions (invokestatic, invokevirtual, invokespecial, invokeinterface) to the new invoke-4 list.  Now for each invoke-4 instruction, arrange so that the branch condition to a mango native method is preceded by the indicated sequence of potential clinit invocatons.  These invocations may now commute back to the beginning of the target method.  

Ok, its a little more complicated than that, because the target method may have several cases, so for each case, there must be an ordered list of clinits, but the basic idea is there.  It would then be necessary to store these lists in the rulebase, as well as abstracted clinit functionality.

So, even if there was never a beginning of time, there would still be a record of what clinits could affect a given method, and this is good information for informed reasoning about the situation.  Notice we can't actually fire the clinits unless we can make some kind of temporal order invariance assumption.

Its hard to imagine what traction a meta-theory for such assumptions could achieve.  For example, after java.lang.out is created, it can be reassigned at will to print to this or print to that, so what can an arbitrary method actually "know" about java.lang.out.  So at the end of the day, you still just come back to reasoning about abstractions. I guess that the point is, at the very least, you have an inventory of things that need to be abstracted.

This is a scalable idea that really should be implemented some day.  For now, punt on soundness, and just say that clinits are "soundness ready".  

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.