ConcurrentLinkedDeque non-linearizability

ConcurrentLinkedDequeTest.kt

class ConcurrentLinkedDequeTest : VerifierState() {
    private val d = ConcurrentLinkedDeque<Int>()

    @Operation fun addFirst(value: Int) = d.addFirst(value)
    @Operation fun addLast(value: Int) = d.addLast(value)
    @Operation fun getFirst() = d.peekFirst()
    @Operation fun getLast() = d.peekLast()
    @Operation fun pollFirst() = d.pollFirst()
    @Operation fun pollLast() = d.pollLast()

    override fun extractState() = d.toList() // to determine same logical states

    @Test
    fun test() = ModelCheckingOptions()
        .actorsBefore(0)
        .actorsAfter(0)
        .check(this::class)
}


// == Invalid execution results =
// Parallel part:
// | addFirst(10): void [-,1] | addFirst(4): void       |
// | getLast():    4    [1,1] | pollFirst(): 4    [-,1] |
// ---
// values in "[..]" brackets indicate the number of completed operations 
// in each of the parallel threads seen at the beginning of the current operation
// ---
// 
// = The following interleaving leads to the error =
// Parallel part trace:
// |                      | addFirst(4): void                                                                                       |
// |                      | pollFirst()                                                                                             |
// |                      |   first(): Node@1 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:915)                    |
// |                      |   item.READ: 4 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917)                       |
// |                      |   prev.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:919)                    |
// |                      |   switch                                                                                                |
// | addFirst(10): void   |                                                                                                         |
// | getLast(): 4         |                                                                                                         |
// |   thread is finished |                                                                                                         |
// |                      |   compareAndSet(Node@1,4,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) |
// |                      |   unlink(Node@1) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921)                     |
// |                      |   result: 4                                                                                             |
// |                      |   thread is finished                                                                                    |