CSE647: Robust (Distributed) Software (Spring 2002)
                              Scott Stoller
                               Homework 4
Due: 4 Apr

This homework is based on: Cormac Flanagan and Stephen Freund.
Type-based race detection for Java.  In Proc. SIGPLAN Conference on
Programming Language Design and Implementation (PLDI).  ACM Press, 2000.

Consider the initial type system extended with thread-local (hereafter
called "unshared") classes but not with external locks; in other words,
consider the rules in Appendices A and C, but ignore the fragments
related to ghost variables in Appendix C.

1. Extend the type system so that it can type-check programs in which
some instances of a class are unshared and some are shared.  The types
keep track of which instances are shared, and which are unshared.  Your
type system should allow some pieces of code to handle both shared and
unshared instances (without losing the distinction); this requires
polymorphism.  For example, the program below is not typable in
Flanagan and Freund's type system and should be typable in yours.

The basic idea is to replace the type C with two types: C<shared> and
C<unshared>.  The close relationship between these two types is expressed
as polymorphism.  C<a>, where a is a type variable ranging over {shared,
unshared}, is also a valid type.  Note that all types (except int) now
have the form C<x> where x is "shared", "unshared", or a type variable.
Please give

(1) changes to the syntax of the language

(2) new typing rules for [SUBTYPE CLASS], [EXP REF], [EXP INVOKE], and
[P;E |- method].  (Some of the other rules change, too, but you don't
need to write them down unless you want to.)

(3) new versions of the restrictions in Section 5; note that, for safety,
expressions with polymorphic types (i.e., types containing type
variables) can be used only in ways that expressions with unshared types
can be used.

(4) types for the program below in your type system.

You'll need new rules that allow instantiation of type variables, e.g.,

               P; E; ls |- e : c
  ---------------------------------------------
  P; E[sigma]; ls[sigma] |- e[sigma] : c[sigma]

where sigma is a substitution that instantiates some type variables,
i.e., replaces them with "shared" or "unshared".  You don't need to
explicitly give this rule or analogous rules for other judgments.


class Collect {
  int total;
  // add for unshared data
  int add(Data d) { synchronized (this) { total=total+d.get(); } }
  // add for shared data.  the only difference is that addsh requires d
  int addsh(Data d) { synchronized (this) { total=total+d.get(); } }
}

class Data {
  int d;
  init(int i) { d=i; }
  int get() { return d; }
}

class Main {
  int main() {
    // create a shared Collect
    Collect c = new Collect;
    // create unshared data
    Data ud = new Data;
    du.init(1);
    // create shared data
    Data sd = new Data;
    sd.init(2);
    c.add(ud);
    fork(synchronized (sd) { c.addsh(sd) });
    return c.total;
  }
}