Concutest


About Concutest
Introduction
ConcJUnit
Thread Checker
Schedule-Based Execution

Using Concutest
Download
How to Run
License

Resources
Documentation
FAQ
Publications

Give Feedback
Features, Bugs, Support
Contact Us

Developers
SourceForge Project
Developer Docs
Javadocs
Developer Blog
Mathias Ricken's Homepage

      Thread Checker Annotation Usage Instructions

The annotations we provide in the tclib.jar file allow the programmer to specify threading invariants for classes and methods. The library includes both a wide array of built-in annotations to express common invariants, as well as a way to combine existing ones using Boolean operations, and create completely user-written annotations.


Usage Examples

Using annotations to specify the threading invariants of a method is easy: Just place the annotation in front of the method, or to affect all methods introduced in a class, in front of the class (for more information about this, see Invariant Inheritance).

For example, to specify that the method foo() may only be run by the AWT/Swing event thread, use the @OnlyEventThread annotation. This is an annotation that does not require any parameters, so all that is necessary is to write the following:

@OnlyEventThread
void foo() {
    // foo's code
}

A more complex invariant may involve prohibiting threads with a certain name, e.g. "bad", to run the bar() method. This requires the programmer to specify the thread name, so the @NotThreadWithName annotation takes a parameter:

@NotThreadWithName("bad")
void bar() {
    // bar's code
}

The @NotThreadWithName annotation has a more advanced form as well that interprets the thread name as regular expression. To enable this interpretation, set the regex value of the @NotThreadWithName annotation to true. In the example below, we are now passing two parameters to the annotation, so we need to specify the names to which we assign the values:

@NotThreadWithName(value="bad.*", regex=true)
void barRegex() {
    // barRegex's code
}

The second example involvong the bar() method only allowed us to omit the name of the values because we were only assigning something, the thread name, to value. The regex value has a default value of false and can therefore be omitted.

For more information on how to use annotations, please refer to the Java Language Specification, 3rd Ed, section 9.7.


Built-In Annotations

These annotations are part of the library and ready to use:

  • OnlyThreadWithName: Allows only threads to run whose thread name matches the name specified as constant.
    • OnlyThreadWithName.InField: Name contained as value in a field.
    • OnlyThreadWithName.InField.ByName: Name contained as value in a field; the class is specified by name.
    For all three annotations, there are annotations that combine several invariants into one using Boolean or: OnlyThreadWithName.Any, OnlyThreadWithName.InField.Any and OnlyThreadWithName.InField.ByName.Any.

  • OnlyThreadWithGroupName: Allows only threads to run whose group name matches the name specified as constant.
    • OnlyThreadWithGroupName.InField: Name contained as value in a field.
    • OnlyThreadWithGroupName.InField.ByName: Name contained as value in a field; the class is specified by name.
    For all three annotations, there are annotations that combine several invariants into one using Boolean or: OnlyThreadWithGroupName.Any, OnlyThreadWithGroupName.InField.Any and OnlyThreadWithGroupName.InField.ByName.Any.

  • OnlyThreadInField: Allows only thread to run whose instance is stored in the specified field.
    • OnlyThreadInField.ByName: The class is specified by name.
    For the two annotations, there are annotations that combine several invariants into one using Boolean and: OnlyThreadInField.Any and OnlyThreadInField.ByName.Any.

  • OnlyEventThread: Allows only the event thread to run.
    • OnlyEventThread.AfterRealized: Allows any thread to run until the display component has been realized; after that, only the event thread may run. This annotation may only be used in subclasses of java.awt.Component.

  • NotThreadWithName: Prohibits threads from running whose thread name matches the name specified as constant.
    • NotThreadWithName.InField: Name contained as value in a field.
    • NotThreadWithName.InField.ByName: Name contained as value in a field; the class is specified by name.
    For all three annotations, there are annotations that combine several invariants into one using Boolean and: NotThreadWithName.None, NotThreadWithName.InField.None and NotThreadWithName.InField.ByName.None.

  • NotThreadWithGroupName: Prohibits threads from running whose group name matches the name specified as constant.
    • NotThreadWithGroupName.InField: Name contained as value in a field.
    • NotThreadWithGroupName.InField.ByName: Name contained as value in a field; the class is specified by name.
    For all three annotations, there are annotations that combine several invariants into one using Boolean and: NotThreadWithGroupName.None, NotThreadWithGroupName.InField.None and NotThreadWithGroupName.InField.ByName.None.

  • NotThreadInField: Prohibits the thread from running whose instance is stored in the specified field.
    • NotThreadInField.ByName: The class is specified by name.
    For the two annotations, there are annotations that combine several invariants into one using Boolean and: NotThreadInField.None and NotThreadInField.ByName.None.

  • NotEventThread: Prohibits the event thread from running.

