Clone wiki

oshajava / Tools

OshaJava Tools

This page describes how to use the OshaJava tools. See also how to write Specifications.

Build

To build, run ant in the top-level directory then, in any shell where you want to use the OshaJava tools, source the setup.sh file to set up a few environment variables and put the four OshaJava tools on your PATH.

Compile Annotated Programs

With build/oshajava.jar on the classpath, compile all files in your project:

javac -cp .:path/to/distribution/build/oshajava.jar *.java

Alternately, once you've sourced setup.sh, you have an oshajavac utility available on your PATH. Usage is identical to javac, but without needing to add oshajava.jar to the classpath.

oshajavac *.java

Note: The OshaJava annotation processor will only see annotation in files that are explicitly passed as arguments to the javac compiler. Implicit dependencies will not be subject to annotation processing.

In addition to generating the usual .class files, the OshaJava compilation stage reads your annotations and generates several .om{i,m,s} files next to the .class files. These OshaJava files hold information needed by the oshajava runtime to check that executions of your program conform to the specification expressed by your annotations. The runtime will warn you if some of these files are missing.

Compilation Options

  • -Aoshajava.annotation.default=inline: By default, all methods that are not annotated (directly or indirectly) with a communication specification receive the @NonComm annotation, meaning they are not allowed to communicate at all. This option allows you to set this program-wide default to either inline or noncomm.
  • -Aoshajava.verbose: Print extra debugging information in the compiler.

Examine Compiled Specifications

The oshamodpp tool lets you pretty print compiled module specifications on disk. Usage:

oshamodpp Module.oms

The tool works on .oms files (compiled module specs), .omi files (incremental storage of module specs for multistage compilation), .omm files (these map every method in a class to the module to which it belongs), and any other file that happens to be a single serialized Java object.

Clean Compiled Specification Files

The oshamodrm tool deletes all .om{i,m,s} files in the directory hierarchies rooted at its arguments. Given no argument it deletes all such files under the current directory.

Run Programs with Communication Checking Enabled

All of the instrumentation performed by OshaJava to track and check communication in a program is done by a bytecode instrumentor that runs at class-load time in the JVM. The OshaJava annotation processor does not transform your program in any way, meaning you can compile your program once with the OshaJava annotation processor enabled and then run it normally with java or with communication checking enabled with oshajava.

To run your program with specification checking enabled, use oshajava:

oshajava [oshajava options] [-javaOptions [java options]] -- Program [program args]

For a complete list of runtime options, run oshajava -help.

Updated