Soundness proof for restricted EPRFJ
	------------------------------------

Amit Sasturkar and Scott D. Stoller		24 January, 2005.
------------------------------------------------------------------

This document presents the semantics and typing rules for a core
subset of Extended Parameterized Race Free Java (EPRFJ) and describes
a soundness proof for the type system. The soundness proof is based
closely on the soundness proof in [1]. 

The type system presented here differs from the Extended Parameterized
Atomic Java (EPAJ) type system [4]
in the following respects. 

(1) It does not include the atomicity type system, and the related
    constructs (write_guarded_by clause, etc). We do not prove
    soundness of the atomicity type system because in EPAJ we use the
    atomicity type system of [2] without modifications. Since 
    soundness of atomicity types depends only on soundness of the
    race-free type system, we prove soundness for a race-free subset
    of EPAJ.

(2) It does not support "readonly" and "unique" objects, and the 
    constructs (!e modifer and "where" clauses) necessary
    for supporting them. Also, it does not support "thisThread" and
    thread-local objects. Proving soundness of "thisThread", "unique"
    and "readonly" annotations is orthogonal to proving soundness for the
    "self" and "f$e" annotations that are the principal changes in
    EPAJ compared to [3].

(3) 'let' construct added.

(4) New judgements added : 
    P; E |- ls  , P;E |- l \in ls, P;E |- ls \in ls'
    These are not really necessary, but are included for
    uniformity with [1].

(5) No "simplify" function since we do not have thisThread, unique and
    readonly. 

(8) Following [1], final expressions can only be variables or
    addresses and not dereferences of final fields. 
    This is essential for a proof based on the proof in [1] to work. 

The grammar for restricted EPRFJ
--------------------------------

Non-terminals are in capitals. Terminal symbols reflect the syntax.


P ::= DEFN* E
DEFN ::=  class CN<FORMAL+> extends C BODY
C    ::=  CN<FORMAL+> | Object<FORMAL>
BODY ::= {FIELD* METH* }
FIELD ::= final? T FD = v [GUARDEDBY LOCK]? 
METH ::= T MN(ARG*) requires (LOCK*)  { E }
ARG ::= T X
T ::= PRIM_TYPE | OBJ_TYPE 
OBJ_TYPE ::= CN<OWNER+> | Object<OWNER>
PRIM_TYPE ::= int | bool | long
OWNER ::= FORMAL | self | E_final | OWNER$E_final
GUARDEDBY ::= guarded_by
LOCK ::= E_final | FORMAL$E_final
E :: = v | new OBJ_TYPE | E.fd | E.fd =E | let X = E in E 
       | E.MN(E*) | synchronized E E | E.fork 
       | in-sync p E

CN \in class names
FD \in field names
MN \in method names
X \in variable names
FORMAL  \in formal owner names
v \in values  (int, long, bool, address)
p \in address

Asterix(*), plus (+), and question mark (?) indicate any number, 1 or more, 
and 0 or 1 occurences, respectively. Square brackets are used for grouping. 
E_final ranges over final expressions as defined in the paper.

in-sync construct cannot appear in the source program.
-----------------------------------------------------------------------------


We use the following typing judgements.

|- P : t   (Program P is well typed and its main expression has type t)
P |- defn  (defn is a well-formed class definition)
P |- E  (E is a well formed typing environment)
P;E |- meth (meth is a well formed method)
P;E |- field   (field is a well formed field)
P;E |- t   (t is a well formed type)

The next three judgements are added for uniformity with [1]
P;E |- ls  (ls is a well formed lockset)
P;E |- l \in ls (lock l is contained in lockset ls)
P;E |- ls \subseteq ls' (lockset ls is a subset of ls')

P;E |- t1 <: t2  ( t1 is a a subtype of t2)
P |- meth \in cn<o_1..n>  (class cn<f1..n> either declares or 
                              inherits meth)
P;E;ls |-_final e : t   (e is a final expression with type t)
P;E |-_owner o   (o is a well formed owner)
P;E |-_owner_formal f (f is a formal owner parameter declared in E)
P;E |-_lock e  (e is a well-formed lock)
P;E |- e : t (expression e has type t provided all necessary locks are
              held)
P;E;ls |- e : t   (expression e has type t provided all necessary
                   locks are in ls)

The following judgements are needed because we support method owner parameters.

P; E |- \theta (\theta is a well-formed substitution)
P; E; <\theta,c> |-_inst field  (field in class c is instantiated with
the substituion \theta) 
P; E; <\theta,c> |-inst meth  (meth in class c is instantiated with
the substituion \theta) 

In the second judgement above, the c on the left determines bindings
for all of the formal owner parameters in the declaration of field;
theta is included only for syntactic uniformity with the third
judgment, and in this judgement is always instantiated with the empty
substitution.  In the third judgment above, theta binds all of the
formal owner parameters in the declaration of meth (which are all
interpreted as method owner parameters, even if they have the same
names as some formal owner parameters in the declaration of class c),
and c is used only to look up the declaration of the method in that
class; bindings of the class owner parameters in c are ignored in this
judgment.

We also use the following predicates.

ClassOnce(P)  :- No class is declared twice in P
WFClasses(P)  :- No cycles in class hierarchy
FieldsOnce(P) :- No class in P contains two fields of same name, either 
                 declared or inherited.
MethodsOncePerClass(P) :- No method name appears more than once per class.
OverRidesOk(P) :-  Each overriding method has the same return type and 
                  parameter types (including the owner parameters) as the 
                  methods being overridden, except for the {\tt this} 
                  argument where the class names differ but the  owner  
                  parameters are same. The requires clause of each overriding 
                  method is the same or a subset of the  requires clause of 
                  the methods being overridden. 

One of the main changes in this type system compared to Boyapati's
PRFJ is the way we write requires clause and guarded_by clause. 
Both requires and guarded_by clauses contain locks. A lock 
is either a final expression  or of the form f$e where e is a final expression
that has type cn<o_1,o_2,...,o_n> and f is a formal
owner parameter which is one of { o_1,o_2,...,o_n }

The notation f$e is used to correctly handle the annotation 'self' 
in the presence of formal owner parameters in methods. It is also
used to get the effect of 'RootOwner' without explicitly defining
RootOwner of objects. The reason why we need this notation is that
when a formal owner parameter is instantiated with 'self', we need to 
know what is the actual object that should replace the formal owner 
parameter. For example consider

class A<f> {
  int i;

  m(A<g> a)  requires g{
   a.i = 10;
  } 
}

Now suppose we have A<self> a  and we call m(a), in the requires clause
of m(), g should be replaced by a. Thus we need to keep track that when
g gets instantiated with 'self', it should really be replaced by a. The way
to do this is by writing the requires clause as g$a. We can then define
how such requires clauses are instantiated. 

Let sigma be a substitution. sigma is of the form [o_1/f_1,...,o_n/f_n]
Let E be the environment. Then, g$a[sigma] is defined as follows.

g$a[sigma] =  a[sigma]           if g[sigma] = self
	      g[sigma]$a[sigma]  if P;E |-owner_formal g[sigma] 
	      g[sigma]           otherwise


Note that applying the empty substitution simplifies the lock expression.
  g$a[] = g  if g is a special owner parameter.
             g$a otherwise.   


[PROG]

