The Manual of Version 0.1
http://www.it.uu.se/research/upmarc/loci

Tobias Wrigstad and Amanj Sherwany


31st March 2011



Loci is a subproject of UPMARC1 umbrella project



Some parts of this document, are taken from the Checker framework’s manual:
http://types.cs.washington.edu/checker-framework/

Copyright (C) 2010-2011 Tobias Wrigstad and Amanj Sherwany.

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license can be found at http://www.gnu.org/licenses/fdl.txt.

1  What is Loci?

Loci is a pluggable type checker, helps the programmer to check the correctness of the thread locality in their programs. It uses a simple statically checkable set of annotations. The current implementation of Loci only supports Java programming language, but we hope to deliver support for other programming languages as well (especially porting to other Java-like programming languages should be straight forward).
This checker uses the Checker framework2, which makes it very easy to use once Java 8 is out3. Nevertheless, you can still use it with the Java 6 compiler4.
Loci is designed in such a way to be backward compatible with the current Java programs, we made sure to support pre-Java 5 programs as well. In order to make sure that we do not break backward compatibility, we applied Loci on lucene 2.4.1 search library and we could annotate almost the whole system without having any incompatibility issues5.
If you apply Loci on your legacy code, it still stays completely backward- compatible: your code compiles with any Java compiler, it runs on any JVM, and your coworkers do not have to use the enhanced type system if they do not want to. You can check only some parts of your program. Type inference 6 tools exist to help you annotate your code.

1.1  How Does Loci Work?

Loci adds several annotations to the standard Java programming language, to let the programmer express thread locality:

1.2  Logical View of the Heap 9

In Loci, the heap of a program with n threads is logically partitioned into n number of isolated heaps, called “heaplets”, plus a shared heap. There is a one-to-one mapping between threads and heaplets. From now on, heap refers to the shared heap accessible by all threads, and heaplets refers to thread-local heaps. The Loci annotation system enforces the following simple properties on Java programs, shown in Figure 15:

  1. References from one heaplet into another are not allowed ();
  2. References from heaplets to the shared heap are unrestricted ();
  3. References from the shared-heap into a heaplet must be stored in a thread-local field ().

The third property above ensures that even though a reference into a heaplet ρi may exist on the shared heap, it is only accessible to the thread i to which ρi belongs. If another thread j reads the same field, it will either get a reference into its own heap ρj that it had written there before, or a thread-local copy of the default value of the field (which may be null). Effectively, there is a copy of each thread-local field for each active thread in the system and writes and reads of the same thread-local field by different threads access different copies. Together, these simple properties make heaplets effectively thread-local, and objects in the heaplets are thus safe from race conditions and data races.


    
Figure 1: Thread-Local Heaplets and a Shared Heap. The teal area (ϱ) is the shared heap, white areas (ρ1..ρ4) represent the thread-local heaplets. Solid arrows are invalid and correspond to property 1 in Section 1.2, dashed arrows are valid pointers into the shared heap (property 2), respectively from the shared heap into heaplets (property 3, when “anchored” in a bullet). The right-most figure is a Venn diagram-esque depiction of the same program to illustrate the semantics of the shared heap.

2  Installing and Using Loci

2.1  Installing the Loci Plugin 10

Loci is designed in a way to be easy to install in future Java releases11, as it only depends on the (to be) standard Java libraries.

Those who want to try Loci with the Java 6 and 7, can follow the following steps:

  1. Requirement: You must have JDK 6 or later installed. You can get JDK 6 from Oracle or elsewhere. If you are using Apple Mac OS X, you can use Apple’s implementation or SoyLatte. The installation process is simple!
  2. Install the enhanced javac:
  3. Put Loci jar file in your Classpath:

2.1.1  Using Loci with Maven, Ant and different IDEs

Loci has an awesome support for Maven, Ant and most of the IDEs. It already has a Maven12 plugin, to use it you can add the following to your pom.xml:

First you need to declare Loci as a dependency:
<dependencies>
    <!-- Loci annotation processor -->
    <dependency>
        <groupId>net.java.loci</groupId>
        <artifactId>loci</artifactId>
        <version>0.1</version>
    </dependency>

    <!-- other dependencies -->
</dependencies>

And finally, you need to attach the plugin to your build lifecycle:
<build>
    <plugins>
        <plugin>
            <groupId>net.java.loci</groupId>
            <artifactId>loci-plugin</artifactId>
            <version>0.1</version>
            <executions>
                <execution>
                    <!-- run Loci after compilation; this can also be any later phase -->
                    <phase>process-classes</phase>
                    <goals>
                        <goal>check</goal>
                    </goals>
                </execution>
            </executions>
            <configuration>
                <!-- required configuration options -->

                <!-- other optional configuration -->
                <!-- full path to a java executable that should be used to create the forked JVM -->
                <executable>/opt/java1.6/bin/java</executable>
                <!-- should an error reported by Loci cause a build failure, or only be logged as a warning; defaults to true -->
                <failOnError>true|false</failOnError>
                <!-- a list of patterns to include, in the standard maven syntax; defaults to **/*.java -->
                <includes>
                    <include>
                     org/company/important/**/*.java
                    </include>
                </includes>
                <!-- a list of patterns to exclude, in the standard maven syntax; defaults to an empty list -->
                <excludes>
                    <exclude>
                     org/company/notimportant/**/*.java
                    </exclude>
                </excludes>
                <!-- additional parameters passed to the JSR308 java compiler -->
                <javacParams>-Alint</javacParams>
                <!-- additional parameters to 
                 pass to the forked JVM -->
                <javaParams>-Xdebug</javaParams>
                <!-- versions of JSR308 to use; defaults to the current newest version: 1.1.2,
                		You cannot provide pre (1.1.2) -->
                <jsrVersion>1.1.2</jsrVersion>
            </configuration>
        </plugin>
    </plugins>
    <!-- other plugins -->
