Def. The "immediate sub-objects" of an object o (as seen by a thread T at some point in its execution p) are any objects referred to by a reference field f of o (as could be seen by T at p). Def. The "sub-objects" of an object o (as seen by a thread T at some point in its execution p) are o itself, o's immediate sub-objects (as could be seen by T at p), and any objects referred to by a reference field f of a sub-object of o (as could be seen by T at p). Def. Suppose thread T creates object o; o is "made accessible" to Thread V when T first assigns a reference to o to a variable that represents a field or element of some object p that is already accessible to V. If a reference to o is assigned to a field or element of an object q that is not accessible to V, o becomes accessible to V when q becomes accessible to V (assuming o has not been made accessible to V already). When a Thread is created are already accessible to it. Static fields are considered to be a part of the relevant Class object, which is considered accessible to all threads (modulo class loader issues). Def. An Object is said to be "monogamous" if none of its fields are modified by any thread other than the one that invoked its constructor. (Less formally: nobody messes with a monogamous object other than the thread that creates it.) Def. A monogamous object is further said to be "superficially stable" if none of its fields or elements are modified (by its creator) after it is made accessible to another thread (by its creator). (Less formally: nobody messes with a superficially stable object once it's made accessible to other threads.) Def. A superficially stable object is said to be "stable" if all of its sub-objects, as seen by its creator immediately before it is first made available to another thread, are superficially stable. (Less formally: nobody messes with any object reachable from a stable object once the former object is made accessible to other threads.) (To a first approximation, immutable objects are stable, though it takes a slightly forced definition of immutable to imply this, given the current definition of stability.) Def. An object o that is accessible to a thread T at some point p in T's execution is said to be "superficially well-defined" to T at p if there is a unique value that T may observe for any field or element f of o at p that is allowable under the memory consistency model. Def. An object o is said to be "everywhere superficially well-defined" if it is well-defined at every thread T and "execution point" p at which o could be accessible to T over the life of the VM. Def. An object o that is accessible to a thread T at some point p in T's execution is said to be "well-defined" to T at p if all of o's sub-objects (as could be seen by T at p) are superficially well-defined at T. Def. An object o is said to be "everywhere well-defined" if it is well- defined at every thread T and "execution point" p at which o could be accessible to T over the life of the VM. Theorem 1. Superficially Stable objects are everywhere superficially well-defined. Proof: Suppose o is a superficially stable object created by thread C, accessible to some thread T != C at some point p in T's execution. Suppose T performs a use action U that accesses some field or element f of o. Since T did not create o, we know that T performed a load action that returned a reference r to o. Let A be the first such load action, and let action P be the corresponding read by the main memory. Similarly, we know that T performed a load action on the variable representing f, at some time preceding U. Let us call the last such load action B, and the corresponding read action Q. Then Q (which returns T's view of f at p) must, by Rule 2, follows P (which returns r). Since o is superficially stable, none of its fields or elements were modified after C's first assign action that made o accessible to some other thread. Because T was able to load r, we know that C performed an assign action and a subsequent store action of the value r on some variable v representing a field of some object accessible to another thread Q (unequal to C but possibly equal to T). Let us call the first such assign action D, the first such store action S, and the corresponding write action W. (W can be thought of as the first "publication" of o to threads other than C.) Then P must follow W (though they do not necessarily apply to the same variable). Because o is superficially stable, no assign actions on f are performed by any thread other than C, and C performs no assign actions on f after D. Let us call C's last assign action on f prior to S (which is, in fact, C's final assign action on f) G. By rule 1, a store action on f must intervene between G and S, and the corresponding write action X (which writes the "correct value" of f) must precede W (the store action corresponding to S). Since W follows X, P follows W and Q follows P, Q (which returns T's view of f at p) follows X, hence T reads the correct value of f. Since f can be any field or element of o, o is superficially well-defined to T at p. Since we made no assumptions about T and p (other than T != C), o is everywhere superficially well-defined. Theorem 2. Stable objects are everywhere well-defined. Proof: Suppose o is a stable object created by thread C, accessible to some thread T != C at some point p in T's execution. Then o is superficially stable. By theorem 1, o is superficially well-defined, so T sees the "correct value" for all of o's reference fields (i.e., T's notion of o's immediate sub-objects at p matches C's notion of same, immediately before o was first made available to another thread). By the definition of stability, all of these immediate sub-objects are, themselves, superficially stable. By induction, all sub-objects of o as seen by T at p are superficially well-defined, thus o is superficially well-defined to T at p. Since we made no assumptions about T and p (other than T != C), o is everywhere well-defined. Theorem 2 is sufficient to prove the correctness of both of the idioms whose lack of correctness under the current memory model spurred this whole endeavor.