The Manual of Version 0.1
Loci is a subproject of UPMARC1 umbrella project
Some parts of this document, are taken from the Checker framework’s manual:
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.
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.
Loci adds several annotations to the standard Java programming language, to let the programmer express thread locality:
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:
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
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:
There are no negative consequences to using the Type Annotations compiler, but if you choose not to do so, you have alternatives. When this document tells you to run javac, you will instead need to run one of the following commands. The command should be all on one line, and followed by javac arguments such as -processor.
To ensure that it was installed properly, run javac -version (using a variant of javac if you did not add it to your path).
The output should be:
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:
<dependencies> <!-- Loci annotation processor --> <dependency> <groupId>net.java.loci</groupId> <artifactId>loci</artifactId> <version>0.1</version> </dependency> <!-- other dependencies --> </dependencies>
<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
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:
Loci has four lint options:
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.
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:
$ 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
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:
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:
Or, provide this option to your javac statement:
Loci defines three annotations for thread-locality:
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.
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.
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
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:
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.
As mentioned previously, @Owner denotes the type holds it, to have exactly the same thread locality as the object contains it, for example:
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.
By following the same semantics of Generics in Java, we could easily forbid this. Consider the following “plain” Java code:
Cell<?> c = b; //Java loses the type information
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.
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.
In Loci, the default annotation for type casting is the annotation which can be retrieved from the expression part of the cast:
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:
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.
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:
is equivalent to the following interface, with the annotations elaborated in:
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:
but the following is not:
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.
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.
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.
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:
Now, consider the possible ways of creating arrays of instances of these classes:
If an array of a different thread-locality than its elements is required, one must use an extra level of indirection, e.g.:
However, an array of a primitive type, should still have @Local element type, regardless of the annotation on the array itself:
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:
As an illustration of point (1) above, consider the following class and variable definitions:
To illustrate point (2) above, consider the following class and variable definitions:
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,
does not compile as x.new B() is thread-local, however
is legal as C is declared as @Shared.
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:
The code example below shows that the checking is straightforward as anonymous classes are simply a syntactic shorthand.
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:
where @Owner has been made explicit for clarity. Instantiating the class, we might write:
For convenience, Loci can infer thread-locality if the annotation is missing using the following rules (order is insignificant):
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:
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.
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:
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.
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.
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):
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:
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:
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.
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:
When calling the above method, o2 and o3 must have the same annotation, while o1’s can be different.
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:
We can derive the bound on the annotation by first elaborating in the default upper class bound:
and then inserting the annotation on the class bound:
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:
As we mentioned above, the generics suffer from the same problems as arrays when downcasting, consider this example:
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.
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:
Cell<?, ?> temp = (Cell<?, ?>) obj; //It is OK
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:
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.
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.
Java’s ThreadLocal API has the following annotations:
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.,
Should be expanded to
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:
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).
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.
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:
But, if we provide the correct annotation, then Loci accepts it:
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.
Or, in this example:
Suppose we have these two classes:
As we mentioned before24, in Loci arrays should have the same annotation as its elements, consider the following:
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.
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.
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.
If you have a problem, please file a bug at
(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:
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.
This document was translated from LATEX by HEVEA.