- If both conditions apply, freeze the location with timestamp `t`. If it
is already frozen, do nothing.
- Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,
- If both conditions apply, freeze the location with timestamp `t`. If it
is already frozen, do nothing.
- Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,