How to implement `extractState()` correctly for abstract set data type?

[danwt]

I don't fully understand what is meant by 'externally observable state of the test instance' and how to provide it.

I see that extractState() should return an object implementing equals() and hashCode() but I'm not clear on how to derive the implementations. In my case I am modelling a Set ADT with get, insert and erase operations. There is no observable state of the test instance other than the Set implementation, but the Set isn't really observable in any sense, as each of its operations are concurrent.

I look forward to your help. Thank you so much.

[danwt]

Is using a Java concurrent set as a mirror sufficient? Thank you.

[alefedor]

@danwt Hi! Thank you for your question.

An observable state is something that determines what the results of operations will be.
If your set implementation has correct equals() and hashCode(), you can just return the set itself. If not, you can, for example, construct in extractState() a standard library set (e.g., java.util.HashSet) by iterating over your set and adding all its keys.

Here is another way to do it for a set. https://github.com/Kotlin/kotlinx-lincheck/blob/fda4d46a72b71af8e127ede7ab9429d135829eaf/src/jvm/test/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/LockBasedSetTests.kt#L42 In this code, a verifier state is just an array that for every possible element contains true iff the element is in the set.

By the way, we will add a guide with examples that will help users to understand Lincheck better soon.

[danwt]

@alefedor Thanks, you definitely answered a few questions, but I'm still not certain about a few things. For now I am doing

public class LinCheckSetADTTests extends VerifierState {

    private final SetADT impl = new SetADTImpl();
    private final ConcurrentMap<Integer, Integer> stateMirror = new ConcurrentHashMap<>();

    @Operation
    public Optional<Integer> get(@Param(name = "k") int k) {
        return impl.get(k);
    }

    @Operation
    public void insert(@Param(name = "k") int k) {
        stateMirror.put(k, k);
        impl.insert(k);
    }

    @Operation
    public void erase(@Param(name = "k") int k) {
        stateMirror.remove(k);
        impl.erase(k);
    }

    @Test
    public void test() {
        Options opts = new StressOptions();
        LinChecker.check(LinCheckSetADTTests.class, opts);
    }

    @Override
    protected Object extractState() {
        return stateMirror;
    }
}

This passes Linchecks sanity test against extractState, but I'm worried that my usage is not sound, and relies on my impl actually being correct. Your idea seems better, is it the case then that extractState is only called during quiescent intervals?

Thank you. I look forward to the guide too.

[alefedor]

@danwt

is it the case then that extractState is only called during quiescent intervals?

That's right. What is more, extractState is guaranteed to be called exactly once for a test instance and no more operations will be invoked after that, so it can actually "destroy" the data structure if needed. The only problem with mirror states is that they influence the concurrent part of testing, making it more difficult to find a bug.

[danwt]

@alefedor Thanks a lot. I understand now.