CSE526: Principles of Programming Languages
			      Scott Stoller
		       atomicity types: example
			version: 3pm,25mar2004

let's type-check the program

P = CLASSI CLASSC MAIN

where the abbreviations are

CLASSI = 
  class I extends Object {
    int f guarded_by this = 0;
  }

CLASSC = 
  class C extends Object {
    atomic int m(I i) { sync i i.f }   // "sync" abbreviates "synchronized"
  }

MAIN = 
  let C c = new C in 
  let I i = new I in 
  c.m(i)

I will only show the type-checking of class C.
Type-checking of class C ends with a use of the 
[CLASS] rule to show that class C is well-typed.  
As an exercise, you could similarly show that 
class I and expression MAIN are well-typed, 
and then use the [PROG] rule to show
that the entire program P is well-typed.

I will present the proof bottom-up.  the main steps are:

1. check "i" using rule [VAR]
2. check "i.f" using rule [EXP REF GUARD]
3. check "sync i i.f" using rule [EXP SYNC] and then rule [EXP SUB]
4. check method m using rule [METHOD]
5. check class C using rule [CLASS]

details appear below.

========================================================================
1. check "i" using rule [EXP VAR]

Notes: 

a. the judgment P |- E just says that E is a well-formed
type environment for program P, for example, that the classes used in E
are declared in P.  proofs of such judgments are omitted.

b. as we will see, the [CLASS] rule is responsible for adding "C this"
to the type environment, and the [METHOD] rule is responsible for
adding "I i" to the type environment.

E = C this, I i
P |- E
---------------------
P; E |- i : I & const

========================================================================
2. check "i.f" using rule [EXP REF GUARD]

Notes:

a. note how the substitution is used to replace "this" (in the
guarded_by clause) with the variable "i" that refers to the object
actually being accessed.

b. the last premise just says that i?mover is a well-formed atomicity.
the proof of this premise is omitted.

E = C this, I i
P; E |- i : I & const
P; E |- int f guarded_by this = 0 \in I
b \equiv this[this:=i]?mover          // thus, b \equiv i?mover
P; E |- i?mover
----------------------------------------
P; E |- i.f : int & const;(i?mover)

using the equations on page 342, we can show that const;(i?mover) is
equivalent to i?mover.  so, the conclusion becomes 

P; E |- i.f : int & i?mover

========================================================================
3. check "sync i i.f" using rule [EXP SYNC] and then rule [EXP SUB]

E = C this, I i
P; E |- i : I & const
P; E |- i.f : int & i?mover
----------------------------------------
P; E |- sync i i.f : int & S(i,i?mover)

recall that i?mover abbreviates i?mover:error.
we compute S(i,i?mover:error) using its definition on page 343.

S(i,i?mover:error) = S(i,mover)
                   = i?mover:atomic

so, the conclusion becomes

P; E |- sync i i.f : int & i?mover:atomic

the type system does not allow parameters like i to be
used in the atomicity in a method declaration (although 
I don't immediately see a problem with allowing it), so 
we use rule [EXP SUB] to replace "i?mover:atomic" with the 
weaker atomicity "atomic".

the premise "P; E |- int <: int" follows from [SUBTYPE REFL].
the last premise follows from the rules on page 343 that define 
\squareLessThanOrEqual.

E = C this, I i
P; E |- sync i i.f : int & i?mover:atomic
P; E |- int <: int
i?mover:atomic \squareLessThanOrEqual atomic
--------------------------------------------
P; E |- sync i i.f : int & atomic

========================================================================
4. check method m using rule [METHOD]

the premise "P; C this, I i |- atomic" follows from [ATOM BASE]
the premise "P |- int" follows from [TYPE INT]
the conclusion says that method m is well-typed.

P; C this |- atomic   
P |- int
P; C this, I i |- sync i i.f : int & atomic
-------------------------------------------
P; C this |- atomic int m(I i) { sync i i.f }

========================================================================
5. check class C using rule [CLASS]

the conclusion says that class C is well-typed.

E = C this
P |- Object
P; C this |- atomic int m(I i) { sync i i.f }
---------------------------------------------
P |- CLASSC