immediate execution of the entry’s body if the guard evaluates to [true]{}, or in spin-looping until eventually the guard evaluates to [true]{}. We call such a spin loop [*sync loop*]{}.

[Read-Modify-Write Synchronization]{}

For [concurrent]{} objects with read-modify-write variables the attributes proposed in Section \[aspects\] apply. All operations of [concurrent]{} objects can be executed in parallel. Read-modify-write variables have to be used for synchronizing the executing operations. The guards of entries have to be of the form [X = X’OLD]{} where [X]{} denotes a read-modify-write variable of the [concurrent]{} object. The attribute [OLD]{} is well-known from postconditions. An example in our context can be found in Listing \[lfsada\].

If during the execution of an entry a read-modify-write operation is reached, that operation might succeed immediately, in which case execution proceeds after the operation in the normal way. If the operation fails, the whole execution of the entry is restarted ([*implicit sync loop*]{}). In particular, only the statements being data-dependent on the read-modify-write variable are re-executed. Statements not being data-dependent on the read-modify-write variables are executed only on the first try.[^2] Precluding non-data-dependent statements from re-execution is not only a matter of efficiency, it sometimes makes sense semantically, e.g., for adding heap 