</build>

You can also use this plugin, with Ant as well as different IDEs. For more details, please visit this page: http:// types.cs.washington.edu/checker-framework/#external-tools

2.2  Summary of Command Line Options13

You can pass command-line arguments to a checker via javac’s standard -A option (“A" stands for “annotation"). Loci supports the following command- line options:

-Awarns
Treat checker errors as warnings
-AskipClasses
Suppress all errors and warnings at all uses of a given class
-Alint
Enable or disable optional checks
-Astubs
List of stub files or directories
-Afilenames, -Anomsgtext, -Ashowchecks
Aids for testing or debugging a checker

2.3  Supported Lint Options

Loci has four lint options:

-Alint:ThreadSafe
tells the checker to print a warning whenever a @Shared 14 variable is assigned into a @ThreadSafe variable.
-Alint:ManuallyVerified
tells the checker to print a warning whenever it sees a @ManuallyVerified method
-Alint:Upcast
tells the checker to print a warning whenever an unsafe upcast is found
-Alint:AllWarnings
tells the checker to print a warning in all the above cases

2.4  A HelloWorld Example

Whenever you want to use Loci, you have to import loci.quals.* package. In the following listing, we show you a simple Java program and apply Loci on it.

import loci.quals.*; //import loci qualifiers @Local public class HelloWorld{ //a thread local class @Shared Object b; //a shared field public static void main(String... args){ System.out.println("Example"); } }

To compile the above program using the Loci checker plugin:
$ javac -processor loci.LociChecker HelloWorld.java
The above program, should not report any problem, while the below program should do:

import loci.quals.*; @Local public class BadHelloWorld{ @Shared Object b = new @Local Object(); public static void main(String... args){ System.out.println("Example"); } }

$ javac -processor loci.LociChecker BadHelloWorld.java
The above program will report some message similar to:

BadHelloWorld.java:3: incompatible types.
    @Shared Object b = new @Local Object();
                                              ^
 found : @Local Object
 required: @Shared Object
1 error

2.5  Compatibility Tip15

In order to make your code compilable with any Java compiler (even pre-Java 5 compilers), you can easily put the annotations within comments. Consider the following code:

import loci.quals.*; /*@Local*/ public class HelloWorld{ /*@Shared*/ Object b; public static void main(String... args){ System.out.println("Example"); } }

The checker automatically reads the annotations from the comments (note that, there should be no space between the annotation and the left or right asterisks of the comment). This feature only works if you provide no -source command-line argument to javac, or if the -source argument is 1.7 or 7.

You can also get rid of import loci.quals.*; statement, by adding the following environment variable:

# Unix:

$ export jsr308_imports=loci.quals.*
# Windows:

C:> set jsr308_imports=loci.quals.*

Or, provide this option to your javac statement:
jsr308_imports=loci.quals.* 16

3  Technical Details About Loci

3.1  Loci Annotations

Loci defines three annotations for thread-locality:

3.1.1  Annotations on Class Declarations

A class annotated as @Local always creates thread-local instances. A class annotated as @Shared always creates shared instances. A class which has no explicit annotation and has no direct or indirect @Shared or @Local superclass (or implemented interfaces) is treated specially17 and can be used to create both shared and thread-local instances and is useful for libraries and other situations where flexibility is desirable (e.g., because future usage is uncertain).

A @Shared class has exactly the same semantics as a normal Java class. @Local and flexible classes must additionally uphold the following property:

A @Local or a flexible class may not assign this to a field where it may be accessible by another thread.”

This is checked at compile-time by Loci and errors are reported to the user.

3.1.2  Annotations on Types

The three annotations above may be used on types to express thread-locality. A type annotated @Local T denotes a thread-local instance of class T (modulo subtyping) and a type annotated @Shared T denotes a shared instance of class T.

The @ThreadSafe annotation is used to allow a limited form of parametricity (cf. Section 3.10) and denotes an object whose thread-locality is not known and must therefore be treated conservatively.

As for @Owner, if c is declared without having an explicit annotation and is an instance of class T when T is a flexible class, then c’s annotation will be the same as the object that contains it.

A field annotated @Local points to a thread-local value (or null). However, we do not allow @Local or @ThreadSafe fields inside non-@Local classes, if you need them, you have to implement them through a java.lang.ThreadLocal indirection, which degrades performance. This is necessary since the enclosing object might be shared across threads making the field effectively shared too.

Due to conservative approximation, @Shared ⇏ that a value is shared (only that it may be shared). However @Local ⇒ that a value is thread-local.

