Hints

Hints and Pitfalls

• Logging

  Please don't use System.out.println(); or e.printStackTrace();. Instead, use the java.util.logging.Logger class like so:

  public class MyClassThatWantsToLogSomething {
      private static final Logger LOGGER =
          Logger.getLogger(MyClassThatWantsToLogSomething.class.getCanonicalName());
  
      public void foo() {
          LOGGER.log(Level.INFO, message);
      }
  
      public void bar() {
          try {
              // ...
          } catch (MyException e) {
              LOGGER.log(Level.SEVERE, message, e);
          }
      }
  }
  

  Entering the canonical class name makes sure that the source of the log messages can easily be determined.

  Please choose sensible log levels.

  If the log message was caused by an exception, please always include it in the log message.

  Using a logger makes it easier to process the log messages. For example, only log messages that are logged with the logger can be displayed by the aprove.gui Eclipse Plug-in.

• System.exit

  Please, don't use System.exit directly. The reason for this is, that if AProVE is executed as an Eclipse Plug-in, calling System.exit causes the IDE to be killed.

  Instead, throw a KillAproveException and make sure that it is propagated back to the main method. There, we can be sure that AProVE is not executed as an Eclipse Plug-in and thus it is fine to indirectly calling System.exit:

      public static void main(String[] args) {
          try {
              doMain(args);
          } catch (KillAproveException e) {
              e.runSystemExit();
          }
      }
  

  The KillAproveException is a checked exception to enable easy propagation to the main method. However, this also means that it is catched by Exception and Throwable. Thus, to ensure proper termination, be sure to catch and rethrow the KillAproveException before Exception and Throwable is catched:

          try {
              // throws KillAproveException and Exception/Throwable
          } catch (KillAproveException e) {
              throw e;
          } catch (Exception e) {
              // handle e
          } catch (Throwable t) {
              // handle t
          }
  

• Throughout the AProVE project, the hierarchies java.util.Collection and java.util.Map are used a lot. If you are not yet familiar with them, take an hour or so to browse the corresponding API documentation and to get a feeling for the capabilities of these classes. This time will be time well-spent.

  • You might also want to check out the class CollectionMap (in aprove.verification.oldframework.Utility)

• If you are not sure which of the many Sets (or Maps) you should be using, in most cases a LinkedHashSet (or LinkedHashMap, respectively) is a good idea. Beware of the temptation to use a mere HashSet/HashMap! In most cases, the speed improvement is negligible. However, if the equals()/hashCode() methods of the contained objects has not been overridden and if one then iterates over your HashSet/HashMap, the order in which the elements are returned will vary from run to run! This is not a bug, but rather caused by the implementation of Object.hashCode(), which typically returns a somehow random number for each object (which usually changes between runs). Nonetheless, this behavior has already consumed many hours of precious debugging time for many AProVE developers. This issue does not occur for LinkedHashSets/LinkedHashMaps, where by default iteration takes place by order of insertion.

• AProVE Processors must be fully reentrant, i.e., they must not have any attributes that are dependent on the input obligation. The reason is that a single Processor object may be used by multiple threads. The rationale for this was to avoid creating multiple objects by reflection which nonetheless all would store the same (input-independent) parameters.

• If you would like to know who is responsible for a special line of code you can use "git blame" (also try git gui blame).

• When using several steps to build Strings to be returned (e.g. when creating a proof for a processor), you are advised not to use the + operator for String concatenation because Strings are immutable and the intermediate String objects will then be thrown away. If you need synchronized access to the String under construction (usually this is not the case), use a StringBuffer to build the String, otherwise use the StringBuilder class (recommended).

  • Ok (the resulting String is actually needed, here as the return value): return this.foo + " " + this.bar();

  • Not ok (the loop creates a lot of intermediate String objects that are thrown away in the next loop iteration; this is not optimised away by the Java Compiler, at least for Java 8):

public static String cat(Collection<String> xs) {
  String res = "";
  for (String x : xs) {
    res = res + x;
  }
  return res;
}

• • Better (uses the mutable StringBuilder class to build Strings step by step):

public static String cat(Collection<String> xs) {
  StringBuilder res = new StringBuilder();
  for (String x : xs) {
    res = res.append(x);
  }
  return res.toString();
}

• Similarly, do not use the class Vector, but the class ArrayList, which is the non-synchronized "successor" of Vector, unless you need synchronized access, of course. Iteration over an ArrayList is 4 times faster than over a Vector!

• If you need both keys and values of a map when iterating, iterate over its entry set instead of iterating over its key set and using key.get(...).

• If you need a mapping with efficient functionality in both directions use aprove.verification.oldframework.Utility.BidirectionalMap. The internal representation uses two LinkedHashMaps so if you need some other implementation feel free to extend the 'BidirectionalMap' framework. Be aware that not all functionality of maps is ported because it is not yet needed. But feel again free to extend it.

