OshaJava is a system of annotations to specify what methods in a Java program are allowed to communicate via shared memory when run in separate threads, and a runtime that dynamically checks conformance to the specification, throwing an exception if the specification is violated. Inter-thread code communication (when a value written in some method in one thread is later read in another method in a different thread) is typically implicit and programmers have no direct way to check or control it. OshaJava makes such code communication explicit and lets a programmer check that only the communication they expect actually occurs at run time. It is complementary to many data-centric approaches for preventing or detecting synchronization errors in shared memory, such as race detection, atomicity checking, or sharing specifications.
Our OOPSLA 2010 paper Composable Specifications for Structured Shared-Memory Communication describes the specification and checking system in detail and evaluates our OshaJava implementation. Some improvements have been made to the tool since the paper was published.
Download the latest stable version at http://bitbucket.org/bpw/oshajava/overview or check out a copy of the code (tip is usually stable here).
ant; source setup.sh
- Compile programs:
- Run with checking:
oshajava [oshajava options] [-javaOptions [java options]] -- Program [program args]
- For more detail on using the OshaJava tools, see Tools.
- For an explanation of how to write OshaJava specs, see Specifications.
- For formal discussion of the specification and checking system, see our OOPSLA 2010 paper, Composable Specifications for Structured Shared-Memory Communication.
The OshaJava implementation was developed by Benjamin P. Wood and Adrian Sampson as part of the Organized Sharing research project with Luis Ceze and Dan Grossman in the Sampa research group at the University of Washington.
All code in the OshaJava distribution is licensed under the New BSD License. See the distribution for the license text.
- Everything except the
libsdirectory comprises the core OshaJava distribution and is licensed under the New BSD License.
- The OshaJava distribution includes two third-party libraries (licensed under the New BSD License) in the
libsdirectory. To avoid instrumentation reentrancy issues in user programs that also use these utilities, OshaJava includes renamed versions of these libraries with package names prefixed