Clearly, at run-time, every value is either thread-local or not. The purpose of @ThreadSafe annotation is to enable flexibility and variability in a design, e.g. methods that accept both @Local and @Shared values, such as Java’s equals methods.

3.1.3  Constraints on Dataflow

Loci requires that dataflow preserves annotations, except for assignments into @ThreadSafe. This dictates what must hold if the contents of a variable y is stored into a variable, field or parameter x (by assignment, argument passing, etc.). For clarity, a summary is found in Figure 2 and Figure 3.


Type of x        Type of y        Result
@Local         @Local          (OK)
@Local         @Shared          (Compile-time error)
@Local         @ThreadSafe         (Compile-time error)
@Shared         @Local         (Compile-time error)
@Shared         @Shared         OK
@Shared         @ThreadSafe         (Compile-time error)
@ThreadSafe         @Local         OK
@ThreadSafe         @Shared         OK (With warning)
@ThreadSafe         @ThreadSafe         OK
Figure 2: Overview of dataflow constraints on Loci annotations when the value in y flows into x.


 
Figure 3: Annotation lattice capturing dataflow constraints. Each wedge denotes permitted dataflow. ⊥ denotes “free” objects.

3.1.4  Annotations and Subclassing

Subclassing must preserve all annotations visible in the interface. @Shared classes may only implement and extend @Shared and flexible interfaces and classes. And, @Local classes may only implement and extend @Local and flexible interfaces and classes.

Since private methods do not participate in overriding, they are safe to change annotations (and types) in any way.

Furthermore, for class-level annotations, a “flexible” class may be subclassed both as a @Local class or a @Shared class (all other annotations in the interface must be preserved).

Since the interface of java.lang.Object constrain its subclasses’ interfaces, we show it here:

public class java.lang.Object { //Object is a flexible class public java.lang.Object(); public final native @Shared java.lang.Class getClass(); public native int hashCode(); public boolean equals(@ThreadSafe java.lang.Object obj); protected native @Owner java.lang.Object clone(); public java.lang.String toString(); public final native void notify(); public final native void notifyAll(); public final native void wait(long time); public final void wait(long time, int x); public final void wait(); protected void finalize(); }

Note the annotation on the return type of clone(). It means that cloning a @Local object will give back another @Local object, cloning a @Shared object will give back another @Shared object, etc. Cloning a @Local object into a @Shared object or the inverse, must be done through another method.

3.1.5  Subtyping and @Owner

As mentioned previously, @Owner denotes the type holds it, to have exactly the same thread locality as the object contains it, for example:

class B{ Object value; //value is implicitly @Owner void setValue(Object b){ //Object b is implicitly @Owner value = b; } Object getValue(){ //returns an @Owner Object return value; } } @Shared B a = ...; //substitute every occurrence of //@Owner inside ``a'' with @Shared @Local B b = ...; //substitute every occurrence of //@Owner inside ``b'' with @Local a.value = new @Local Object(); //Not OK, a.value is @Shared a.value = new @Shared Object(); //OK, a.value is @Shared b.value = new @Local Object(); //OK, b.value is @Local b.value = new @Shared Object(); //Not OK, b.value is @Local

When a type is @ThreadSafe, that means Loci does not know it’s thread locality. and thus Loci treats it carefully. Therefore, Loci cannot guarantee the proper thread locality of its @Owner types. If we treat all the @Owner types as its enclosing instance (here @ThreadSafe), then the @Owner types become @ThreadSafe, which makes the follow code legal, despite having a serious leak.

@Shared B b = ...; //b.value should be @Shared @ThreadSafe B c = b;//if we suppose that c.value is @ThreadSafe c.value = new @Local Object();//Leak!

By following the same semantics of Generics in Java, we could easily forbid this. Consider the following “plain” Java code:

class Cell<T>{ void set(T t){...} T read(){...} } Cell<Object> b = ...;

