[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Extend Jimple keywords

I will explain firstly the idea of Bandera then our synchronous language and finally why I need to modify jimple.
The answers for Navin and Chris questions are also included.

1. Roughly speaking, Bandera is a set of tools that takes a Java program, generates it to Jimple, applies some techniques to optimize the program, optimize the specification (written in temporal logics) of the program, then generates the optimized Jimple to a back-end model-checker such as SMV or SPIN. Bandera has a tool called JJJC (Java-Jimple-Java compiler) that generates a Jimple file directly from a Java source file and de-generates a Java file from a Jimple code (in case the model-checker reports a counter example).

2. Our synchronous Java language (called sJava) is an extension to Java (has all features of Java). sJava has some new keywords (such as active, select, accept) that support synchronization in concurrent Java applications. sJava has its own compiler and kernel (or VM).
A sJava object has methods as a normal Java object, but if another object wants to call these methods, the caller can not itseft decide to executing the method, it must wait until the called object ACCEPTs the call, then both objects can continue their executions. The synchronization happens at this moment.

The example I have shown (more detail now):
-----------------------------------
active class A{

CallerClass caller = new CallerClass();
public void my_method(){ ... }

public void run(){
for (;;)
select{
case accept my_method;
blockStmt0;
case caller.calling_method(param);
blockStmt1;
}
}}
}
-------------------------------------
'active': a sJava object
CallerClass is another sJava object that contains a method calling_method(param).
The idea of select and accept:
When the thread of class A arrives at "select" statement, it will be postponed, wait for one of the events in the 2 cases happen:
- If some other object calls the method "my_method", the thread of A will accept that call and continue to execute blockStmt0 and exit the select block.
- If the object "caller" accepts the call "caller.calling_method" of thread of A, then thread of A will execute calling_method, then exit the select block.

:::The sJava compiler generates the above sJava to Java as the following:
...
int PC;
LinkedList list;
for (;;)
collectCase(list, null, my_method);
collectCase(list, caller, calling_method);
PC = syncWait(list);
switch(PC){
case 0: // accept my_method
blockStmt0;
break;
case 0: // execute calling_method
caller.calling_method(param);
blockStmt0;
break;
}
}
...
collectCase(listOfCase, callerObject, methodName) and syncWait(listOfCase) are the methods of the sJava kernel.

::: The sJava kernel: collects all cases of the select (method collectCase: add my_method to A.list, if the second parameter is null, this is an accept, otherwise, it is a call to the method 'calling_method' of object 'caller'). Then calculates (syncWait) if there is any pair calling-caller (a rendezvous - a call and an accept of the same method of an object), if a rendezvous happens, then the value PC will indicate which case has been occured in the kernel, then corresponding to PC, a case in switch will be executing.

3. Why modifying Jimple and JJJC.
!!! If I input the converted-java above to JJJC, then I must bring the whole sJava kernel to Bandera as input program, and by consequence, Bandera will analyze also this kernel!!!! The huge number of state will be generated from the sJava Kernel classes! This is what I mean "explosion" (not the original meaning in state explosion in model checking).

This is the reason why I wanted to bring sJava kernel to the JJJC library and modify the latter parts of Bandera according to these changes.

The jimple code will be generated:
---------------------
class A extend java.lang.Object{
 public static void main(java.lang.String[]){
   LinkedList list;
   ...
  addCase list my_method;
  addCase list caller calling_method;
  PC = syncWait list;
  lookupswitch(PC){
    case 0: goto label0;
    case 1: goto label1;
 }
 label0:
    //do something
    blockStmt0;
    goto label2:
 label1:
    staticinvoke [caller.calling_method():void](param);
    blockStmt1;
 label2:
...
-------------------------

When the Jimple Reader (the latter part of Bandera that reads jimple code, then analyzes and generates to one of the back-end model-checker) arrive at 'addCase', 'syncWait' statement, it will call the corresponding methods collectCase, SyncWait in Jimple Reader library, then make the internal calculation (search for a rendezvous), then return only the value of PC! By this way, Bandera will eleminate all the unnecessary states that was created as 'internal'.

About the new keywords: as I said, collectCase and syncWait are the keywords in jimple, but collectCase() and syncWait() are the methods in Jimple-Reader, it will be used when Jimple Reader scanning through these new keywords. The same idea as when Jimpe-Reader goes through the "entermonitor" and "exitmonitor" statement in jimple, Jimpe-Reader should know what to do with this (I am not wrong!)

About Shimple, I have a look at that, but the Bandera I am using does not use the funtion in Shimple, so I can not think about that so far, unless I plan to turn out a new solution for my sJava model-checker completely Soot (by using the byte code analysis and optimisation in Soot)!

This is a really long explanation, sorry for that. I tried to explan shortly, but it's difficult to make it clear. Even now it is still NOT! :)

Anyway, if you have time, please give me some more idea on that. Thank you in advance.
Questions to elaborate the problem are very much welcome.
Regards,
Duy

----------------------------------
Vo Duc Duy - Doctoral Assistant Computer Science Department
Swiss Federal Institute of Technology
1015 Lausanne Switzerland

Phone: (+41 21) 693 6776
Email: duy.voduc@epfl.ch
----------------------------------