One of the most prevalent GUI-related bugs is invalid UI update or invalid thread access: accessing the UI directly from a background thread.
Most GUI frameworks (including Android, AWT, Swing, and SWT) create a single distinguished thread — the UI event thread — that handles all GUI events and updates. To keep the interface responsive, any expensive computation should be offloaded to background threads (also called worker threads). If a background thread accesses a UI element such as a JPanel (by calling a JPanel method or reading/writing a field of JPanel), the GUI framework raises an exception that terminates the program. To fix the bug, the background thread should send a request to the UI thread to perform the access on its behalf.
It is difficult for a programmer to remember which methods may be called on which thread(s). The GUI Effect Checker solves this problem. The programmer annotates each method to indicate whether:
• It accesses no UI elements (and may run on any thread); such a method is said to have the “safe effect”.
• It may access UI elements (and must run on the UI thread); such a method is said to have the “UI effect”.
The GUI Effect Checker verifies these effects and statically enforces that UI methods are only called from the correct thread. A method with the safe effect is prohibited from calling a method with the UI effect.
For example, the effect system can reason about when method calls must be dispatched to the UI thread via a message such as Display.syncExec.
@SafeEffect
public void calledFromBackgroundThreads(JLabel l) {
l.setText("Foo"); // Error: calling a @UIEffect method from a @SafeEffect method
Display.syncExec(new Runnable() {
@UIEffect // inferred by default
public void run() {
l.setText("Bar"); // OK: accessing JLabel from code run on the UI thread
}
});
}
The GUI Effect Checker’s annotations fall into three categories:
• effect annotations on methods (Section 19.1),
• class or package annotations controlling the default effect (Section 19.4), and
• effect-polymorphism: code that works for both the safe effect and the UI effect (Section 19.5).
There are two primary GUI effect annotations:
@SafeEffectis a method annotation marking code that must not access UI objects.
@UIEffect
is a method annotation marking code that may access UI objects. Most UI object methods (e.g., methods of JPanel) are annotated as @UIEffect.
@SafeEffect is a sub-effect of @UIEffect, in that it is always safe to call a @SafeEffect method anywhere it is permitted to call a @UIEffect method. We write this relationship as
@SafeEffect ≺ @UIEffect
The GUI Effect Checker ensures that only the UI thread accesses UI objects. This prevents GUI errors such as invalid UI update and invalid thread access.
The GUI Effect Checker issues errors in the following cases:
• A @UIEffect method is invoked by a @SafeEffect method.
• Method declarations violate subtyping restrictions: a supertype declares a @SafeEffect method, and a subtype annotates an overriding version as @UIEffect.
Additionally, if a method implements or overrides a method in two supertypes (two interfaces, or an interface and parent class), and those supertypes give different effects for the methods, the GUI Effect Checker issues a warning (not an error).
The GUI Effect Checker can be invoked by running the following command:
javac -processor org.checkerframework.checker.guieffect.GuiEffectChecker MyFile.java ...
The default method annotation is @SafeEffect, since most code in most programs is not related to the UI. This also means that typically, code that is unrelated to the UI need not be annotated at all.
The GUI Effect Checker provides three primary ways to change the default method effect for a class or package:
@UIType
is a class annotation that makes the effect for unannotated methods in that class default to @UIEffect. (See also @UI in Section 19.5.2.)
@UIPackage
is a package annotation that makes the effect for unannotated methods in that package default to @UIEffect. It is not transitive; a package nested inside a package marked @UIPackage does not inherit the changed default.
@SafeType
is a class annotation that makes the effect for unannotated methods in that class default to @SafeEffect. Because @SafeEffect is already the default effect, @SafeType is only useful for class types inside a package marked @UIPackage.
There is one other place where the default annotation is not automatically @SafeEffect: anonymous inner classes. Since anonymous inner classes exist primarily for brevity, it would be unfortunate to spoil that brevity with extra annotations. By default, an anonymous inner class method that overrides
or implements a method of the parent type inherits that method’s effect. For example, an anonymous inner class implementing an interface with method @UIEffect void m() need not explicitly annotate its implementation of m(); the implementation will inherit the parent’s effect.
Methods of the anonymous inner class that are not inherited from a parent type follow the standard defaulting rules.
Sometimes a type is reused for both UI-specific and background-thread work. A good example is the Runnable interface, which is used both for creating new background threads (in which case the run() method must have the @SafeEffect) and for sending code to the UI
thread to execute (in which case the run() method may have the @UIEffect). But the declaration of Runnable.run() may have only one effect annotation in the source code. How do we reconcile these conflicting use cases?
Effect-polymorphism permits a type to be used for both UI and non-UI purposes. It is similar to Java’s generics in that you define, then use, the effect-polymorphic type. Recall that to define a generic type, you write a type parameter such as <T> and use it in the body of the
type definition; for example, class List<T> . To instantiate a generic type, you write its name along with a type argument; for example, { ... T get() {...} ... }List<Date> myDates;.
To declare that a class is effect-polymorphic, annotate its definition with @PolyUIType. To use the effect variable in the class body, annotate a method with @PolyUIEffect. It is an error to use @PolyUIEffect in a class that is not effect-polymorphic.
Consider the following example:
@PolyUIType
public interface Runnable {
@PolyUIEffect
void run();
}
This declares that class Runnable is parameterized over one generic effect, and that when Runnable is instantiated, the effect argument will be used as the effect for the run method.
To instantiate an effect-polymorphic type, write one of these three type qualifiers before a use of the type:
@AlwaysSafe
instantiates the type’s effect to @SafeEffect.
@UI
instantiates the type’s effect to @UIEffect. Additionally, it changes the default method effect for the class to @UIEffect.
@PolyUI
instantiates the type’s effect to @PolyUIEffect for the same instantiation as the current (containing) class. For example, this is the qualifier of the receiver this inside a method of a @PolyUIType class, which is how one method of an effect-polymorphic class may call an
effect-polymorphic method of the same class.
As an example:
@AlwaysSafe Runnable s = ...; s.run(); // s.run() is @SafeEffect @PolyUI Runnable p = ...; p.run(); // p.run() is @PolyUIEffect (context-dependent) @UI Runnable u = ...; u.run(); // u.run() is @UIEffect
It is an error to apply an effect instantiation qualifier to a type that is not effect-polymorphic.
Note that no annotation is required on the anonymous class declaration itself (e.g., new Runnable(){...} does not require a type use annotation, although the variable, field, or argument it ends up being assigned to might). Instead, the GUI Effect Checker will infer the effect qualifier based on the
method being called from within the members of that specific anonymous class.
Sometimes you may wish to subclass a specific instantiation of an effect-polymorphic type, just as you may extend List<String>.
To do this, simply place the effect instantiation qualifier by the name of the type you are defining, e.g.:
@UI
public class UIRunnable extends Runnable {...}
@AlwaysSafe
public class SafeRunnable extends Runnable {...}
The GUI Effect Checker will automatically apply the qualifier to all classes and interfaces the class being defined extends or implements. (This means you cannot write a class that is a subtype of a @AlwaysSafe Foo and a @UI Bar, but this has not been a problem in our experience.)
With three effect annotations, we must extend the static sub-effecting relationship:
@SafeEffect ≺ @PolyUIEffect ≺ @UIEffect
This is the correct sub-effecting relation because it is always safe to call a @SafeEffect method (whether from an effect-polymorphic method or a UI method), and a @UIEffect method may safely call any other method.
This induces a subtyping hierarchy on type qualifiers:
@AlwaysSafe ≺ @PolyUI ≺ @UI
This is sound because a method instantiated according to any qualifier will always be safe to call in place of a method instantiated according to one of its super-qualifiers. This allows clients to pass “safer” instances of some object type to a given method.
Sometimes it is useful to have @PolyUI parameters on a method. As a trivial example, this permits us to specify an identity method that works for both @UI Runnable and @AlwaysSafe Runnable:
public @PolyUI Runnable id(@PolyUI Runnable r) {
return r;
}
This use of @PolyUI will be handled as is standard for polymorphic qualifiers in the Checker Framework (see Section 32.2).
@PolyUIEffect methods should generally not use @PolyUI arguments: it is permitted by the framework, but its interaction with inheritance is subtle, and may not behave as you would hope.
The shortest explanation is this: @PolyUI arguments may only be overridden by @PolyUI arguments, even though the implicitly @PolyUI receiver may be overridden with an @AlwaysSafe receiver.
As noted earlier (Section 32.1.6), Java’s generics are invariant — A<X> is a subtype of B<Y> only if X is identical to Y. Class-level use of
@PolyUI behaves slightly differently. Marking a type declaration @PolyUIType is conceptually equivalent to parameterizing the type by some E extends Effect. But in this view, Runnable<SafeEffect> (really @AlwaysSafe Runnable)
would be considered a subtype of Runnable<UIEffect> (really @UI Runnable), as explained earlier in this section. Java’s generics do not permit this, which is called covariant subtyping in the effect parameter. Permitting it for all generics leads to problems where a type
system can miss errors. Java solves this by making all generics invariant, which rejects more programs than strictly necessary, but leads to an easy-to-explain limitation. For this checker, covariant subtyping of effect parameters is very important: being able to pass an @AlwaysSafe Runnable in place
of a @UI Runnable is extremely useful. Since we need to allow some cases for flexibility, but need to reject other cases to avoid missing errors, the distinction is a bit more subtle for this checker.
Consider this small example (warning: the following is rejected by the GUI Effect Checker):
@PolyUIType
public interface Dispatcher {
@PolyUIEffect
void dispatch(@PolyUI Runnable toRun);
}
@SafeType
public class SafeDispatcher implements Dispatcher {
@Override
public void dispatch(@AlwaysSafe Runnable toRun) {
runOnBackgroundThread(toRun);
}
}
This may initially seem like harmless code to write, which simply specializes the implicit effect parameter from Dispatcher in the SafeDispatcher implementation. However, the way method effect polymorphism is implemented is by implicitly making the receiver of a
@PolyUIEffect method — the object on which the method is invoked — @PolyUI. So if the definitions above were permitted, the following client code would be possible:
@AlwaysSafe SafeDispatcher s = ...; @UI Runnable uitask = ...; s.dispatch(uitask);
At the call to dispatch, the Checker Framework is free to consider s as its supertype, @UI SafeDispatcher. This permits the framework to choose the same qualifier for both the (implicit) receiver use of @PolyUI and the toRun argument to
Dispatcher.dispatch, passing the checker. But this code would then pass a UI-thread-only task to a method which should only accept background thread tasks — exactly what the checker should prevent!
To resolve this, the GUI Effect Checker rejects the definitions above, specifically the @AlwaysSafe on SafeDispatcher.dispatch’s parameter, which would need to remain @PolyUI.
A subtlety of the code above is that the receiver for SafeDispatcher.dispatch is also overridden, switching from a @PolyUI receiver to an @AlwaysSafe receiver. That change is permissible. But when that is done, the polymorphic arguments may no longer be
interchangeable with the receiver.
The paper “JavaUI: Effects for controlling UI object access” [GDEG13] (ECOOP 2013, https://homes.cs.washington.edu/~mernst/pubs/gui-thread-ecoop2013-abstract.html) includes some case studies on the checker’s efficacy, including descriptions of the relatively few false warnings we encountered. It also contains a more formal description of the effect system.