|M.Sc Student||Polyakov Sergey|
|Subject||Researching the Java Memory Model|
|Department||Department of Electrical Engineering||Supervisors||Professor Yoram Moses|
|Professor Assaf Schuster|
This thesis researches the shared memory model provided by the Java Virtual Machine (JVM). A non-operational characterization of the Java Memory Model is developed. It is proved that the non-operational model is precisely equivalent to the original, operational definition, as given in the Java Language Specification. In addition, complexity of verifying JVM memory implementation is analyzed.
The definition of the memory mechanism of Java, given by Sun Microsystems in The Java Language Specification, relies on a specific abstract machine. An equivalent non-operational definition, developed in this thesis, doesn't rely on the abstract machine. The definition is based on the concept of serialization, a sequence containing all the operations in the execution. The goals achieved by building a non-operational definition are (1) compatibility with the future release of JMM, which is planned to be formalized in non-operational form, (2) verification and compliance checking of the large volume of existing multithreaded Java code.
The thesis studies whether the non-operational model makes it possible to check the Java system from the high level view (by collecting sequences of shared memory accesses and analyzing them for compliance with Java memory requirements). In this analysis the simplified non-operational definition of the Java memory model is used intentionally for the purpose of clarifying if the ``kernel'' of JMM is suitable for efficient verification. The verification problem is proved to be NP-complete in the general case, as well as in some private cases in which the number of variables, the number of operations per sequence, and the number of writes per variable are restricted.