1. In the ARM code of steal, the first `ctrl_isync` barrier after (b)
    is redundant as all following instructions are conditional upon
    the test `t < b`, hence we can exploit the control dependency.

The following two bugs have been kindly reported by Brian Demsky et
al. from the University of California, Irvine.

 2. In both versions of the code, there is a missing reload of
    variable `a` after a resize. Also, in 4.2.2, the read instance
    `Ra,&x'` is missing, although the following accesses are correctly
    made against `x'`, and the rest of the proof behaves as if
    variable a were correctly reloaded.

 3. In the C11 code of steal, the read from variable a requires
    `memory_order_consume` instead of `memory_order_relaxed`:

       Array *a = load_explicit(&q->array, memory_order_relaxed);
       x = load_explicit(&a->buffer[t % a->size], memory_order_relaxed);

   Needs to be fixed to:

       Array *a = load_explicit(&q->array, memory_order_consume);
       x = load_explicit(&a->buffer[t % a->size], memory_order_relaxed);

    The address dependency between the two statements is needed to
    ensure correctness in the presence of possible races between
    a resizing push and a concurrent steal operation. Consider, for
    example, the following scenario (reproduced from the initial bug
    report by Brian Demsky):

     1. Suppose the push operation performs a resize.
     2. Suppose the steal operation reads the `t` and `b` from the
        prior steal operation (it doesn't synchronize with this steal
        operation).
     3. Suppose the steal operation then reads the `array` field
        written by the resize operation.
     4. The steal operation can then read values from the array object
        in a partially initialized state as no synchronization is
        established between the resize operation and the loads from
        the buffer array.

    Neither the ARM assembly version nor the proof needs to be
    changed. The proof correctly relies on an address dependency being
    present; this hypothesis is used to establish Lemma 6 and
    Corollary 2, which would be violated by the above example, if the
    dependency were ineffective. Address dependencies are implicit in
    ARM assembly, and need not be materialized in the code. The
    dependency was subsequently lost in the translation to C11 from
    ARM assembly.