Gradual Ownership Types

Ilya Sergey and Dave Clarke

Katholieke Universiteit Leuven

DistriNet,   Dept. Computer Science

Gradual Ownership Types are a framework to annotate programs with ownership types in a lightweight way, allowing only partial information about object owners to preserve the Owners-as-Dominators property for the object graph of a program. The front-end compiler is implemented for Java 1.4 via JastAdd as an extension of JastAddJ: The JastAdd Extensible Java Compiler.

The compiler performs type-checking on the provided source files and generates translated source files with inserted dynamic checks if the key -gen is provided.

Download

• Get the sources from GitHub
• Pre-built JAR file

Build

All tools needed (jastadd2, jflex, beaver, etc.) are included into the archive with sources. You only need to have javac and Apache Ant installed in order to build. The ant script build.xml is located in the root folder of the archive. Inspect the README file for more information about the project structure.

To build the jar file with the compiler, run

  > ant rebuild.all 

To run compiler tests:

  > ant run.tests

Run

How to run the OwnershipChecker (make sure that OwnershipChecker.jar is included into your Java classpath):

  > java OwnershipChecker java-source-files 

See what options are available, e.g., for optional generation of sources with dynamic checks inserted:

  > java OwnershipChecker -help
 

Technical report

• Gradual Ownership Types   Ilya Sergey and Dave Clarke, Report CW 613, Katholieke Universiteit Leuven, December 2011.

Example

class E /*< P >*/ {
  // the owner of myD is NOT specified
  D myD = new D /*< P >*/();
}

class D /*< owner >*/ {
  // the owner of e is specified
  E /*< owner >*/ e;
  
  void use(D /*< owner >*/ arg) { 
    System.out.println(arg.toString()); 
  }
  
  void exploit(E /*< owner >*/ arg) { this.e = arg; }

  void test() {
    final E e = new E /*< this >*/();
    // exact owner of d is unknown
    final D d = e.myD;
    // safe argument passing
    // owners of the receiver and the argument are equal
    d.use(d);
    // non-safe argument passing
    // dynamic type cast will be inserted
    d.exploit(e); 
  }
}