Consultant Log

Consultation Date,Time,
Consultation 2 28th April 2003,
1:30pm - 2:30pm,
One of the issue discussed in this consultation is regarding the scope of the RUP. "Should the RUP be applied across the whole program or if it's possible that some form of scoping is possible to apply different RUP across different scope of a program. The discussion has a conclusion that it's possible to apply scoping into the RUP but for the project-wise, this will not be applied and we shall concentrate on 1 RUP applied across the whole program.
With regards to the Scoping Methods discussed in other paper on RUV, we have analysis it and decided that there are some flaws in the way how RUV is enforced. "Synthesized Effects" as discussed in the paper can be infered so that it will be less error prone as well as it will simplify the whole process. Resource usage is enforced by encoding a prefix of codes and postfix of codes so that before and after the body of operations in concerned, the resource policy is not broken. Such a method is cumbersome and also not global. In analysing the Scoping Methods in RUV that we hope that it will enlighten us on how inheritance and polymorphism may complicate the RUV but seems like it has little help.
In this consultantion, the lecturer has sheered some light on the fix point theory on how to compute the calling patterns, based on the formula on page of the paper[1]
Due to the fact that the lecturer will be not free for the coming month, there shall be no consultation for awhile. The task at hand now is to find the C grammar and also perform a demo on computing the calling pattern successfully.
  1. Resource Usage Verification (Kim Marriott, Peter J. Stuckey, Martin Sulzmann)
Consultation 1 22nd April 2003,
First HYP consultation
Clarification of intention of project :
Given L(GCFG) L(GDFA), where GCFG is an approximation of the behaviour of the program and GDFA is the Determinstic Finite Automata(DFA) of the Resource Usage Policy(RUP), we are able to ensure that the behaviour of the program will not violate the RUP.
Question is posed on why the RUV couldn't be performed on 2 GCFG such that it will be a testing on L(GCFG) L(GCFG)? The reason is that it is generally undecidable to test for entailment between two CFG grammars.
Other suggested approaches have considered using regular expression to approximate the program, but the approach is not refine enough and will introduce unnecessary runtime tests being augmented into the program.
Given example program,

proc f()
   if (...)

The approximated CFG will be as follows

F  -> IF
IF ->
є | read F write

Hence, for L(F) = { є, read write, read2 write2, read3 write3, readn writen}

But if a regular expression will be used, it will be F' = (read | write)*

If the RUP is defined by a DFA as

We will find that the regular expression will not be able to approximate the program as closely and as accurately as the CFG

We have discussed on the issues that might arise from the which particular language might be used for the Resource Usage Verification(RUV). The 2 language suggested are Java and C. In C, things will be simpler because of no classes scoping but pointers in C might pose a problem when coming to deciphering which particular function is called at runtime. Java also faced such problems when coming to overloading and overwriting of methods in polymorphism.

Given the following classes

class A
   void f()

class B extends A
   void f()

if having a code as such

void main()
   A a = ...

We might not be able to decipher at compile time which function of instance `a' is invoked because `a' can be either instance of class A or B, which at times might be undecidable. Hence of tackle this particular problem, 2 solutions are suggested

  1. We check that overloaded methods of class A and subclasses of A must comply to the following rule
    L(A.f) | for all B subclasses(A)
    In this way, since A.f is the most relax function that satisfy the RUP, therefore the more constraint overloaded functions in the subclasses of A will of course also comply to the RUP.
  2. Another approach will be to adopt a brute force method that we check that all overloaded functions used do comply to the RUP. Of course, such a method might not be feasible because we understand that the depth of inheritance can be deep at times and would make the analysis inefficient.
Languages that may allow templating are also discusses on how the might be augmented to perform RUV on them. Given the following possible code:

void <X> g(X a)

We can see that the type of `a' depends on `X'. Hence the CFG to represent the program will have to include information to decipher the type of `a' as such

G(X) -> open X.F close

Hence at analysis time, X can be replaced with 'A' if it's the assigned type, which render

G(A) -> open A.F close

With regards to the fix point algorithm discuss in the paper to compute reach, we will discussed over it.


f q0 = {q0 q1}
f q1 = {q0 q1 q2}
f q2 = {q0 q1 q2}

s1 = {q0}
s2 = f s1 = {q0 q1}
s3 = f s2 = {q0 q1 q2}
s4 = f s3 = {q0 q1 q2}

therefore s3 = s4 = f s3 =* fn s3

What we can conclude from here is we have reached the fix point at s3 and the implementation must be able to detect it and halt the computation and carry on with the others.

In the next consultation, the following points will be discussed
  • look indepth into languages C and Java and understand further on what issues we need to solve to correctly implement RUV in them.
  • discussion of the implementation of reach algo
  • look into pointers in C
  • decide on a language to be analyse