I am referring to the formal definition of C++11 memory model (Mark Batty et al.), which includes atomics, locks, relaxed memory models, but no formal definition on the behavior of condition variables. Similarly in Java Memory Model, there also is no definition on the wait() and notify() mechanisms. Why is that?
Similarly in Java Memory Model, there also is no definition on the wait() and notify() mechanisms. Why is that?
Because it is a memory model. It models / specifies the behavior of memory read and memory write operations in a multi-threaded application.
Aspects of the behavior of wait() and notify() are (in a sense) emergent from the memory model. Calls to wait() and notify() must be with primitive mutexes. That means that lock and unlock actions occur at specific points, and (in the case of wait()) they are specified as doing unlock and lock actions under certain circumstances. Those actions are modeled in the memory model ... and this makes the emergent semantics of condition variables sound, provided that you stick with the recommended patterns for implementing them.
Other aspects of the wait() and notify() are specified in the JLS. It is in the same chapter as the Memory Model. But a different section. 17.2 rather than 17.4. The rest of the behavior is defined in the javadoc.