Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and developing multiprocessor programs. In order to promote understanding and enable automated verification, it is highly desirable that a memory model specification be both declarative and executable. We present a specification framework called Nemos (Nonoperational yet Executable Memory Ordering Specifications), which supports precise specification and automatic execution in the same framework. We employ a uniform notation based on predicate logic to define shared memory semantics in an axiomatic as well as compositional style. We also apply constraint logic programming and SAT solving to make the axiomatic speci.cations executable for memory model analysis. To illustrate our approach, this paper formalizes a collection of classical memory models, including sequential consistency, coherence, PRAM, causal consistency, and processor consistency.