For more detailed information, please refer to the tclib.jar javadoc for the annotations.


User-Written Annotations

There are two forms of user-written annotations: @PredicateLink-style annotations and @Combine-style annotations. The former link an annotation interface to a predicate, a Java method returning boolean. The latter combine existing annotations using the Boolean operations and, or, and not. Both @PredicateLink and @Combine are "meta-annotations", i.e. they are annotations that are applied to other annotations.

User-Written @PredicateLink-Style Annotations

User-Written @PredicateLink-style annotations consist of two parts: An annotation interface definition, containing the information necessary to specify the invariant, and a Java method returning boolean to evaluate whether the invariant has been met. The annotation interface itself is annotated with the @PredicateLink meta-annotation, which establishes a link to the Java method by providing the class object and the name of the method. The method name can be omitted, in which case the name "check" is assumed.

Below is an annotation interface definition that contains an int and an array of String:

@PredicateLink(value=MyPredicate.class, method="check")
@interface MyPredicate {
    int i;
    String[] sarr;
}

Since the method name can be omitted, which makes it default to "check", the first line of the example above could also have been written in the following, simpler way:

@PredicateLink(MyPredicate.class)
...

The @PredicateLink meta-annotation specifies that a method called "check" in the MyPredicate class will evaluate whether the invariant specified by an instance of this annotation has been met. This method has to meet several criteria:

  • It has to be accessible from anywhere, which implies that the method and all its enclosing classes have to be public and static.
  • It has to return boolean.
  • If the annotation that links to the method has n value members, the method has to have n+1 parameters:
    1. The first parameter has to be of type Object; the variable name can be chosen arbitrarily (with some limitations due to the rules below). This parameter is used to pass the value of this if the method being called is non-static; if the method is static, null is passed.
    2. For each value member of the annotation, the method must have one parameter with the same type and name as the value member. This way, the information about the invariant can be passed to the method. The order of these parameters is not important.

Below is an example of a MyPredicate class with a "check" method that suits the requirements:

public class MyPredicate {
    public static boolean check(Object thisO, int i, String[] sarr) {
        return (i<sarr.length) && (sarr[i].length()>0);
    }
}

This predicate returns true if and only if the value of i is a valid index in the string array sarr, and the entry sarr[i] is non-empty. I can't imagine when a predicate like this could be useful, but it demonstrates the power of user-written predicates.

The annotation can now be used just like in the examples above:

@MyPredicate(i=2, sarr={"a", "b", "c", "d"})
void fum() {
    // fum's code
}

It is worth noting that the value members of @PredicateLink-style annotations may not be annotations or arrays of annotations; those are reserved for @Combine-style annotations described below.

User-Written @Combine-Style Annotations

@Combine-style annotations were developed to increase code-reuse. In theory, once a small set of basic invariants has been developed, more complex invariants could be developed by combining existing ones. Unfortunately, the Java grammar makes this very difficult. It isn't even possible to specify the @NotThreadWithName annotation twice to exclude two threads from execution. The following code is not legal Java:

@NotThreadWithName("bad")
@NotThreadWithName("worse") // error, specified @NotThreadWithName twice
void fum() {
    // fum's code
}

More details to come.


More Examples

Many examples can be found in the sample programs linked to the tcrt.jar Javadoc.


Invariant Inheritance

The invariants specified for a method are inherited to overriding methods in subclasses. More details to come.


Concutest is partially funded by the National Science Foundation and the Texas Advanced Technology Program.
Copyright © 2004-2010 by Mathias Ricken. All rights reserved.
Support This Project