[Memory ordering] WSDeque rewrite

This is part of a large-scale refactoring of our use of atomic memory operations (or, rather, fixing the lack therefore) in the runtime system. See !2642 (merged) for details.

---

As described in !2642 (merged), the GHC runtime currently relies heavily on undefined behavior due to data races. While the runtime's WSDeque implementation does attempt to enforce ordering via explicit barriers, these appear to have been added due to observed bugs rather than careful formal reasoning. Consequently, while I believe the current barriers are necessary, I have my doubts that they are sufficient for sound operation.

Thankfully, with the introduction of the C11 memory model we have a widely-used vocabulary for describing concurrent shared-memory algorithms and a deep literature to borrow from.

This patch rewrites GHC's WSDeque implementation to use the Chase and Lev deque implementation provided by [Lê, Pop, et al.]¹. In particular this paper provides three implementations:

• a C implementation relying on sequentially consistent memory ordering (equivalent to the version reported in the original Chase and Lev paper, which our implementation is derived from)
• an optimised C11 implementation using weakly ordered atomics, suitable for use on weakly-ordered memory architectures
• an implementation for ARMv7 using that architecture's LL/SC operations

as well as a proof of soundness of the last implementation (and a sketch of how this proof can be adapted to the C11 implementation). In this patch we steal the C11 implementation for use in WSDeque, shifting a large set of tricky proof obligations off of our shoulders onto the literature.

Deviations from the paper

• Like the original WSDeque implementation, this patch does away with the ability to resize the deque buffer.
• The cas_top operation does not take advantage of the fact that the failure path only requires relaxed ordering.
• We continue to expose the dequeElements and discardElements operations (TODO: Why are these safe? Improve documentation)

1. N.M. Lê, A. Pop, A.Cohen, and F.Z. Nardelli. "Correct and Efficient Work-Stealing for Weak Memory Models". PPoPP'13, February 2013, ACM 978-1-4503-1922/13/02. ↩