of a non-blocking stack using our proposed new syntax for [concurrent]{} objects. Implementation of entry [Push]{} (lines \[lfs:pushb\]–\[lfs:pushe\]) behaves as follows. In Line \[lfs:newb\] a new element is inserted at the head of the list. Pointer [Next]{} of this element is set to the current head. The next statement (Line \[lfs:rmwo\]) assigns the new value to the head of the list. Since variable [Head]{} has aspect [Read\_Modify\_Write]{} (line \[lfs:rmw\]), this is done with RMW semantics, i.e., if the value of [Head]{} has not been changed (since the execution of [Push]{} has started) by a different thread executing [Push]{} or [Pop]{} (i.e., [Head = Head’OLD]{}), then the RMW operation succeeds and execution proceeds at Line \[lfs:pushe\], i.e., [Push]{} returns. If the value of [Head]{} has been changed ([Head /= Head’OLD]{}), then the RMW operation fails and entry [Push]{} is re-executed starting from Line \[lfs:newb\]. Line \[lfs:new\] is not re-executed as it is not data dependent on [Head]{}.

Several memory order attributes apply to the RMW operation (Line \[lfs:rmwo\]) which are given in lines \[lfs:mmb\]–\[lfs:mme\]: In case of a successful execution of the RMW, the value of [Head]{} is released such that other threads can read its value via memory order acquire. 