used in the implementation of the [concurrent]{} object’s operations (functions, procedures, and entries) are employed for specifying behavior according to the memory model. Variables are labeled by the boolean aspect [[Synchronized]{}]{}.

Read accesses to [synchronized]{} variables in the implementation of the [concurrent]{} object’s operations may be labeled with the attribute [Concurrent\_Read]{}, write accesses with the attribute [Concurrent\_Write]{}. Both attributes have a parameter [Memory\_Order]{} to specify the memory order of the access. (If the operations are not labeled, the default values given below apply.) In case of read accesses, values allowed for parameter [Memory\_Order]{} are [Sequentially\_Consistent]{}, [Acquire]{}, and [Relaxed]{}. The default value is [Sequentially\_Consistent]{}. For write accesses the values allowed are [Sequentially\_Consistent]{}, [Release]{}, and [Relaxed]{}. The default value is again [Sequentially\_Consistent]{}.

For example, assigning the value of [synchronized]{} variable [Y]{} to [synchronized]{} variable [X]{} is given like In addition we propose aspects for specifying variable specific default values for the attributes described above. In more detail, when declaring [synchronized]{} variables the default values for read and write accesses can be specified via aspects [Memory\_Order\_Read]{} and [Memory\_Order\_Write]{}. The allowed values are the same as those given above for read and write accesses. If these memory model aspects are given when declaring a 