Iqueue implementation for which the lincheck is not able to find non-linearizable execution .It's giving it linearizable.(Both Stress Testing and Model Checking )

[jayrathi5]

Iqueue-pdf.pdf

[eupp]

Hi @jayrathi5 !

In general, Lincheck does not guarantee completeness --- it is a testing/bug-finding tool and naturally it can miss some bugs. It may not be able to generate an execution scenario where non-linearizable execution manifests.

With that being said, it can be that in your specific case it is rather a bug and Lincheck miss some non-linearizable error that should be easy to detect.

If you would share:

• source code of data structure, and
• an execution scenario where non-linearizability should be detectable,

it can simplify an investigation for us.

[jayrathi5]

Hi @jayrathi5 !

In general, Lincheck does not guarantee completeness --- it is a testing/bug-finding tool and naturally it can miss some bugs. It may not be able to generate an execution scenario where non-linearizable execution manifests.

With that being said, it can be that in your specific case it is rather a bug and Lincheck miss some non-linearizable error that should be easy to detect.

If you would share:

• source code of data structure, and
• an execution scenario where non-linearizability should be detectable,

it can simplify an investigation for us.

I have attached a pdf which consists of data structure information and the interleaving which tool is not able to detect.
Iqueue-pdf.pdf

[eupp]

I have attached a pdf which consists of data structure information and the interleaving which tool is not able to detect.
Iqueue-pdf.pdf

Yes, I saw that.
If you will provide it as a code, it will be simpler for us to reproduce error, as we will not have to re-type the code from the pdf : )

[jayrathi5]

Code

`import java.util.concurrent.atomic.AtomicInteger;

public class IQueue {
private final AtomicInteger head = new AtomicInteger(0);
private final AtomicInteger tail = new AtomicInteger(0);
private final Object[] items;

public IQueue(int capacity) {
    items = new Object[capacity];
}

public void enq(T x) throws FullException {
    int slot;
    do {
        slot = tail.get();
        if (slot - head.get() >= items.length) {
            throw new FullException("Queue is full");
        }
    } while (!tail.compareAndSet(slot, slot + 1));
    items[slot % items.length] = x;
}

@SuppressWarnings("unchecked")
public T deq() throws EmptyException {
    T value;
    int slot;
    do {
        slot = head.get();
        if (tail.get() - slot <= 0) {
            throw new EmptyException("Queue is empty");
        }
        value = (T) items[slot % items.length];
    } while (!head.compareAndSet(slot, slot + 1));
    return value;
}

// Custom Exceptions
public static class FullException extends Exception {
    public FullException(String message) {
        super(message);
    }
}

public static class EmptyException extends Exception {
    public EmptyException(String message) {
        super(message);
    }
}

}
`