Adding a bound to an unbounded queue

Question

I have an approximate concurrent bounded queue written in Java - it is intended to mimic the behavior of a LinkedBlockingQueue except that a. it doesn't use locks and b. it only partially respects the queue's size invariant.

public class LockFreeBoundedQueue<T> {
    private final ConcurrentLinkedQueue<T> queue = new ConcurrentLinkedQueue<>();
    private final AtomicInteger size = new AtomicInteger(0);
    private final int max;

    public LockFreeBoundedQueue(int max) {
        this.max = max;
    }

    public T poll() {
        T t = queue.poll();
        if(t != null) {
            size.decrementAndGet();
        }
        return t;
    }

    public boolean offer(T t) {
        if(t == null) throw new NullPointerException();
        if(size.get() < max) {
            size.incrementAndGet();
            return queue.offer(t);
        }
        return false;
    }

    public int size() {
        return queue.size();
    }
}

If the queue used a lock to enforce the size invariant then model checking would be relatively simple in that the queue would only have three states: empty (poll returns null), full (offer returns false), and neither empty nor full. However, it is possible for more than one thread to pass the size.get() < max guard while size == (max - 1) which will leave the queue in a state with size > max. I am not familiar with how this sort of "approximate invariant" can be specified or verified.

Intuitively, given a system with N threads that may concurrently call offer, I can model the queue as though it had a precise bound of max + N; however if I could prove that this invariant held then I wouldn't need to ask how to prove that this invariant holds.

Answer 1

Couldn't you use if (size.incrementAndGet() < max) { in the atomic fashion it was intended for?

        if (size.incrementAndGet() < max) {
            return queue.offer(t);
        } else {
            // Undo my excessive increment.
            size.decrementAndGet();
        }

Surely this would enforce your invariant.