Most definitions of weak consistency models (WCM) in the literature are specific to one style of semantics description (e.g. transition systems), one language (e.g. x86 assembly), and one computer architecture (e.g. ARM). This makes generality a difficult goal: each verification, static analysis, or transformation technique has to be reinvented if any of these three parameters changes.

In contrast, our work provides a wide variety of semantics definitions, all under the same framework. More precisely, we view the semantics of a parallel program P under a WCM as two-fold:

• a computation part, i.e., an architecture and language independent instruction semantics;

• a communication part, i.e., a set of constraints on communications.

More precisely a WCM is the intersection (in the formal sense) of its computation and communication parts. Its computation part is said to be anarchic since it imposes no constraint on communications. To describe its communication part, we choose to use the cat domain specific language, which allows a user to list a set of constraints on communication in a concise manner.

We define a hierarchy of computation semantics from ground valued to (un)interpreted symbolic execution, from interleaved to true parallelism, from event to state-based, from trace to transition-based, etc. Each level of the hierarchy is an abstraction of the bottom computation semantics.

Although the abstractions in the hierarchy do lose information in general (for example w.r.t. program termination), they do not loose any information w.r.t. the bottom semantics. Moreover, all the abstractions preserve the cat specification of communications, viz. a given cat specification forbids exactly the same behaviours on any two abstractions.

This allows us to provide a wide variety of semantics definitions: each and every computation semantics (whether state-based or not, trace-based or not) can be married to any communication semantics as described by a cat specification. Thus we can provide, for example, two (or more) definitions of TSO, Power, or ARM, adjusted to the taste of the user, or the practicality w.r.t. verification techniques.