A model of multicopy semantics of low level memory operations is made in mCRL2. These memory operations can be relaxed, release, acquire and sequentially consistent, which determine whether these operations can be executed before or after surrounding instructions. Using this model it is investigated which semantics the read and write operations of Peterson’s mutual exclusion algorithm must have to work correctly.