Model checking violation (2.18.1 vs 2.25)

[ben-manes]

After upgrading Lincheck I am receiving a model checking interleaving violation. This test ran flawlessly on Lincheck since adopting it at v2.14.1. I'm unsure if it is a regression or an improved checker, as ChatGPT and Gemini are of opposing opinions. Unfortunately I can't narrow it down to the Lincheck version due to previous bugs; thank you for fixing those!

Here is failing github action, the raw log, and can be reproduced locally by running ./gradlew :caffeine:lincheckTest on that commit.

The cache is layered on top of ConcurrentHashMap, which holds the (K => Node) mapping for the LRU entry. A write is performed first in the hash table under its lock, and then recorded into a write buffer (afterWrite) to replay the work against the eviction policy asynchronously. As the test is set with an unreachable capacity, no evictions occur and this LRU reordering is a not a user-visible state change. In the logs, after the write then the thread is appending to the JCTools queue and will then return the writer's result. If I switch to an unbounded queue then this does not fail locally, so it seems to be related to the queue growing or perhaps being full (where the caller may assist in the maintenance work to drain it).

ChatGPT says this is not linearizable because of the delay between Thread 1 writing but returning after Thread 2 overwrote the value. The delay was due to waiting on the event to be recorded in the write buffer and it will return the map operation's result so the data is consistent. It says that "this violates the linearizability property, which requires that operations appear to take effect instantaneously at some point between their invocation and response."

Gemini says that "the final outcome in this specific case doesn't violate linearizability" but that warning of a potential ordering anomaly makes sense for evaluation, assuming it can be suppressed as a false positive.

What do you think? Any reason why the model checker would flag this on the latest version but not in the previous one?

[ben-manes]

oh, v2.26 was released today explicitly to fix this issue! 😅

It passes on x86.

It seems to have hung on aarch64.

I have run it successfully locally on an M3 macbook, but not on CircleCI, likely because of fewer cpu cores (as we saw that affected Lincheck in past bugs).

[ndkoval]

Hi @ben-manes, it's cool that the recent fix has helped you!

I've created an issue (#280) for the remaining problem and closing the current one.