Limited But Tractable Type Inference Against Races

this report, I describe a limited form of that type system, and its polynomial-time algorithm. Two unproven conjectures are curently required in the proof of correctness of the algorithm. 2 The Language and Type System The language used is shown in Figure 1 and is derivative of RFJ2 used by Flanagan and Freund.[3] Each class definition is parameterized by a single ghost variable, which can occur in any of the annotations within the class body. In addition to the limitation to a single class paramater, note the removal of method ghost parameters. The first is key to finding a tractable sub-problem, and the second probably just a technical detail, to be worked out in full in the future. Type checking of RFJ2-1 proceeds according to the rules in Figure 3, and a set of constraints upon the lock set variables in the program is accumulated. For an annotated program, these constraints must simply hold; for an unannotated program they will drive the type inference process. These constraints, and a couple of other constructs that do not appear in source programs but are necessary for type-checking, are defined in Figure 2. Important to note is that # #, where # ranges over any lock set variable, is not evaluated while type-checking, but only explicitly, in the context of some assignment to all the lock set variables. The notation for immediately applying a substitution to some set s is #(s). P ::= defn # e (program) defn ::= class cn#ghost g# field # method # (class declaration) field ::= t fn guarded by # (field declaration) method ::= t mn(arg # ) requires s (method declaration) arg ::= t x (argument declaration) c, t ::= cn### (type) s ::= x x (lock set) e ::= x null new c(e # ) e.fn e.fn = e e.mn(e # ) (expressions) let x = e tin e synch..