 Cell<?> c = b; //Java loses the type information

Object b = c.read(); //OK c.set(new Object());//Is not OK

Therefore, Loci does not permit @Owner types belonging to a @ThreadSafe type to be written into, and it treats them in a read-only manner. However, @Owner types belonging to @Local and @Shared are still allowed to be read and written into.

@ThreadSafe B c = ...; //Now, every occurrences of @Owner treated in a read-only manner c.value = ...; //Not OK, c.value is read only c.setValue(...); //Not OK, the parameter is treated in a read-only manner @ThreadSafe Object value = c.getValue(); //OK

3.2  Exceptions

In Loci, exceptions are always thread-local. The class java.lang.Throwable, which is the common superclass of all errors and exceptions in Java, has been annotated @Local, meaning it can only be used to create thread-local instances. If you want to use exceptions to return shared values from a deeply nested stack, you can still do so in a shared field.

Adding annotations to specficiations of exceptions in a method is not necessary, and the only legal annotation is @Local.

3.3  Type Casting

In Loci, the default annotation for type casting is the annotation which can be retrieved from the expression part of the cast:

Object obj = "hello"; String str = (String) //this is the casting part obj; //this is the expression part

Sometimes you need to specify which annotation should the type cast have, like in equals method where the parameter’s annotation is @ThreadSafe Object and we want to downcast it to a @Shared class or @Local class, as in the following example:

@Shared class B{ public boolean equals(@ThreadSafe Object obj){ if(obj instanceof B){ B b = (@Shared B) obj; ... } ... } }

When providing an annotation, Loci reports an error if the annotation either is not identical with the annotation that can be derived from the expression part, or with the annotation on the class that we downcast to.

@Shared class B{ public boolean equals(@ThreadSafe Object obj){ if(obj instanceof B){ ... = (@Shared B) obj; //OK ... = (@Local B) obj; //Produces an error ... } ... } }

3.4  Interfaces

Loci supports annotations on interfaces just like on classes. By default interfaces are “flexible” to allow them to be implemented by both @Local and @Shared classes, and the default annotation on types mentioned in an interface is @Owner. As an example, the following interface declaration:

interface AnInterface { @Shared Bar method(Foo e); }

is equivalent to the following interface, with the annotations elaborated in:

interface AnInterface { @Shared Bar method(@Owner Foo e); }

When an interface is implemented by a class, the @Owner annotation is replaced by the annotation on the class, just like @Owner annotations are elaborated in for regular classes18. As an example, the following is correct:

@Local class AnImpl implements AnInterface { @Shared Bar method(@Local Foo e) { ... } }

but the following is not:

@Local class AnImpl implements AnInterface { Bar method(@Shared Foo e) { ... } }

and produces two compile-time errors: (1) method should return a shared Bar instance not an (implicitly) thread-local, and (2) expects a thread-local argument, not a shared one. Notably, if the annotation on AnInterface was @Shared, the first example would have been wrong and the second correct.

3.4.1  Constraining Interfaces with Annotations

If annotations are put on an interface, they will constrain classes implementing the interface in a straightforward fashion. As an example, AnInterface above requires all classes implementing it to return a @Shared Bar from method or a compile error will be signalled.

3.4.2  Interface Annotations and Inheritance

Interface annotations and inheritance work exactly as for classes. A “flexible” interface can be extended (and implemented) by “flexible”, @Shared or @Local interfaces (or classes), a @Shared interface must be extended (and implemented) by @Shared interfaces (or classes), and a @Local interface must be extedned (and implemented) by @Local interfaces (or classes).

Annotations on methods must be preserved and overloading based on annotations is not permitted.

3.5  Arrays

Loci supports thread-local arrays with thread-local data, and shared arrays with shared data. Thread-locality of the elements of an array is the same as the array variable’s thread-locality, and instances of @Shared and @Local classes may only be stored in @Shared and @Local arrays respectively. The reason why mixed thread-locality is not supported is purely technical and slightly subtle19.

For concreteness, consider the following three classes with different thread-locality:

@Shared class A { ... } @Local class B { ... } class C { ... }

Now, consider the possible ways of creating arrays of instances of these classes:

@Shared A[] a1; //Legal shared array of shared elements @Local A[] a2; //Illegal @Local B[] b1; //Legal thread-local array of thread-local elements @Shared B[] b2; //Illegal @Shared C[] c1; //Legal shared array of shared elements @Local C[] c2; //Legal Thread-local array of thread-local elements

If an array of a different thread-locality than its elements is required, one must use an extra level of indirection, e.g.:

@Local class Proxy { @Shared A[] a3; }

However, an array of a primitive type, should still have @Local element type, regardless of the annotation on the array itself:

int @Shared [] a1; //@Shared array of type @Local int, which is equivalent to @Local int @Shared [] a2; //same as the above int[] a3; //denotes a @Local array of type @Local int

3.6  Inner Classes and Nested Classes

Loci imposes no restrictions on nested (or inner) classes. A @Shared class can have a nested (or inner) @Local class, and vice versa. To protect thread-locality, however, a few additional restrictions are in place for inner classes:

  1. A @Shared inner class may only access explicitly @Shared parts of any enclosing class.
  2. An @Owner inner class is always instantiated with the same thread-locality as its enclosing instance.

As an illustration of point (1) above, consider the following class and variable definitions:

@Local class A { @Shared Object s; @Local Object t; @Shared class B { Object a = s; // OK @Local Object b = A.this; // Not ok @Local Object c = A.this.t; // Not ok } }

To illustrate point (2) above, consider the following class and variable definitions:

class A { class B { ... } @Shared class C { ... } } @Local A x; @Shared A y; A z; // @Owner implicit

Now, the instantiation x.new B() has type @Local B, y.new B() has type @Shared B and z.new B() has type @Owner B. Consequently,

@Shared B b = x.new B();

does not compile as x.new B() is thread-local, however

@Shared C b = x.new C();

is legal as C is declared as @Shared.

3.7  Anonymous Classes

Loci fully supports anonymous classes. If the new expression uses an annotation, this is used (if legal, same rules apply as for instantiating classes). Otherwise, the new object inherits thread-locality from the annotation on the class or interface they were constructed from, possibly @Owner. Examples:

@Local interface A {} @Shared interface B {} interface C {} new A() {}; // Has type @Local A new B() {}; // Has type @Shared B new C() {}; // Has type @Owner C @Shared C a = new @Shared C() {}; // OK @Shared C b = new C() {}; // OK, expands to new @Shared C() @Local C c = new C() {}; // OK, expands to new @Local C() C d = new C() {}; // OK, expands to new @Owner C()

The code example below shows that the checking is straightforward as anonymous classes are simply a syntactic shorthand.

interface A {} class B { void m(@Local Object a) { A b = new A() { Object x = a; // Not OK, since the instance is @Owner @Local Object x = a; // OK }; @Local A c = new @Local A() { Object x = a; // OK }; } }

3.8  Constructors and Instantiation

Constructors follow the same rules as methods. In a @Shared class, this is @Shared and in a @Local class, this is @Local. When compiling a “flexible” class, it is unknown at compile-time how it is going to be used, and conservatively, this must be treated as @Owner (i.e., only be stored in @Owner fields and variables, etc.).

A @Shared or a @Local class always produce @Shared or @Local instances, respectively. When instantiating a “flexible” class, the resulting instance can be either, @Shared, @Local or @Owner and is specified by adding an annotation to the new expression. Assume the following class:

class Foo { public Foo() { ... } public Foo(@Owner Object b) { ... } }

where @Owner has been made explicit for clarity. Instantiating the class, we might write:

... = new @Shared Foo(); // Creates a @Shared foo ... = new @Local Foo(); // Creates a @Local foo ... = new Foo(arg); // Creates an @Owner foo

For convenience, Loci can infer thread-locality if the annotation is missing using the following rules (order is insignificant):

