Reputation: 18148
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.
Upvotes: 4
Views: 724
Reputation: 65811
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.
Upvotes: 4