In "A better run queue" the second code block has
self.tail.store(tail + 1, Release);
self.tail.store(tail.wrapping_add(1), Release);
Another comment:
> The first load can most likely be done safely with Relaxed ordering, but there were no measurable gains in switching.
This code is using an Acquire/Release pair, except it's Acquire/Release on different memory slots, which means there's no actual happens-before edge. This makes the Acquire/Release pair somewhat confusing (which tripped me up too in the first version of this comment).
Furthermore, I don't see anything in here that relies on the head load here being an Acquire. This Acquire would synchronize with the Release store on head in the pop operation, except what's being written in the pop is the fact that we don't care about the memory anymore, meaning we don't need to be able to read anything written by the pop (except for the head pointer itself).
This suggests to me that the head load/store should be Relaxed (especially because in the load literally all we care about for head is the current pointer value, for the length comparison, as already explained by the article). The tail of course should remain Release on the push, and I assume there's an Acquire there on the work-stealing pop (since you only list the local-thread pop code, which is doing an unsynced load here as an optimization). I don't promise that this is correct but this is my impression after a few minutes of consideration.