Before, we could get "no element" response, when in fact the queue is not empty. This can happen when tail_ is being in the middle of the update but its "next" field has not been updated yet (inside Push).
Before the change, we treated this state as "Empty", while the queue could have multiple entries (probably 1 or 2). After this change: we retry the pop operation in scheduler until we reach the true depletion of the remote queue.
Before, we could get "no element" response, when in fact the queue is not empty. This can happen when
tail_is being in the middle of the update but its "next" field has not been updated yet (inside Push).Before the change, we treated this state as "Empty", while the queue could have multiple entries (probably 1 or 2). After this change: we retry the pop operation in scheduler until we reach the true depletion of the remote queue.