ClassOnce(P) WFClasses(P) MethodsOncePerClass(P)
FieldsOnce(P) OverRidesOk(P)
P = defn_1...n e
P |- defn_i    
P; \emptyset ; \emptyset |- e : t
----------------------------------------------------
  |- P : t 


[CLASS]

g_i = owner_formal f_i
E = g_1,g_2,...,g_n
P;E |- c
P;E,final cn<f_1,f_2,...,f_n> this |- field_i  for i=1..j
P;\emptyset |- meth_i  for i=1..k
----------------------------------------------------------------
   P |- class cn<f_1,f_2,...,f_n> extends c 
	{field_1, field_2,...,field_j  meth_1,meth_2,...,meth_k}


owner_formal f_i says that the type of f_i is owner_formal, i.e. f_i
is a formal owner parameter. Note that the grammar ensures that each
f_i is a formal owner parameter, thus we do not need to check isFormal(f_i)
Since explicit declaration of 'this' is required in method
declarations, and method owner parameters are allowed, the empty
environment can be used to type-check methods.
The [METHOD] rule adds 'this' and the method owner parameters to the
environment before typechecking the method body. 


Well-formed Owners
-------------------

[OWNER_FORMAL]

P |- E
E = E_1, owner_formal f, E_2
-----------------------------
P;E |-_owner_formal f



[LOCK FINAL]

P;E |-_final e : t 
----------------------
P;E |-_lock e


[LOCK FORMAL]

P;E |-owner_formal f
P;E |-_final e : cn<o_1,o_2,...,o_n> 
f \in {o_1,o_2,...,o_n}
-----------------------------------------
P;E |-_lock f$e


[OWNER SELF]

P |- E
-----------------
P;E |-_owner self


[OWNER FORMAL]

P;E |-_owner_formal f
-----------------------------
P;E |-_owner f


[OWNER LOCK]

P;E |-_lock e
----------------------
P;E |-_owner e


[LOCK SET EMPTY]

------------------
P; E |- \emptyset

[LOCK SET]

P;E |- ls
P;E |-_lock l
-------------------
P; E |- ls U { l }


[LOCK SET ELEM]

P;E |- ls
P;E |-_lock l
l \in ls
---------------
P;E |- l \in ls

[LOCK SET SUBSET]

P;E |- ls P;E |- ls'
ls \subseteq ls'
---------------------
P;E |- ls \subseteq ls'


Well-formed Environment
------------------------

[ENV \emptyset]

-------------- 
P |- \emptyset

Empty environment is well-formed.

[ENV OWNER_FORMAL]

P |- E   f \notin Dom(E)
---------------------------
P |- E, owner_formal f


[ENV VAR]

P;E |- t    x \notin Dom(E)
---------------------------
P |- E, t x


[ENV ADDRESS]

P; E |- c   
p \notin Dom(E)
-------------------------
P |- E, c p 


Well-formed Types
------------------

[TYPE INT]

P |- E
----------
P;E |- int


[TYPE LONG]

P |- E
----------
P;E |- long


[TYPE BOOL]

P |- E
----------
P;E |- bool


[TYPE OBJECT]

P;E |-_owner o
-----------------
P;E |- Object<o>


[TYPE C]

P;E |-_owner o_i
class cn<f_1,f_2,...,f_n> { ... } \in P
--------------------------------------
P;E |- cn<o_1,o_2,...,o_n>

[SUBTYPE REFL]

P;E |- t
--------------
P;E |- t <: t


[SUBTYPE CLASS]


P;E |- c <: cn<o_1,o_2,...,o_n>
cn<f_1,f_2,...,f_n> extends cn'<f'_1,f'_2,...,f'_m> { .. } \in P
-------------------------------------------------------------------------
P;E |- c <: cn'<f'_1,f'_2,...,f'_m>[o_1/f_1]...[o_n/f_n]


Well-formed substitution
------------------------

[SUBSTITUTION]

forall x \in dom(\theta)
  P;E |-_owner \theta(x)
-----------------------
P;E |- \theta

This rule checks that \theta is a well formed substitution.
Every element in the domain of \theta should be mapped to an owner. 


[FIELD INSTANTIATE]

