寻找对我的线程安全，无锁队列实施的批评

所以，经过一些研究，我已经写了一个队列。它使用固定尺寸的缓冲区，因此是圆形队列。它必须是线程安全的，我试图使其无锁。我想知道这是什么问题，因为这些事情很难自己预测。

这是标题：

template <class T>
class LockFreeQueue
{
public:
    LockFreeQueue(uint buffersize) : buffer(NULL), ifront1(0), ifront2(0), iback1(0), iback2(0), size(buffersize) { buffer = new atomic <T>[buffersize]; }
    ~LockFreeQueue(void) { if (buffer) delete[] buffer; }
    bool pop(T* output);
    bool push(T input);
private:
    uint incr(const uint val)
        {return (val + 1) % size;}
    atomic <T>* buffer;
    atomic <uint> ifront1, ifront2, iback1, iback2;
    uint size;
};

这是实现：

template <class T>
bool LockFreeQueue<T>::pop(T* output)
{
    while (true)
    {
        /* Fetch ifront and store it in i. */
        uint i = ifront1;
        /* If ifront == iback, the queue is empty. */
        if (i == iback2)
            return false;
        /* If i still equals ifront, increment ifront, */
        /* Incrememnting ifront1 notifies pop() that it can read the next element. */
        if (ifront1.compare_exchange_weak(i, incr(i)))
        {
            /* then fetch the output. */
            *output = buffer[i];
            /* Incrememnting ifront2 notifies push() that it's safe to write. */
            ++ifront2;
            return true;
        }
        /* If i no longer equals ifront, we loop around and try again. */
    }
}
template <class T>
bool LockFreeQueue<T>::push(T input)
{
    while (true)
    {
        /* Fetch iback and store it in i. */
        uint i = iback1;
        /* If ifront == (iback +1), the queue is full. */
        if (ifront2 == incr(i))
            return false;
        /* If i still equals iback, increment iback, */
        /* Incrememnting iback1 notifies push() that it can write a new element. */
        if (iback1.compare_exchange_weak(i, incr(i)))
        {
            /* then store the input. */
            buffer[i] = input;
            /* Incrementing iback2 notifies pop() that it's safe to read. */
            ++iback2;
            return true;
        }
        /* If i no longer equals iback, we loop around and try again. */
    }
}

编辑：根据评论，我对代码进行了一些重大修改（感谢Killiands和N.M.！）。最重要的是，Ifront和Iback现在是IFRONT1，IFRONT2，IBACK1和IBACK2。push（）现在将增加iback1，并通知其他推动线程可以安全地写入下一个元素（只要它不满），写入元素，然后递增iback2。iback2是由pop（）检查的全部。pop（）做同样的事情，但是使用ifrontn索引。

现在，我再次陷入了"这应该起作用……"的陷阱，但我对正式证明或类似的事情一无所知。至少这一次，我想不出一种可能失败的潜在方法。除了"停止尝试编写免费锁定代码"外，任何建议都将受到赞赏。