Re: ConcurrentLinkedDeque is non-linearizable

I'm the right guy for linearizability.
I hope to have time to look at this, but not soon.
I filed JDK-8256833 <https://bugs.openjdk.java.net/browse/JDK-8256833>

On Sun, Nov 22, 2020 at 4:51 PM Nikita Koval via Concurrency-interest <
[email protected]> wrote:

> Something got wrong with the formatting, here is the link to the code and
> the test output:
> https://gist.github.com/ndkoval/56ff3b83d2d39e0afd3a08900e1499d4
>
> 23.11.2020, 03:43, "Nikita Koval" <[email protected]>:
>
> Hi,
>
> ConcurrentLinkedDeque was known as non-linearizable in case of concurrent
> operations on the head for a while — that is because the original paper
> with the algorithm was buggy. Nevertheless, there were two attempts about
> ~2 years ago (first <https://bugs.openjdk.java.net/browse/JDK-8196529>,
> second <https://bugs.openjdk.java.net/browse/JDK-8189387>) to make it
> linearizable in Java 9; that was impressive! Unfortunately, I just found a
> new non-linearizable interleaving with Lincheck
> <https://github.com/Kotlin/kotlinx-lincheck> framework.
>
> = 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
>                                                        |
>
> Here is the Lincheck <https://github.com/Kotlin/kotlinx-lincheck> test
> code that reproduces the error:
> 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 in LTS construction *    @Test    fun test() =
> ModelCheckingOptions()        .actorsBefore(0)        .actorsAfter(0)
>    .*check*(this::class) }
>
> I hope this will help to make it correct! I would also suggest using
> Lincheck <https://github.com/Kotlin/kotlinx-lincheck> for testing all
> concurrent data structures from the standard concurrency library. It is
> also possible to support blocking operations like Thread.park() (now we
> support blocking operations for Kotlin Coroutines, and the approach can be
> scaled) to test synchronization primitives, like locks or semaphores, as
> well — just let me know if you are interested in this.
>
> Best regards,
> Nikita Koval
>
>
> _______________________________________________
> Concurrency-interest mailing list
> [email protected]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>

_______________________________________________
Concurrency-interest mailing list
[email protected]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest