engleski

Formalization of the Java Memory Model

The goal of this thesis is to give a mathematically precise specification of the Java memory model and discuss its interpretation in the ASM context. We have refactored the original specification in order to clearly stipulate how it conditions the behavior of the environment. We show how each thread in a multithreaded Java program can be seen as an ordinary interactive small-step algorithm, and, consequently, how the Java program gives rise to a distributed ordinary interactive small-step ASM.

Java memory model; formalization; partial orders; ASM; DASM; complexity results for verification problem

nije evidentirano