Consultation 2 |
28th April 2003,
1:30pm - 2:30pm,
Office |
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. |
- Resource Usage Verification (Kim Marriott, Peter J.
Stuckey, Martin Sulzmann)
|
|
Consultation 1 |
22nd April 2003,
1pm-2pm,
Office |
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 (...)
{
read;
f();
write;
}
}
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 = ...
a.f();
}
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
- We check that overloaded
methods of class A and subclasses of A must comply to the
following rule
L(B.f) ≤ 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.
- 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)
{
open;
a.f();
close;
}
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. Given
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
|
|