  1. If a parameter annotated @Owner is bound to a @Shared argument, the resulting instance must be shared. If arg on line 3 above is @Shared, the expression has type @Shared Foo.
  2. If a parameter annotated @Owner is bound to a @Local argument, the resulting instance must be thread-local. If arg on line 3 above is @Local, the expression has type @Local Foo.
  3. If neither of the above rules apply (e.g., because arg was annotated @Owner, or because there were no arguments, or these were all primitive, immutable or null), the thread-locality is determined by the annotation on the variable (or equivalent) which holds it.

All @Owner parameters must be bound to arguments of the same thread-locality, or it results in a compile-time error. Examples of the third rule above:

@Shared Foo = new Foo(); // Creates a @Shared Foo @Local Foo = new Foo(); // Creates a @Local Foo Foo = new Foo(); // Creates an @Owner Foo

We expect that most instantiations will be resolved by inference, rather than by explicit annotation. Importantly, the inferred annotation is always maximally permissive and there is no additional expressiveness from explicit annotations on instance creation except clarity or to express programmer intent.

Notably, with explicit annotations, constraints flow in the opposite direction, if we write new @Local Foo(arg) and the constructor parameter is @Owner, then arg must be @Local.

3.9  Static Fields, Blocks and Methods

In static context, the enclosing object is a class object, which is shared by all threads (in Loci’s eyes —completely ignorant of class loaders, etc.). Consider the following class:

@Local class Foo { static Object f; static { @Shared Object x = new Object(); f = x; // OK, f is implicitly @Shared } static Object id(Object o1) { return o1; } static Foo fooId(Foo o2) { return o2; } }

Since instances of Foo will always be thread-local, o2 implicitly becomes @Local. For the remaining variables and types, as Object is a “flexible” class, their implicit annotation is @Owner. However, since we can trivially decide that they exist in a static context, which is implicitly shared20, we can immediately change @Owner to @Shared. Notably, o2 stays @Local and x stays @Shared.

Consequently:

Foo.f = new @Local Foo(); // Not OK, Foo.f is @Shared Foo o = new Foo(); // o is implicitly @Local Foo.id(o); // Not OK, id takes @Shared argument o = Foo.fooId(o); // OK (both return and argument)

Loci does not allow annotating static fields with @Local and @ThreadSafe. In order to have them, you have to use ThreadLocal indirection. Although, you still can have @Local and @ThreadSafe method parameters, method return and variables inside a static method.

3.10  Annotation-Polymorphic Methods

The id method in the above example has the downside of forcing its arguments to be @Shared. Since Java does not do overloading based on annotations, we cannot simply create two versions of the method. If you need a method to handle arguments of any thread-locality, this can be solved by using parametric polymorphism (where @X 21 can be instantiated with any valid Loci annotation):

<@X T extends Object> static T id(T o) { return o; }

In the body of id, the thread-locality of o cannot be determined statically (since it may vary with call-site). The annotation on T controls how it can be assigned inside the method:

<@X T extends Object> void example(T o) { T u = o; //OK @Shared Object bad1 = o; // Not allowed @Local Object bad2 = o; // Not allowed Object bad3 = o; //Not allowed }

Correctness for the first assignment can be established by tracing the origin of u to see that although thread-locality is unknown, it is preserved. But the next three assignments, are all not allowed, for the first two, it is obvious, and the third one, since it is not a must that the owner of this method should have the same thread locality as the passed parameter.

Loci allows instantiation of different type parameters with objects of different thread-locality. Given the following method definitions:

<@X T extends Object> void m1(T o1, T o2) { ... } <@X T1 extends Object, @X(2) T2 extends Object> void m2(T1 o3, T2 o4) { ... }

We are only allowed to call m1 with arguments o1 and o2 of the same thread-locality. For m2, o3 and o4 can have different thread-locality as they have different parametric types (albeit identical in their definition). Notably, since o3 and o4 can have different thread-locality in m2, assigning between them is not allowed.

As a convenience, @ThreadSafe annotation can be used on method parameters and return type to express unknown, parametric thread-locality. @ThreadSafe parameters may not flow into @Local or @Shared variables etc. This is useful for typing methods such as equals.

void m(@ThreadSafe Object o) { ... } @Local Object x = ...; @Shared Object y = ...; m(x); // ok m(y); // ok

At last, defining a method that takes multiple parameters of different types but with the same parametric thread-locality can be done by providing @X 22 with the same passed number:

void <@X T1, @X(2) T2, @X(2) T3> m(T1 o1, T2 o2, T3 o3){...}

When calling the above method, o2 and o3 must have the same annotation, while o1’s can be different.

3.11  Parametric Polymorphism (Generics)

With JSR 308, Loci supports annotations on type parameters, both on classes and methods. Annotations are bounded similar to how types are bounded by the extends clause. If a bound on annotations is not explicitly defined, the annotation on the (possibly implicit) upper class bound is used. Thus, for the following Pair class:

class Pair<T> { T fst; T snd; }

We can derive the bound on the annotation by first elaborating in the default upper class bound:

class Pair<T extends Object> { T fst; T snd; }

and then inserting the annotation on the class bound:

class Pair<T extends @ThreadSafe Object> { T fst; T snd; }

Generics Java types suffer from the same problems as arrays —subsumption to Object allows forgetting any parameterized thread-locality at the type level. Absence of run-time type information further precludes downcasting. Thus, annotations on type variables are the same as the type parameter boundaries, unless they are annotated explicitly. For example, the type @Shared Pair<Object> denotes a shared pair of threadsafe objects. There is no way of specifying a shared pair of non-threadsafe objects except expressly bounding T by @Local Object or by @Shared Object.
However, we could still have @Shared Pair<Exception> or @Shared Pair<Thread> (taking that Exception is always @Local and Thread is always @Shared).
The rule is:
Loci does not allow annotations on type variables, except in the following cases:

  1. The annotation on the type variable matches the annotation on its class. e.g. Exception is @Local, thus Pair<Exception> == Pair<@Local Exception>
  2. The annotation on the type variable matches the annotation on the type parameter.

As we mentioned above, the generics suffer from the same problems as arrays when downcasting, consider this example:

@Local class Cell<T extends Object>{ //equivalent to T extends @ThreadSafe Object T f; } Cell<Thread> c; @Local Object o = c; Cell c2 = (Cell) o; c2.f = new Exception(); //c.f now contains @Local object, which leads to leak!

To prevent this, Loci reports a warning whenever it sees a downcasting or an assignment that goes from an instance with less type variables to an instance with more type variables, unless the annotations on the type parameters are predictable (i.e either @Local or @Shared) hence, (Cell is counted as Cell<Object>)23.

class A<T extends Object>{...} class B<K extends Object, T extends Object> extends A<T>{...} class C<K extends @Local Object, T extends Object> extends A<T>{...} A<Object> a; B<Object, Object> b= (B<Object, Object>) a; //Produces a warning C<Object, Object> c= (B<Object, Object>) a; //Does not produce a warning

A good way to avoid warnings when writing boolean equals(Object obj) method, for the classes with uncertain type variables, is doing something similar to:

@Local public class Cell<T, K>{ T t; K k; public boolean equals(Object obj){ //Cell<T, K> temp = (Cell<T, K>) obj; produces a warning, see above

   Cell<?, ?> temp = (Cell<?, ?>) obj; //It is OK

T fst = (T)temp.t; K snd = (K)temp.k; ... } }

3.12  Java’s Thread API

In Loci, the java.lang.Thread is a @Shared class and java.lang.Runnable is a @Shared interface. This is natural, as instances of the Thread class are always shared between two threads: the creating thread and the thread it represents.

If a run() method wants to store thread-local data in fields, rather than creating heavy-handed thread-local fields in the thread class, an extra level of indirection is recommended:

@Local class ThreadLocalComputation { Foo f; void doIt() { ... } } @Shared Thread t = new Thread() { void run() { new ThreadLocalComputation().doIt(); } };

This way, there is no need for an extra indirection in f and there is no actual semantic difference. If a shared channel is needed for communicating between the new thread and its creator, simply install a @Shared back-pointer to the actual thread object in ThreadLocalComputation.

As a result of these default annotations, Loci works naturally with Java ThreadPools. Java’s InheritableThreadLocal also works well with the annotations as inherited values are fresh thread-local copies for the new thread. Extending Loci to support InheritableThreadLocal is straightforward.

3.13  Understanding Annotation Defaults

Class declarations
A class is “flexible” (as every class is a subclass of Object) unless the class, its superclass or at least one of implemented interfaces is annotated as @Local or @Shared.
Interface declarations
follow the same rules as for classes. If a super interface is @Local (or @Shared) no other extended interfaces may be @Shared (or @Local).
Types
defaults depend on their class part. Since @Local and @Shared classes always have thread-local respective shared instances, types of such classes must be @Local or @Shared, respectively, and default accordingly. For types of “flexible” classes, their annotation default to “@Owner,” meaning the thread-locality of the current this (which is @Shared in a @Shared class, @Local in a @Local class and unknown at compile-time otherwise).
Exceptions
are always @Local, since the root class of the exception hierarchy is @Local. Consequently, exceptions never need explicit annotations.

3.14  Primitive Types and Immutable Classes

Primitive types and immutable classes can safely be ignored by the Loci system. If they are not annotated, the system will ignore them and allow them to be treated in any way allowed by Java. Since primitive values have value semantics, they are inherently thread-local and there is little point in annotating them.

However, if a type of immutable class, like String or Integer is explicitly annotated, Loci will treat the immutable class just like any ordinary class. The reason for this is to allow expressing dependencies to allow for a Loci-aware run-time system to play tricks with locality.

3.15  Java’s java.lang.ThreadLocal API

Java’s ThreadLocal API has the following annotations:

@Shared public class ThreadLocal<T extends @Local Object> extends Object{ protected T initialValue(); public T get(); public void set(T value); public void remove(); }

As one would expect, only thread-local values can flow in and out of a thread-locality indirection.

In Loci, a @Local and @ThreadSafe field in a @Shared or “flexible” class, should be expanded to a @Shared field with a ThreadLocal indirection, i.e.,

@Shared class Example { @Local Foo f; //not valid @Local Foo bar() { return f; } }

Should be expanded to

@Shared class Example { @Shared ThreadLocal<Foo> f = new ThreadLocal<Foo>(); @Local Foo bar() { return f.get(); } }

3.16  The @ManuallyVerified Annotation

The @ManuallyVerified annotation is a “core Loci” annotation used internally for developing thread-locality preserving API’s that the Loci tool itself is not strong enough to type check (such as the ThreadLocal API class above). It should be used with utmost care for implementing “language-level” API’s where thread-locality preservation is manually verified. Examples of code that use this annotation is ThreadLocal classe.

Only methods can have @ManuallyVerified, and it should only appear on the return type, example:

class B{ @ManuallyVerified @Local Object method(){ //Warnings and errors here are ignored } }

Loci only checks the signature of @ManuallyVerified methods, statements within the body are not checked. It is better to postpone putting the @ManuallyVerified as much as possible (possible, delay it until you are totally done with annotating your program).

4  Known Bugs and Reporting New Bugs

4.1  Known Bugs

This version of Loci comes with some known bugs, some are out of our control and we cannot fix them (as they are from the Checker framework), and others should be fixed in the future releases.

4.1.1  Implementing Parameterized Interfaces

When implementing a parameterized type (say Comparable) if you provide the type arguments, you also need to provide their correct annotations, otherwise Loci rejects the code:

For example, this code produces an error:

@Local class A{} class B extends A implements Comparable<B>{ public Comparable getValue(){ return new Test(); //Loci, accepts this } ... }

But, if we provide the correct annotation, then Loci accepts it:

@Local class A{} class B extends A implements Comparable<@Local B>{ public Comparable getValue(){ return new Test(); //Loci, accepts this } ... }

4.1.2  Anonymous Classes “Sometimes” Need Extra Annotations

Sometimes, when you have an anonymous class, and it has an implicit annotation other than @Owner, you might need to add the right annotation explicitly to prevent Loci from producing false reports.

for example:

abstract class A{ m(); } @Shared class B{ Object method(){ return null; } void m1(){ A a = new @Shared A(){ //We need to put this annotation, even though it // should be obvious in Loci's eyes, that this // class should be @Shared as it is located // in an @Shared class to prevent Loci from // producing an error in the line // (Object b = new method();) public m(){ Object b = method(); } } } }

Or, in this example:

abstract class A{ A(A b, @Shared Object k){} public abstract A m(); public static A getA(){ return null; } } public class ClassTest{ void m(A b){ @Shared A dd = b.getA(); dd = new @Shared A(dd, b.getA()){ //Even though, Loci should automatically detect // the implicit annotation here, it fails. // Unfortunately, that is because, Loci expects the // called constructor to be inside the anonymous class body! // and fails to fetch the correct constructor element // (which is practically inherited from the // abstract class A) public A m(){return null;} }; } }

4.1.3  Non-Flexible Child Class Calls a Method From Flexible Parent Class

Suppose we have these two classes:

class A{ //A Flexible class void method(Object b){...} //the annotation over b is @Owner } @Shared class B extends A{ void method(Object b){ //b is implicitly @Shared super.method(b); //Loci reports an error, // saying, b is @Shared while @Owner is required //and the error can be safely ignored //since we know, every instances of the current B //can only be @Shared. ... } }

4.1.4  Miscalculating Arrays of Type Variables

As we mentioned before24, in Loci arrays should have the same annotation as its elements, consider the following:

class B<T>{ T[] method(){...} } B<Exception> b = new B<Exception>(); Exception[] array = b.method(); //Produces an error, telling that //b.method() returns Exception @ThreadSafe[] //array, while Exception @Local[] is required, //this occurs due to mis-understanding between //Loci and the framework that we have used to implement //Loci. Again, you can easily ignore this error by using //@ManuallyVerified.

4.1.5  Some Methods in the Standard JavaSE Library are not “Correctly” Annotated

Although, we have annotated most of the classes of the Standard JavaSE library, but still there are many of them haven’t been annotated. please if you faced any of them, file a bug report 25.

4.1.6  Incorrect Inference of Method Type Arguments

This is a bug from the Checker framework, and it is already patched but haven’t been pushed to a stable version yet, once they fixed the code Loci works as it should26.

4.2  Avoiding Bugs

In order to avoid bugs, you can put @ManuallyVerified on your methods, so that the Loci compiler does not complain about the code. We encourage you to put the @ManuallyVerified when you are done with annotating the body of the method, and postpone putting the @ManuallyVerified to the last moment.

4.3  How to Report Bugs?

If you have a problem, please file a bug at
http://java.net/bugzilla/buglist.cgi?product=loci&order=Importance&limit=25.
(First, check whether there is an existing bug report for that issue.) Alternatively (especially if your communication is not a bug report), you can create a thread in Loci’s forum at http://java.net/projects/loci/forums. We welcome suggestions, annotated libraries, bug fixes, new features, and other improvements.

Please ensure that your bug report is clear and complete. Otherwise, we may be unable to understand it or to reproduce it, either of which would prevent us from fixing the bug. Your bug report will be most helpful if you:

  1. Add -version and -verbose to the javac options. This causes the compiler to output debugging information, including its version number.
  2. Indicate exactly what you did. Don’t skip any steps, and don’t merely describe your actions in words. Show the exact commands by attaching a file or using cut-and-paste from your command shell;
  3. Include all files that are necessary to reproduce the problem. This includes every file that is used by any of the commands you reported, and possibly other files as well.
  4. Indicate exactly what the result was by attaching a file or using cut-and-paste from your command shell (don’t merely describe it in words). Also indicate what you expected the result to be – Remember, a bug is a difference between desired and actual outcomes.

5  More Help...

6  Acknowledgments

Many thanks to the developers behind the Checker’s framework27. Without their awesome tool, and continuous help, this tool wouldn’t exist. We also thank Adam Warski28 who developed a Maven2 plugin for the Checker framework, and we re-used his code base to develop a Maven2 plugin for Loci. Also many thanks to Nosheen Zaza, she gave useful tips and comments, also she contributed by Loci's logo and revised this manual.


1
Uppsala Programming for Multicore Architectures, http://www.it.uu.se/research/upmarc
You also can find Loci’s research homepage at:
http://www.it.uu.se/research/upmarc/research/pl/facile
2
A framework that enhances Java’s type system to make it more powerful and useful. And lets software developers detect and prevent errors in their Java programs. This framework is going to be a part of Java 8, as it is represented by JSR 308. For more information, http://types.cs.washington.edu/checker-framework/.
3
It is planned to be released sometime in 2012.
4
See the next section to learn how to install it.
5
We will publish a paper about this.
6
http://types.cs.washington.edu/checker-framework/current/checkers-manual.html\#type-inference-tools
7
@Owner can never be provided in the code, it is inferred from the context automatically.
8
See the section (cf. Section 3.1020Annotation-Polymorphic Methodssubsection.3.10) for more detail
9
Taken from: Loci: Simple Thread-Locality for Java. Wrigstad et. al. 2009
10
Parts of this subsection are taken from: http://types.cs.washington.edu/checker-framework/current/checkers-manual.html\#installation
11
from Java 8 and up, please see the JSR308 http://types.cs.washington.edu/jsr308/
12
The plugin was contributed by Adam Warski to the Checker framework team, and I forked it to suit Loci’s need.
13
Taken from: http://types.cs.washington.edu/checker-framework/current/checkers-manual.html\#running
14
If you read @Shared like (at Shared) then you have to say “an @Shared”, but if you read it like (Shared) only, then you have to say “a @Shared”. In this manual, we considered the latter.
15
More info can be found at http://types.cs.washington.edu/checker-framework/current/checkers-manual.html\#backward-compatibility
16
Please refer to this page, for more information: http://types.cs.washington.edu/checker-framework/current/checkers-manual.html\#implicit-import-statements
17
In this manual we call them “flexible” classes.
18
Loci rejects a program, which implements two interfaces having a method with the same signature and different thread localities.
19
Assume @Shared class A and that we allow @Local A[] f. Now store f in a @Local Object and then downcast it to an @Local Object[] f2, all legal operations. Now, there is no way of telling whether the elements of f2 are shared or thread-local, since there is no thread-locality information for objects at run-time. An alternative design would be to use special annotations for arrays but this departs from standard Java subtyping—@Shared Object would not be the supertype of all shared objects, etc.—which would break many patterns in existing code.
20
Even though instances of Foo will always be thread-local!
21
This annotation is only allowed on method type variables
22
Indeed, @X is equivalent to @X(1), but it differs from @X(2) or any other number.
23
By default, Loci does not warn for upcasting, to activate this warning, you need to provide “Upcast” lint option, see Section 2.39Supported Lint Optionssubsection.2.3.
24
See Section 3.516Arrayssubsection.3.5
25
For reporting bugs, please see Section 4.331How to Report Bugs?subsection.4.3.
26
Please see this bug report:
http://code.google.com/p/checker-framework/issues/detail?id=93
27
http://types.cs.washington.edu/checker-framework/
28
http://www.warski.org/
29
http://www.wrigstad.com

This document was translated from LATEX by HEVEA.