[Question] ordering in stack push for maintaining invariant

[GWS0428]

Hello,

The lecture slide points out the following invariant

Invariant: head’s pointer value has release view ⊒ (>= for each loc.)
the messages of all node’s value & next pointer

For maintaining that invariant, I think it is necessary to use load Acquire ordering in stack push method.

    loop {
            let head = self.head.load(Relaxed, &guard);
            n.next = head.as_raw();

            match self
                .head
                .compare_exchange(head, n, Release, Relaxed, &guard)
            {
                Ok(_) => break,
                Err(e) => n = e.new,
            }

            // Repin to ensure the global epoch can make progress.
            guard.repin();
        }

without using Acquire, it seems impossible to get the head's release view and store the updated view into the new head. Could you explain why it is correct to use Relaxed ordering in "self.head.load(Relaxed, &guard);" part?

[kingdoctor123]

If the CAS on head succeeds, then release view of previous head is automatically included in the new message due to release sequence. As a result, you don't need to acquire the release view when you execute let head = slef.head.load(Relaxed, &guard);. You can see more information on p.115 of the lecture slide.