P;E |- c <: cn<o_1..n>
class cn<f_1..n> extends c' { .... field .... } \in P
\theta'=[o_1/f_1,...o_n/f_n]
-------------------------------------------
P;E;<\theta,c> |-_inst field[\theta']


Note that the substituion necessary for instantiating the formal
parameters in the field's type is constructed from the type of the
enclosing class "cn". The substitution \theta is ignored.

[FIELD INIT]

P; E; \emptyset |- v : t
if t = cn<o_1,o_2,...,o_n>
   o_i is not a special owner for i=1..n 
P;E |-_lock l
-----------------------------------------------
P;E |- t fd = v guarded_by l   

The type of a field cannot contain special owners (self); it 
can only contain a lock (final expression or f$e) or
a formal owner parameter. 
A guarded_by clause can only contain lock expressions.

[FINAL FIELD INIT]

P; E; \emptyset |- v : t
if t = cn<o_1,o_2,...,o_n>
   o_i is not a special owner for i=1..n 
--------------------------------------------------------------------------
P;E |- final t fd  = v

[METHOD DECL/INHER]

P;E |- c <: cn<o_1..n>
class cn<f_1..n> extends c' { .... meth .... } \in P
---------------------------------------------
P; E |- meth \in c

This rule checks if a method is declared or inherited in a class. It
does not initialize the method owner parameters.

[METHOD INSTANTIATE]

P;E |- \theta
P;E |- meth \in c
MethodOwnerParams(meth) \subseteq dom(\sigma)
---------------------------------------------
P;E;<\theta,c> |-_inst meth[\theta]

Note that the type of the class (c) is only used to check that
the method is available in that class. The substitution that
instantiates the method parameters is constructed externally, and
passed to the rule as an argument (P;E;<\theta,c>) 

[METHOD]

E' =  E U {owner_formal f | f appears in some arg_i and not in E}
E'' = E', arg_0, arg_1, ... arg_n
P; E' |- t
P; E'' |- ls  (ls is a well formed lockset)
P; E''; ls |- e : t 
---------------------------------------------------------------------------
P; E |- t mn(arg_0,arg_1,...,arg_n) 
      requires ls  { e } 

Add the method owner parameters to the environment. Both E' and E''
must be well-formed; this ensures that the types of the arguments are
well formed. Also, the return type and argument types in the method  
should not contain 'this'. 


[EXP TYPE]
There exists ls 
 P; E; ls |- e : t 
-------------------------------
P; E |- e : t

[EXP SUB]

P; E ; ls |- e : t1
P; E |- t1 <: t  
----------------------------------
P; E; ls |- e : t 


[EXP NEW]

P;E |- c  P;E |- ls
-------------------------
P;E;ls |- new c : c  

[EXP VAR]

P; E |- ls  
E = E1, t x , E2
-----------------------------
P; E; ls |- x : t

[EXP ADDRESS]

P; E |- ls  
E = E1, c p , E2
-----------------------------
P; E; ls |- p : c

[FINAL VAR]

P; E |- ls  
E = E1, t x , E2
-----------------------------
P; E; ls |-_final x : t

[FINAL ADDRESS]

P |- E
E = E1, c p , E2
-----------------------------
P; E |-_final p : c 


[EXP SYNC]

P; E; ls |-_final e1 : c
P; E; ls U {e1} |- e2 : t
---------------------------------------------------
P; E; ls |- synchronized e1 e2  : t

e1 has to be final because otherwise, the following will typecheck.

synchronized(o) {
  o = new A<self>();
  o.f = 10;  <-- lock on o is not really held here
}

[EXP IN-SYNC]

P; E |-_final p : c
P; E; ls U {p} |- e : t
---------------------------------------------------
P; E; ls |- in-sync p e  : t


[EXP REF FINAL]

P; E; ls |- e : c
P; E; <\epsilon,c> |-_inst (final t fd = v)
----------------------------------------------
P;E;ls |- e.fd : t[e/this]


[EXP REF GUARD]

P; E; ls |- e : c
P; E; <\epsilon,c> |-_inst (t fd = v guarded_by l) 
P;E |- l[e/this] \in ls 
---------------------------------------------------------
P; E; ls |- e.fd : t[e/this]


[EXP ASSIGN GUARD]

P; E; ls |- e : c
P; E; <\epsilon,c> |-_inst (t fd = v guarded_by l) 
P;E |- l[e/this] \in ls 
P; E; ls |- e1 : t[e/this]
----------------------------------------
P; E; ls |- e.fd = e1 : t[e/this]

[EXP INVOKE]

There exists a substitution \theta such that
P; E; ls |- e_0 : c
P; E; <\theta,c> |-_inst (t mn(t_0 this,t_1 y_1,..,t_k y_k)
                                   requires ls')
for j = 0..k
 P;E;ls |- e_j: t_j
 P;E |- ls'[e_0/this][e_1/y_1][e_2/y_2]...[e_k/y_k] \in ls  
------------------------------------------------------------
P; E; ls |- e_0.mn(e_1,e_2,...,e_k) : t


In the 2nd hypothesis, \theta is chosen such that the 3rd
hypothesis (P;E;ls |- e_j : t_j) is true. \theta
instantiates the method owner parameters.
The return type (t) and argument types (t_i i=0..n) do not contain 'this' 


[EXP FORK]

P; E; ls |- e : cn<o_1,o_2,...,o_n> 
E'= cn<o_1,o_2,...,o_n> this
P;E';\emptyset |- this.run() : int
---------------------------------------------
P; E; ls |- e.fork : int


[EXP LET]

P;E;ls |- e_1 : t
E' = E, t x
P;E';ls |- e_2 : t_2
P;E |- t_2[e_1/x]
---------------------------------------------
P;E;ls |- (let t x = e_1 in e_2) : t_2[e_1/x]

[STATE] 

P |- \sigma : E  |T| > 0
P;E;\emptyset |- T_i : t_i forall i=1..|T|
-------------------------------------------
P |- <\sigma,T> : E 

This rule says that every expression in the thread sequence is well
typed and that the store \sigma and the environment E are compatible.

[STORE]

|- P
dom(\sigma) = {p_1,...,p_n}
\sigma(p_i) = {|..|}^{(i,j)}_{c_i} for i=1..n
E = c_1 p_1,...,c_n p_n
P;E;p_i |- \sigma(p_i) : c_i for i=1..n
---------------------------------------------
P |- \sigma : E

This rule checks the compatibility of the store and the environment
and verifies that the store is well formed.

[VAL OBJECT]

---------------------------------------
P;E;p |- {||}^{(i,j)}_{Object} : Object

[VAL SUBCLASS]

for i=1..m
 P;E;<\epsilon,c> |-_inst ([final]? t_i fn_i = v'_i [guarded_by l_i]?)
 P;E;\emptyset |- v_i : t_i[p/this] 
------------------------------------------------------------------
P;E;p |- \sigma(p) = {|fn_1 = v_1,...,fn_m = v_m|}^{(i,j)}_c : c

This rule ensures that the field mapping for each address in the store
is well formed, i.e. types of values and fields match.


Note that this rule differs from [VAL SUBCLASS] rule in [1]. We have
simplified this rule by using the |-_inst judgement.

[INIT OBJECT]

for i=1..m
 P;E;<\epsilon,c> |-_inst ([final]? t_i fn_i = v_i [guarded_by l_i]?)
--------------------------------------------------------------------
P;E;c |-_initial { fn_1 = v_1,..,fn_m v_m }

This rule is used to initialize the fields when a new object is created.
This rule also differs from the corresponding rule in [1].

END OF TYPING RULES
-----------------------------------------------------------------------

Semantics
----------

State space
-----------

S \in Store * ThreadSeq
\sigma \in Store : Address -> d
d = {|db|}^{m}_c
m \in { 0,1,....} \times { 0,1,....}
c : type of object
db : fn -> value   (maps each field of c to a value)

Evaluation starts in state <\emptyset, e> where P = defn* e
P |- <\emptyset, e> --->* <\sigma, v_1...n>

v_i is the final value computed by thread i

We adopt the same semantics as in [1] except for the following transitions.

1. [RED NEW] : We modify this rule to account for the change in [INIT
OBJECT] rule.

P |- <\sigma,T.E[new c].T'> --> <\sigma',T.E[p].T'>
where p \notin dom(\sigma),
dom(\sigma) = { p_1,..,p_n }
\sigma(p_i) = {|db_i|}^{..}_{c_i},
E = c_1 p_1,..,c_n p_n  
P;E;c |-_initial db
\sigma'=\sigma[p-->{|db|}^{(0,0)}_{c}]


2. [RED INVOKE] : We modify the [RED INVOKE] rule to also instantiate
method owner parameters.


P |- <\sigma,T.E[p.mn(v_1..n)].T'> --> 
     <\sigma,T.E[e[v_1/x_1,...,v_n/x_n,p/this]].T'>  
where     
dom(\sigma) = { p_1,..,p_n }
\sigma(p_i) = {|db_i|}^{..}_{c_i}
E = c_1 p_1,..,c_n p_n 
\sigma(p) = {|db|}^{(i,j)}_{c}
and there exists a substitution \theta such that
P;E;<\theta,c> |-_inst t mn(t_0 this,t_1 x_1,...,t_n x_n) requires ls {e}
P;E;\emptyset |- p : t_0
for i=1..n
  P;E;\emptyset |- v_i : t_i


\theta gives the substitution that instantiates the method owner
parameters.

3. [RED SYNC] and [RED IN-SYNC] : We modify these rules to support
nested lock acquires. The semantics in [1] do not support nested lock
acquires. 

The following program fragment never completes execution.

synchronized e1
  synchronized e1
      e2

This is due to the synchronized stmt progressing only when lock on e1
is not held. As a result, the second sync stmt gets stuck.

We change the semantics of synchronized and in-sync constructs to also
keep track of the thread that acquires the lock, and the nesting level
of the synchronized statement.
We use (0,0) to indicate that the lock not held, and 
(i,n) to indicate that thread i holds the lock and is at nesting level
n. Threads get numbered from 1 onwards; the main thread is the 1st
thread.    

E_k is the context for the kth thread.

if synchronized p e is the redux when lock p held, the nesting level is
increased by 1.

[RED SYNC]
                                                                
P |- <\sigma[p-->{|db|}^{i,j}_{c}], T.E_k[synchronized p e].T'> ----------> 

     <\sigma[p-->{|db|}^{k,j+1}_c], T.E_k[in-sync p e].T'> when i=0 or k
    
if in-sync p v is at the outermost nesting level, the lock on p is released.

[RED IN-SYNC]
                                                           
P |- <\sigma[p-->{|db|}^{k,1}_c],T.E_k[in-sync p v].T'> ----------->

     <\sigma[p-->{|db|}^{0,0}_c],T.E_k[v].T'> 


If in-sync p v is not the outermost nesting level, the nesting level
decreases by 1 but the lock on p is not released.

[RED IN-SYNC]
                                                          
P |- <\sigma[p-->{|db|}^{k,j}_c],T.E_k[in-sync p v].T'> ----------->

     <\sigma[p-->{|db|}^{k,j-1}_c],T.E_k[v].T'>  when j>1


END OF SEMANTICS
-------------------------------------------------------------------

Soundness Proof for restricted EPRFJ
------------------------------------

[1] describes a race free type system and also gives a soundness proof.
Our type system differs from the type system given in [1] as follows.  

We allow
1. "self" as an owner.
2. f$e as an owner. 
3. Parameterized Methods.


Parameterized methods increase the expressiveness of the language.
Consider the following program fragment that uses parameterized methods.

class A<f> {
 
  void print(B<g> b) {
    ....
  }
}

print(..) is a parameterized method that can be used to print an
instance of class B with any owner. In the absence of parameterized
methods, the class declaration would have to contain the formal owner
"g". This is not only tedious but also restricts the print(..) method
to printing objects with the same owner. 


Our type system does not allow special owner parameters
to appear in the type of fields. (Check rules [FIELD INIT] and [FIELD
FINAL INIT]). EPAJ [4] enforces this restriction to support
thread-local objects. Parameterized methods are necessary to ensure
that this restriction does not reduce the expressiveness of the
language. 

The following is a typical program that uses special owners in the
types of fields. We will show that using method owner parameters
this program can be re-written to eliminate the need for special
owners in field types.  

class A<f> {

B<self> b guarded_by f$this;

 int access() requires f$this {

  let B<self> b1 = this.b in 
     synchronized(b1) 
        b1.f = 10
 }
}

let A<self> a = new A<self>() in
  synchronized(a) a.access()
  let A<a> a1 = new A<a>() in
      synchronized(a) a1.access()


We handle fields with special owners by requiring methods to declare a
type for 'this' in their argument list. 
This explicit declaration of "this" takes precedence over the type in
the class declaration, so only method owner parameters (i.e., owner
parameters that appear in the types of the method's parameters)
may be used in the method body.
We allow the type for 'this' to contain special
owners and fresh formal owners. Instead of making an exception only
for the 'this' parameter, we choose to uniformly support fresh formal
owners in the types of all parameters.

The above example can be re-written as follows using method owner
parameters and removing the special owner from the field type.

class A<f,g> {

B<g> b guarded_by f$this;

 int access(A<h,self> this) requires h$this {

  let B<self> b1 = this.b in 
     synchronized(b1) 
        b1.f = 10
 }
}

let A<self,self> a = new A<self,self>() in
  synchronized(a) a.access()
  let A<a,self> a1 = new A<a,self> in
      synchronized(a) a1.access()

Note that, without the method owner parameter "h",
a and a1 could not have invoked the same method "access".
Thus, method owner parameters are necessary to support special owners
in types of fields. 

-----------------------

Proof Outline
-------------

We follow the proof structure in [1] closely, reusing many of the
lemmas and theorems. 


Lemma 1 : If there exists a deduction concluding P;E;ls |- e : t
then that deduction contains a subdeduction concluding 
P;E;ls : e : t' that does not end with an application of rule
[EXP SUB] for some type t' where P;E |- t' <: t

--------------

Lemma 2 (Context subexpression) : Suppose there is a deduction
concluding P;E;ls |- E[e] : t. Then, the deduction contains at
the position corresponding to the hole in E, a subdeduction 
P;E;ls' |- e : t' for some t' and ls' such that 
ls \subseteq ls' and E(e) is in the critical section of every
lock in ls' \ ls. 

-------------

Lemma 3 : Suppose there is a deduction
concluding P;E;ls |- E[e] : t. Then, the deduction contains at
the position corresponding to the hole in E, a subdeduction 
P;E;ls' |- e : t'for some t'and ls' such that 
ls \subseteq ls' and E(e) is in the critical section of every
lock in ls' \ ls. In addition, the subdeduction does not end with an
application of the [EXP SUB] rule.

-----------
Lemma 4 is the main lemma that guarantees that the transition rules
preserve the well typedness of expressions. Here e2 can be thought of
as the expression obtained when e1 is evaluated according to the
defined semantics. Lemma 4 guarantees that if e1 and e2 have the same
type, then the complete expression retains its well-typedness property
after a transition.

Lemma 4 (Context replacement) : Suppose a deduction concluding 
P;E;ls |- E[e1] : t contains a subdeduction concluding 
P;E;ls' |- e1 : t1  at a position corresponding to the hole in E.
If e1 is not a value and P;E;ls' |- e2 : t1 then 
P;E;ls |- E[e2] : t

----------

Lemma 5 handles the transition rule for "let" and "method invoke"
constructs. The transition rule for "let" is as follows.

P |- <\sigma,E[let t x = v in e]> --> <\sigma,E[e[v/x]]>

Lemma 5 guarantees that if P;E |- let t x = v in e : t'  then
P;E |- e[v/x] : t'. Now, Lemma 4 can be applied to deduce that
the "let" transition rule also preserves well typedness of expressions.

\theta[v/x] in part 6 represents composition of two substitutions and
is defined in the standard manner.
If f and g are substitutions  and Exp is an expression, then
Exp[f.g] = (Exp[f])[g]


Lemma 5 (Substitution) : If P;E;ls' |- v : s then
1. if P;E,s x,E' |- Z then P;E,E'[v/x] |- Z[v/x]
2. if P;E,s x,E';ls |- Z then P;E,E'[v/x];ls[v/x] |- Z[v/x]
3. if P;E,s x,E' |-_final Z then P;E,E'[v/x] |-_final Z[v/x]
4. if P;E,s x,E' |-_lock Z then P;E,E'[v/x] |-_lock Z[v/x]
5. if P;E,s x,E' |-_owner Z then P;E,E'[v/x] |-_owner Z[v/x]
6. if P;E,s x,E';<\theta,c> |-_inst Z then
   P;E,E'[v/x];<\theta[v/x],c[v/x]> |-_inst Z[v/x]

-------------

Lemma 6 is similar to Lemma 5 but deals with formal owner
substitutions. The transition rule for "method invoke" involves
variable substitution as well as formal owner substitution. As a
result, both Lemma 5 and Lemma 6 are required to argue about
preservation of well-typedness by [RED INVOKE] rule.

Lemma 6 (Formal owner substitution) :  If P;E |-_owner o 
1. if P;E,owner_formal f,E' |- Z then P;E,E'[o/f] |- Z[o/f]
2. if P;E,owner_formal f,E';ls |- Z then P;E,E'[o/f];ls[o/f] |- Z[o/f]
3. if P;E,owner_formal f,E' |-_final Z then P;E,E'[o/f] |-_final Z[o/f]
4. if P;E,owner_formal f,E' |-_lock Z then P;E,E'[o/f] |-_lock Z[o/f]
5. if P;E,owner_formal f,E' |-_owner Z then P;E,E'[o/f] |-_owner Z[o/f]
6. if P;E,owner_formal f,E';<\theta,c> |-_inst Z then
   P;E,E'[o/f];<\theta[o/f],c[o/f]> |-_inst Z[o/f]

Lemma 6 given above differs from Lemma 6 in [1]. It is the main lemma
that must be proved to show that "self" and "f$e" constructs are used
in the semantically correct manner.

Lemma 6 can be proved by a simultaneous induction on the 
6 statements.

I will prove the lemma for statement 4 and statement 6.

Let RTP stand for Required to Prove (!!)

Proof for statement 4 :
-----------------------

RTP : if P;E |-_owner o and P;E,owner_formal f,E' |-_lock z then
P;E,E'[o/f] |-_lock z[o/f]

Let I(n) : The statements 1,2, 3, 4, 5 and 6 are true for all
judgements for which there exists a derivation tree of height <=n
(where n is an integer). 

Assume I(n) is true for some n>1. 
Let D = P;E,owner_formal f,E' |-_lock z
and suppose the shortest derivation tree of D has height n+1.

 Then, the last rule to be applied in this shortest derivation
 sequence is 
 
 (a) [LOCK_FINAL]
     Then z is a final expression. 
     Thus, P;E,owner_formal f,E' |-_final z : t (for some t) has a
     derivation tree of 
     height n. By induction, P;E,E'[o/f] |-_final z[o/f] : t[o/f]. Thus,
     P;E,E'[o/f] |-_lock z[o/f] 

 (c) By applying [LOCK_FORMAL] rule.
     Then, z is of the form f$e. Thus, we have 
     P;E,owner_formal f,E' |-_owner_formal f 
     P;E,owner_formal f,E' |-_final e : cn<f_1..n>
     f \in { f_1..n } 

    Three cases must be considered based on what o is. 

 (c1) o=self
 By induction, 
 P;E,E'[self/f] |-_final e[self/f] : cn<f_1..n>[self/f]
 Since f$e[self/f] = e[self/f], from the above judgement, and applying
 [LOCK FINAL], we have
 P;E,E'[self/f] |-_lock e[self/f].  Thus, we have
 P;E,E'[o/f] |-_lock e[o/f]. (since o=self)
 

 (c2) o is a formal owner. P;E |-_owner_formal o
  By induction,
  P;E,E'[o/f] |- owner_formal o
  P;E,E'[o/f] |-_final e[o/f] : cn<f_1..n>[o/f] 
  f \in { f_1..n } => o \in { f_1..n } [o/f] 

  Thus, [LOCK FORMAL] can be applied to get 
  P;E.E'[o/f] |-_lock o$e[o/f]   

  But since z[o/f] = (f$e)[o/f] = o$e[o/f] (follows from the substitution
  rule defined for f$e), we have proved
  P;E.E'[o/f] |-_lock z[o/f]   

 (c3) o is a lock. P;E |-_lock o
 Thus, z[o/f] = o  (follows from substitution rule defined for f$e)     
 Thus, P,E |-_lock z[o/f]. 
 We can extend the environment to get P;E,E'[o/f] |-_lock z[o/f]


Proof of statement 6:
----------------------
Given : P;E |-_owner o and P;E,owner_formal f,E';<\theta,c> |-_inst Z 
RTP: P;E,E'[o/f],<\theta[o/f],c[o/f]> |-_inst Z[o/f] 

Let I(n) be as described above.
Assume I(n) is true for some n>1
Let D = P;E,owner_formal f,E',<\theta,c> |-_inst Z
Suppose the shortest derivation tree for D has height n+1.

Case 1:
Z = field  

From D and [FIELD INSTANTIATE] rule, we must have
P;E,owner_formal f, E' |- \theta (1)
P;E,owner_formal f,E' |- c <: cn<o_1..n>  (2)
class cn<f_1..n> .... { ... field' ... } \in P (3)
\theta' = [o_1/f_1,..,o_n/f_n]  (4)
field'[\theta'] = field  (5)

Using induction and applying Lemma 6 to (1) and (2), we have
P;E,E'[o/f] |- \theta[o/f]  (6)
P;E,E'[o/f] |- c[o/f] <: cn<o_1..n>[o/f] (7)
\theta'' = [o_1/f_1,..,o_n/f_n][o/f] (8)
Then, field'[\theta''] = field[o/f] (9)

From (6), (7), (3), (8) and (9) and applying the [FIELD INSTANTIATE] rule,
we can deduce P;E,E'[o/f];<\theta[o/f],c[o/f]> |-_inst field[o/f]

(proved)

Case 2:
Suppose Z = meth

From D and [METHOD INSTANTIATE] rule, we must have

P;E,owner_formal f,E' |- \theta (1)
P;E,owner_formal f,E' |- meth' \in c (2)
MethodOwnerParams(meth') \subseteq dom(\theta) (3)
meth'[\theta] = meth (4)

From (2) and [METHOD DECL/INHER] we have

P;E,owner_formal f,E' |- c <: cn<o_1..n> (5)
class cn<f_1..n> extends c' { .... meth' .... } \in P (6)

Using induction and replacing [o/f] in (1) and (5) we get
P;E,E'[o/f] |- \theta[o/f]  (7)
P;E,E'[o/f] |- c[o/f] <: cn<o_1..n>[o/f]  (8)

From (6), (8) and applying [METHOD DECL/INHER] we have
P;E,E'[o/f] |- meth' \in c[o/f] (9)

Also dom(\theta[o/f]) = dom(\theta)  if f \in dom(\theta)
                      = dom(\theta) U { f } if f \notin dom(\theta)

Therefore dom(\theta) \subseteq dom(\theta[o/f]) and from (3) we have
MethodOwnerParams(meth') \subseteq dom(\theta[o/f]) (10)

From (4) we have meth'[\theta][o/f] = meth[o/f] (11)

From (7), (9), (10) and (11) and applying [METHOD INSTANTIATE] rule,
we get P;E,E'[o/f];<\theta[o/f],c[o/f] |-_inst meth[o/f]

(proved)


Lemma 7 (Environment strengthening) : If E = E', owner_formal f, E''
and P |- E then
1. If P;E',E'' |- Z then P;E |- Z
2. If P;E',E'';ls |- Z then P;E;ls |- Z
3. If P;E',E'' |-_final Z then P;E |-_final Z


Lemma 8 (Class Instantiation) : If |- P and P;E;ls |- p : c then 
P;E |- c

This lemma ensures that all class instantiations are correct.

Lemma 9 (Field and Method instantiation): If |- P and P;E;ls|-p : c 
1. if P;E;<\theta,c> |-_inst field then P;E |- field[p/this]
2. if P;E;<\theta,c> |-_inst meth then P;E |- meth

This lemma guarantees that fields and methods are instantiated
correctly. This lemma is different from Lemma 9 in [1]. This
difference is due to our support for method owner parameters. note
that in part 2, we prove P;E |- meth  instead of P;E |- meth[p/this]
as in [1]. This is because we consider 'this' to be a parameter of
the method and deal with it similarly to the other parameters.

Proof of 1.

if P;E;<\theta,c> |-_inst field then from [FIELD INSTANTIATE] rule
we have

P;E |- c <: cn<o_1..n>
class cn<f_1..n> extends c' { .... field' .... } \in P
\theta=[o_1/f_1,...o_n/f_n]
field=field'[\theta]


Since we have assumed |- P, from the [CLASS] rule we get
P;owner_formal f_1,..,owner_formal f_n,cn<f_1..n> this |- field' -- (3)
Applying Lemma 6 and Lemma 7 and replacing formal owners f_i with o_i, we have
P;E,cn<o_1..n> this |- field'[o_1/f_1,..,o_n/f_n]
Applying Lemma 5 and replacing 'this' with p, we have
P;E |- field'[o_1/f_1,..,o_n/f_n,p/this]

Thus, we have P;E |- field[p/this]
(proved)

Proof of 2
----------

Suppose P;E;<\theta,c> |-_inst meth. From [METHOD INSTANTIATE] we have

dom(\theta)=MethodOwnerParams(meth') (1)
P;E |- meth' \in c  (2)
P;E |- \theta (3)
meth=meth'[\theta] (4)

To derive (2) we must apply [METHOD DECL/INHER] rule, whose hypotheses
are

P;E |- c <: cn<o_1..n>
class cn<f_1..n> extends c' { .... meth' .... } \in P

Let meth' = t mn(arg_0..n) requires e_1..m { e }

Since |- P, [CLASS] rule requires  P;\emptyset |- meth' which must be derived
from [METHOD] rule. Thus, we must have

E' =  {owner_formal f | f appears in some arg_i}
E'' = E', arg_0, arg_1, ... arg_n
P; E' |- t   (5)
P; E'' |- { e_1...m }   (6)
P; E''; e_1,e_2,...,e_m |- e : t  (7)

Note that MethodOwnerParams(meth') = { f | f appears in some arg_i }
Therefore, from (1) we have dom(\theta) = {f | f appears in some arg_i } 
Also, since P;E |- \theta (3 above), for all x \in dom(\theta)
P;E |-_owner \theta(x) . Thus, applying Lemma 6 to 5,6 and 7
above we have,

P;E |- t[\theta]
P;E,arg_0[\theta],..,arg_n[\theta] |- { e_1...m }[\theta]
P; E,arg_0[\theta],..,arg_n[\theta];e_1[\theta],..,e_m[\theta] |-
					  e[\theta] : t[\theta]

From the above three, applying the [METHOD] rule, we can deduce

P;E |- t[\theta] mn(arg_0[\theta],..,arg_n[\theta])
       requires { e_1..m }[\theta] { e[\theta] }

Thus, P;E |- meth'[\theta]  i.e. P;E |- meth

(Part 2 proved)

----------------------------------

Lemma 10 (Inferred to exact types) : If P |- \sigma : E and 
P;E;ls |- p : c, then P;E;\emptyset |- p : c and there
exists c' such 
that P;E |- c'<:c  and E(p) = c' and \sigma(p) = {|db|}^{i,j}_{c'}.

Lemma 10 has P |- \sigma : E as hypothesis whereas Lemma 10 in [1] has 
P |- <\sigma,T> : E as hypothesis.

The proof follows the one given in [1].

-----------------

Lemma 11 (Object fields well-typed) : Suppose P |- \sigma : E and 
\sigma(p) = {|....fn = v....|}^{i,j}_{c}. If 
P;E;<\epsilon,c> |-_inst ([final]? t fn = v' [guarded_by l]?) 
then P;E;\emptyset |- v : t[p/this] 

This lemma guarantees that a value assigned to a field has the same
type as the field. This lemma is necessary to show that transitions
involving field accesses preserve well-typedness, i.e. if p.fn = v
then P |- E[p.fn] ---> E[v] and since the types of p.fn and v are the
same by lemma 11, lemma 4 ensures that E[v] is also a well typed expression.

Proof : Since P |- \sigma : E, we must have
dom(\sigma) = {p_1..n }
E = c_1 p_1,..,c_n p_n
\sigma(p_i) = {|db|}^{r,s)_{c_i} for i=1..n
P;E;p_i |- \sigma(p_i) : c_i  for i=1..n

Thus, it follows that P;E;p |- \sigma(p) : c  (p = p_k for some k \in 1..n)
From the [VAL SUBCLASS] rule we have

P;E;<\epsilon,c> |-_inst ([final]? t' fn = v' [guarded_by l']?) (1)
P;E;\emptyset |- v : t'[p/this]  (2)

Since we also have P;E;<\epsilon,c> |-_inst (([final]? t fn = v' [guarded_by l]?)
using (1) we have t=t'.

Thus, from (2) we have P;E;\emptyset |- v : t[p/this]

(proved)

--------------------

Lemma 12 (Lockset strengthening) : If P;E;ls |- v : t and 
P;E |- ls \subseteq ls', then P;E;ls' |- v : t

Proof: From [1]

By lemma 1, there exists a subdeduction not ending in [EXP SUB] such
that P;E;ls |- v : s  and P;E |- s <: t 
The only rules which can be used to derive P;E;ls |- v : s are
[EXP VAR] and [EXP ADDRESS].
Both these rules have the hypotheses
P;E |- ls
E = E_1, s v, E_2

Since P;E |- ls \subseteq ls' we have P;E |- ls'
Thus, applying [EXP VAR] or [EXP ADDRESS] with lockset ls',
we get P;E;ls' |- v : s
Now, from [EXP SUB], we can derive P;E;ls' |- v : t

(proved)
------------------------------

Lemma 13 (Type subject reduction) : If P |- S : E and S --> S', then
P |- S' : E' for some E'.

The first reduction lemma is same as Lemma 13 in [1].
This is the central lemma in the soundness proof. It says that the
transition semantics and the type system guarantee that transitions
from a well formed state always lead to well formed states.

Proof

Let S = <\sigma,e_1,..,e_k,...e_n> and let the kth thread be reduced.
Let S'=<\sigma',e_1,..,e'_k,..,e_n>.
We deal with the [RED FORK] transition separately.

Given P |- S : E and P;E |- E[e_k] : t.
RTP : P |- S' : E' and P;E' |- E[e'_k] : t

1. [RED NEW]

<\sigma, E[new c]> --> <\sigma',E[p]>  where
p \notin dom(\sigma)
\sigma' = \sigma[p -> {|db|}^{(0,0)}_{c}
E' = E, c p and P;E';c |-_initial db

RTP : (1) P |- \sigma' : E'
      (2) P;E';\emptyset |- E[p] : t

Proof of (1)

Let dom(\sigma) = { p_1,..,p_{n-1} } and let p_n=p, c_n=c
Then, dom(\sigma') = { p_1,..,p_n }
\sigma'(p_i) = \sigma(p_i) for i=1..n-1

Since P |- \sigma : E  and E'=E, c_n p_n
for i=1..n-1,
  E'(p_i) = c_i
  P;E';p_i |- \sigma'(p_i) : c_i

Thus, to prove P |- \sigma' : E' we have to prove
E'(p_n) = c_n  (follows from definition of E')
and P;E';p_n |- \sigma'(p_n) : c_n (3)

Let \sigma'(p_n) = {|fn_1 = v_1,..,fn_m = v_m|}^{(0,0)}_{c_n}

Since P;E';c |-_initial {|fn_1 = v_1,..,fn_m = v_m|}^{(0,0)}_{c_n} : c_n
it follows that
for i=1..m
  P;E';<\epsilon,c_n> |-_inst ([final]? t_i fn_i = v_i [guarded_by l_i]?)

Since |- P (from [STORE]) and P;E;\emptyset p_n : c_n
applying Lemma 9 (field instantiation) it follows that
for i=1..m
 P;E' |- ([final]? t_i[p/this] = v_i[p/this] [guarded_by l_i[p/this]]?)

Also, v_i[p/this] = v_i (v_i is an address since E' contains only addresses)

Thus, using [FINAL FIELD INIT] or [FIELD INIT] we have
for i=1..m P;E |- v_i : t_i[p/this] 

Thus, we have
\sigma'(p_n) = {|fn_1 = v_1,..,fn_m = v_m|}^{(0,0)}_{c_n}
for i=1..m
  P;E';<\epsilon,c> |-_inst ([final]? t_i fn_i = v_i [guarded_by l_i]?)
  P;E' |- v_i : t_i[p/this] 

Applying [VAL SUBCLASS] rule, we get P;E';p_n |- \sigma(p_n) : c_n 
Thus, we have proved (3) and hence Part 1.

(proved)

Part 2 : Given P;E;\emptyset |- E[new c] : t. Prove P;E';\emptyset |- E[p] : t

Proof of Part 2
---------------
Extend E to E'. P;E';\emptyset |- E[new c] : t
From Lemma 3 , we have a subdeduction P;E';ls |- new c : c
(for some lockset ls) 
This judgement can be derived from [EXP NEW]
which only requires P;E' |- ls and P;E' |- c

Choosing ls = \emptyset, we have P;E';\emptyset |- new c : c
From [EXP ADDRESS] we have P;E';\emptyset |- p : c

Thus, applying Lemma 4, we get P;E';\emptyset |- E[p] : t

(proved)

2. [RED READ]
S=<\sigma,E[p.fn]>  S'=<\sigma,E[v]> where
\sigma(p) = {|.... fn = v .....|}^{(i,j)}_{c}

Let P |- \sigma : E  and P;E;\emptyset |- E[p.fn] : t
RTP : P;E;\emptyset |- E[v] : t

Proof :
There is a subdeduction P;E;ls |- p.fn : s (1)
We can use either [EXP REF GUARD] or [EXP REF FINAL] to derive it.
Suppose [EXP REF GUARD] is used.
Then P;E;ls |- p : c
P;E;<\epsilon,c> |-_inst (s' fn = v' guarded_by l) 
s=s'[p/this]

Applying Lemma 11, we have P;E;\emptyset |- v : s and applying Lemma
12, P;E;ls |- v : s (2)
From (1) and (2), applying Lemma 4, we have P;E;\emptyset |- E[v] : t
(proved)

3. [RED ASSIGN]
S=<\sigma,E[p.fn = v]>   S'=<\sigma',E[v]> where
\sigma'=\sigma[p.fn --> v]

Let P |- \sigma : E  and P;E;\emptyset |- E[p.fn = v] : t
RTP : (1) P |- \sigma' : E
      (2 P;E;\emptyset |- E[v] : t

Proof of 1
----------
We know that dom(\sigma') = dom(\sigma)
Let \sigma'(p) = {| .... fn = v .....| }^{(i,j)}_{c}

From Lemma 3, there exists a subdeduction P;E;\emptyset |- p.fn = v : s
This judgement can only be derived from [EXP ASSIGN] rule, which requires 

P;E;ls |- p : c
P;E;<\emptyset,c> |- (s' fn guarded_by l')
s=s'[p/this]
P;E;ls |- v : s

Using the above judgements and P |- \sigma : E, and the [VAL SUBCLASS]
rule, we can deduce P |- \sigma' : E

(proved)

Proof of Part 2
---------------

The proof for this is similar to the proof of [RED READ].

4. [RED LET]

   S = <\sigma,E[let x=v in e]> . S'=<\sigma,E[e[v/x]]>

Given P |- S : E and P;E;\emptyset |- E[let x=v in e] : t
RTP : P;E;\emptyset |- E[e[v/x]] : t

Proof : There exists a subdeduction P;E;ls |- let x=v in e : s (1)
Note that
[EXP LET] rule gives us
P;E;ls |- v : t' 
P;E,t' x;ls |- e : s' (2)
P;E |- s'[v/x]
s=s'[v/x]

Also, P;E |- ls and P |- E,t' x  implies that ls does not contain x

Substituion [v/x] in (2) and applying Lemma 5, we have
P;E;ls |- e[v/x] : s'[v/x]

Thus, we have P;E;ls |- e[v/x] : s. Using this and (1) and applying
Lemma 4, we have P;E;\emptyset |- E[e[v/x]] : t

(proved)

5. [RED SYNC]

S=<\sigma,E[synchronized p e]>  S'=<\sigma',E[in-sync p e]>
Given P |- \sigma : E and P;E;\emptyset |- E[synchronized p e] : t
RTP : P |- \sigma' : E and P;E;\emptyset |- E[in-sync p e] : t

\sigma' differs from \sigma at p.
If \sigma(p) = {|db|}^{(0,0)}_{c} then \sigma'(p) = {|db|}^{(k,1)}_{c}
(thread k acquires lock on p)
If \sigma(p) = {|db|}^{(k,i)}_{c} then \sigma'(p) = {|db|}^{(k,i+1)}_{c}
(thread k already holds the lock on p)

In both cases, P |- \sigma' : E follows from P |- \sigma : E

Proof : There is a subdeduction P;E;ls |- sunchronized p e : s
This is derived using the [EXP SYNC] rule.
Thus, we have
P;E;ls |-_final p : c
P;E;ls U { p } |- e : s

From these two, using the [EXP IN-SYNC] rule, we can deduce
P;E;ls |- in-sync p e : s

Thus, using lemma 4, we have P;E;\emptyset |- E[in-sync p e] : t

(proved)

6. [RED IN-SYNC]

Proof similar to [RED SYNC] above.

7. [RED FORK]

S=<\sigma,T.E[p.fork].T'>  S'=<\sigma,T.E[0].T'.(p.run())>

Given P |- S : E and P;E;\emptyset |- E[p.fork] : t
RTP : (1) P;E;\emptyset |- E[0] : t  
      (2) P;E;\emptyset |- p.run() : t'


Proof :

There exists a subdeduction P;E;ls |- p.fork : int
This can only be derived from the [EXP FORK] rule.
Thus, we have

P;E;ls |- p : c (1)
E' = c x
P;E';\emptyset |- x.run() : int (2)

Note that we can choose ls = \emptyset
Thus, we have P;E;\emptyset |- p.fork : int
Using P;E;\emptyset |- 0 : int and Lemma 4 we have
P;E;\emptyset : E[0] : t

(Part 1 proved)

Extending the environment in (2) to E and choosing x such that P |- E, c x,
we have P;E,c x;\emptyset |- x.run() : int

Using (1) and Lemma 5, replace x with p to get
P;E;\emptyset |- p.run() : int

(Part 2 proved)

8. [RED INVOKE]

S=<\sigma,E[p.mn(v_1..n)]>  S'=<\sigma,E[e[x_1/v_1,..,x_n,v_n,p/this]]>
where
dom(\sigma) = { p_1,..,p_n }
\sigma(p_i) = {|db_i|}^{..}_{c_i}
E = c_1 p_1,..,c_n p_n  
\sigma(p) = {|db|}^{(i,j)}_{c}
\theta is a substitution such that
P;E;<\theta,c> |-_inst
	t mn(t_0 this,t_1 x_1,...,t_n x_n) requires ls { e } (1) 
for i=1..n
  P;E;\emptyset |- v_i : t_i  (2)
  P;E;\emptyset |- p : t_0   (3)

Given P |- \sigma : E  and P;E;\emptyset |- E[p.mn(v_1..n)] : s
RTP : P;E;\emptyset |- E[e[v_1/x_1,../,v_n/x_n,p/this]] : s

Proof :

From the hypothesis and Lemma 3, there exists a subdeduction
P;E;ls' |- p.mn(v_1..n) : t' (4) 

[EXP INVOKE] rule, gives us

There exists \theta' such that
P; E; ls' |- p : c  
P; E; <\theta',c> |-_inst (t' mn(t'_0 this,t'_1 x_1,..,t'_k x_k)
                              requires ls'' { e' }
for i = 1..n
 P;E;ls' |- v_i: t'_i
P;E;ls |- p : t'_0 
P;E |- ls''[v_1/x_1,..,v_n/x_n,p/this] \subseteq ls'  (5)

From  (1), (2), and (3) we can take \theta'=\theta, t'=t, t'_i = t_i
and ls''=ls in the above judgements.

Using (1) and Lemma 9 (method instantiation) we get
P;E |- t mn(t_0 this,t_1 x_1,..,t_n x_n) requires ls { e }

Using the [METHOD] rule, we get
E'=E
E''=E,t_0 this,..,t_n x_n
P;E |- t
P;E'' |- ls  (6)
P;E'';ls |- e : t (7)

Using (2), (3) and applying Lemma 5 to (6) and (7),
we have
P;E |- ls[v_1/x_1,..,v_n/x_n,p/this]
P;E;ls[v_1/x_1,..,v_n/x_n,p/this] |-
	e[v_1/x_1,..,v_n/x_n,p/this] : t[v_1/x_1,..,v_n/x_n,p/this]

Note that t cannot contain x_1..n or 'this'. Therefore,
t[v_1/x_1,..,v_n/x_n,p/this]=t
Thus, P;E;ls[v_1/x_1,..,v_n/x_n,p/this] |- e[v_1/x_1,..,v_n/x_n,p/this] : t (8)
			
Using (5) and the result ls''=ls, we have
P;E |- ls[v_1/x_1,..,v_n/x_n,p/this] \subseteq ls'
Extending the lockset in (8), we have
P;E;ls' |- e[v_1/x_1,..,v_n/x_n,p/this] : t (9)

Using (9), (4), t'=t and applying Lemma 4 to the hypothesis, we get
P;E;\emptyset |- E[e[v_1/x_1,..,v_n/x_n,p/this]] : s

(proved)

---------------------------------------------------------

Lemma 14 and Lemma 15 of [1] show that two threads cannot hold the same lock
simultaneously. These lemmas are adopted as is.

Lemma 14 : If e is in the critical section of p and ls |-_{cs} e, then 
p \in ls.

Lemma 15 (Mutual exclusion subject reduction) : If P |- S : E and
|-_{cs} S and P |- S ---> S', then |-_{cs} S'.


Lemma 16 differs from Lemma 16 in [1] in that it does not include P |- S:E 
in the hypothesis. 

Lemma 16 (Field Access) Suppose P;E;\emptyset |- e : t
and e accesses p.fn. Then P;E |- p : c and

1. P;E;<\epsilon,c> |-_inst (s fn = v guarded_by l) and e is in the
critical section of l[p/this].
OR
2.P;E;<\epsilon,c> |- (s final fn = v)

Lemma 16 guarantees that whenever any thread access a guarded field, it has
to first acquire the lock guarding the field.

Proof : 

Let e = E[p.fn] 
Since P;E;\emptyset |- E[p.fn] : t, by lemma 3, there exists a
subdeduction concluding P;E;ls |- p.fn : s 
We can reach this conclusion via either [EXP REF GUARD] or [EXP REF FINAL]

a. [EXP REF GUARD]

  Since P;E |- p : c, it follows that 

P;E;<\epsilon,c> |- (s' fn = v guarded_by l) 
s = s'[p/this]
P;E |- l[p/this] \in ls

Thus, from lemma 3 it follows that
E[p.fn] is in the critical section of l[p/this] 

b. [EXP REF FINAL]
Since P;E |- p : c, it follows that
P;E;<\epsilon,c> |- (final s' fn)
s=s'[p/this] 

(proved)

----------

Theorem 17 (No conflicting accesses) Suppose P |- S : E and |-_cs S.
Then S does not have any conflicting accesses.

Theorem 17 says that no two threads can access the same guarded field
concurrently.

Proof :  From [1]. 

Let S = <\sigma,T>.  Since P |- S : E, we have 
P;E;\emptyset |- t_i  for i=1..|T|
If t_i accesses p.fn, from lemma 16 we have 

a. either p.fn is a final field, in which case it cannot have a
conflicting access.
b. t_i is in the critical section of the lock guarding p.fn (say l). 
  Since |-_cs S, for all j!=i, t_j is not in the critical section of l
and hence t_j cannot access p.fn. Thus there is no conflicting access
on p.fn

(proved)

Theorem 18 (Race Freedom) If |- P, then P does not have a race condition. 

Proof: From [1].

Since |- P, we have P;\emptyset;\emptyset |- e : t 
We start in the state <\emptyset,e> .
P |- <\emptyset,e> : \emptyset  follows from [STATE]
|-_cs <\emptyset,e> also holds. 
Thus, if <\emptyset,e> --->* S then by lemmas 16 and 17 P |- S : E for
some E and |_cs S. Thus, lemma 17 ensures that S does not have any
conflicting accesses. Since every state S reachable from the initial
state does not have conflicting accesses, P is race-free.

(proved)

------------------------------------------------------------------

References

 [1] Martin Abadi and Cormac Flanagan and Stephen Freund. Types for
 Safe Locking: Static Race Detection for Java. ACM Transactions on
 Programming Languages and Systems.to appear.
 
 [2] C. Flanagan and S. Qadeer. A type and effect system
 for atomicity. In Proc. ACM SIGPLAN Conference on
 Programming Language Design and Implementation
 (PLDI), pages 338{349. ACM Press, 2003.
 
 [3] C. Flanagan and S. Freund. Type-based race detection
 for Java. In Proc. ACM SIGPLAN Conference on
 Programming Language Design and Implementation
 (PLDI), pages 219{232. ACM Press, 2000.

 [4] Amit Sasturkar, Rahul Agarwal, Liqiang Wang and Scott D. Stoller.
     Automated Type-Based Analysis of Data Races and Atomicity.
     Computer Science Department, SUNY at Stony Brook.
     Technical Report DAR-04-18.
     Available at http://www.cs.sunysb.edu/~amits/papers/atomicity-inference/