• When you create a new array based collection or map (e.g. HashSet, ArrayList, HashMap, ...), make sure that you pass a suitable initial size to the constructor if you know in advance how many elements are going to be stored in the collection/map. Like this, you can avoid unnecessary waste of clock cycles for System.arrayCopy(...), which is performed for resizing the array. So: write List<Foo> bar = new ArrayList<Foo>(42); instead of List<Foo> bar = new ArrayList<Foo>(); if you already know that you are going to add exactly 42 elements to bar.

• Use generic code whenever possible. E.g., instead of having a comparable class Bar implement Comparable, have it implement Comparable<Bar>. In this case, your compare method won't have to deal with non-Bar objects.

• Make your method signature as general as (sensibly!) possible. E.g., write void foo(Set<Bar> baz) instead of void foo(HashSet<Bar> baz) if you do not have really good reasons to insist on a HashSet in this case. Of course, writing void foo(Object baz) is unlikely to be a good idea if you intend to use methods like baz.contains(myBar).

• To a (slightly) lesser extent, this also applies to the types of fields of classes. It can be a good idea to make a field have an interface or an abstract class as static type if you think that there are several classes that might be suitable dynamic types for the attributes (see also the hint regarding method signatures). E.g., writing private Set<Foo> bar; in lieu of private LinkedHashSet<Foo> bar; is likely to be a good idea unless you want to insist on the reduced flexibility entailed by making all possible instances of the field bar extensions of LinkedHashSet.

• In case of non-trivial classes, it is often a good idea to make the constructors private and use a public static Foo create(Bar param) method instead of a constructor public Foo(Bar param). Constructors are not really flexible regarding calls of one constructor to another, so public static create methods, which can (but do not have to!) make use of the private constructors, are often a better choice.

• Although auto strategies have the name aprove.Auto, they are stored in aprove.predefinedstrategies.Auto.

• The built-in arrays in Java behave differently than other collections. E.g. the int hashCode() and boolean equals(Object) method do not reflect the contents of the array. Two arrays are in general only equal and have the same hashcode if they are the same object. For taking the contents into account one should use java.util.Arrays.hashCode(someArray) and java.util.Arrays.equals(someArray, anotherArray)

Threading Pitfalls

Abortions and synchronized sections

If you modify a data structure visible to other threads, which is not thread-safe by itself, you have to encapsulate every (read- and write) access to the modified data structure with a synchronized block (or method, in the following paragraphs, the term synchronized block refers to both). However, there are some pitfalls to this technique.

• Every synchronized block protecting the above data structure must use the same monitor object. In many cases, there is some obvious encapsulating object which can be used ("this"), but if the data structure is referenced (and accessed) from multiple objects, you need a dedicated locking object. If the data structure is a collection, have a look at the synchronized*() methods in java.utils.Collections.

• Synchronized blocks should be short, because holding a lock may block other threads.

• You must ensure that there is always a consistent state when a synchronized block is left. This is easy for the regular return case, but care must be taken if the synchronized block is left via a (runtime) exception. This may happen especially if a helper method throws an AbortionMethod, but other cases (Assertions, NullpointerExceptions, ...) will happen too. To do this, it may be useful to change fields as follows

tmp = new List();
expensiveOrAbortableFillOfList(tmp);
field = tmp;

instead of

field = new List();
expensiveOrAbortableFillOfList(tmp);

The latter form has also the advantage, that you can make field a unmodifiable (or unmutable) list.

Lazy initialization

• If you use the following construct

private volatile ExpensiveObject expensiveObject = null;

public ExpensiveObject getExpensiveObject() {
  if (this.expensiveObject == null) {
    synchronized(this) {
      if (this.expensiveObject == null) {
        this.expensiveObject = ExpensiveObject.create();
      }
    }
  }
  return this.expensiveObject;
}

make sure your object is declared volatile. Without this modifier, no memory synchronization is done and other threads may see ExpensiveObject in an inconsistent state. Explaining all the reasons here would take too much room, so see why double-checked locking is broken.

• When one thread waits for another, the constructs used must be variations of:

synchronized(foo) {
  foo.setBlah(true);
  foo.notify();
}

and

synchronized(foo) {
  while(! foo.isBlah()) {
    foo.wait();
  }
}

If you put the synchronized() inside the while or after the setBlah, you risk a race condition where notify() is called before wait() is entered. Also, you always need a while loop, not a plain if, because as per java spec, wait() may wake up spontaneously for "no reason".

• So what is this pesky InterruptedException all about? What's Thread.interrupt() do anyway?
  • Well, interrupts are java's "friendly" way of asking a thread to finish. Basically, an interrupt is just a boolean field in a thread.
  • Calling t.interrupt() on a thread sets the field to true. When the field is/becomes true, wait() will throw an InterruptedException, and some IO methods may throw an InterruptedIOException.
  • So this exception is an indication that someone wants you to stop.
  • You can also explicitly check for interruptedness of your own thread with Thread.interrupted()
  • Note that both the exception and Thread.interrupted() re-set the interrupted field to false.

This means that the "good" way of dealing with InterruptedException is:

try {
  Thread.sleep(5000);
} catch (InterruptedException someoneWantsUsToStop) {
  myExecutor.abort(); // Stop my stuff
  Thread.currentThread().interrupt(); // Re-set interrupted flag
  return;
}