JSR166 Concurrency

ConcurrentLinkedDeque is non-linearizable

Classic

List

Threaded

3 messages Options

JSR166 Concurrency mailing list

ConcurrentLinkedDeque is non-linearizable

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, second) to make it linearizable in Java 9; that was impressive! Unfortunately, I just found a new non-linearizable interleaving with 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 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 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

JSR166 Concurrency mailing list

Re: ConcurrentLinkedDeque is non-linearizable

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" <[hidden email]>:

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, second) to make it linearizable in Java 9; that was impressive! Unfortunately, I just found a new non-linearizable interleaving with 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(): [hidden email] 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 | |
| | [hidden email],4,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) |
| | [hidden email]) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921) |
| | result: 4 |
| | thread is finished |

Here is the 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 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

JSR166 Concurrency mailing list

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

On Sun, Nov 22, 2020 at 4:51 PM Nikita Koval via Concurrency-interest <[hidden email]> 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" <[hidden email]>:
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, second) to make it linearizable in Java 9; that was impressive! Unfortunately, I just found a new non-linearizable interleaving with 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(): [hidden email] 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 | |
| | [hidden email],4,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) |
| | [hidden email]) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921) |
| | result: 4 |
| | thread is finished |

Here is the 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 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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

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