Non-linearizable execution of channels

[qwwdfsad]

ChannelLinearizabilityTest.testConflatedChannelLinearizability:

Non-linearizable execution:
Thread 0: [[close1=true, receive2=java.io.IOException: close1], [close2=false]]
Thread 1: [[receive1=COROUTINE_SUSPENDED], [receive2=COROUTINE_SUSPENDED]]
Thread 2: [[send2=java.io.IOException: close1], [send1=kotlin.Unit, receive1=1]]
Op map: {close1=[true], receive2=[java.io.IOException: close1], close2=[false], send2=[java.io.IOException: close1], send1=[kotlin.Unit], receive1=[1]}

[qwwdfsad]

ChannelLinearizabilityTest.testUnlimitedChannelLinearizability

Non-linearizable execution:
Thread 0: [[receive1=COROUTINE_SUSPENDED], [receive2=COROUTINE_SUSPENDED]]
Thread 1: [[close1=true, receive2=java.io.IOException: close1], [close2=false]]
Thread 2: [[send2=java.io.IOException: close1], [send1=kotlin.Unit, receive1=1]]
Op map: {close1=[true], receive2=[java.io.IOException: close1], close2=[false], send2=[java.io.IOException: close1], send1=[kotlin.Unit], receive1=[1]}

[elizarov]

ChannelLinearizabilityTest.testUnlimitedChannelLinearizability
https://teamcity.jetbrains.com/viewLog.html?buildId=2488201&buildTypeId=KotlinTools_KotlinxCoroutines_NightlyStressWindows

Non-linearizable execution:
Thread 0: [[receive2=COROUTINE_SUSPENDED], [receive1=COROUTINE_SUSPENDED]]
Thread 1: [[send1=java.io.IOException: close1], [send2=kotlin.Unit, receive2=2]]
Thread 2: [[close1=true, receive1=java.io.IOException: close1], [close2=false]]
Op map: {send1=[java.io.IOException: close1], send2=[kotlin.Unit], receive2=[2], close1=[true], receive1=[java.io.IOException: close1], close2=[false]}

[dkhalanskyjb]

testArrayChannelLinearizability[jvm]

Non-linearizable execution:
Thread 0: [[send1=kotlin.Unit], [receive1=3, send2=kotlin.Unit]]
Thread 1: [[send2=COROUTINE_SUSPENDED], [close2=true, receive2=java.io.IOException: close2]]
Thread 2: [[receive2=COROUTINE_SUSPENDED], [close1=false]]
Op map: {send1=[kotlin.Unit], receive1=[3], send2=[kotlin.Unit], close2=[true], receive2=[java.io.IOException: close2], close1=[false]}

[elizarov]

ChannelLinearizabilityTest.testUnlimitedChannelLinearizability
https://teamcity.jetbrains.com/viewLog.html?buildId=2513715&buildTypeId=KotlinTools_KotlinxCoroutines_NightlyStressWindows

Non-linearizable execution:
Thread 0: [[receive1=COROUTINE_SUSPENDED], [receive2=COROUTINE_SUSPENDED]]
Thread 1: [[close1=true, receive2=java.io.IOException: close1], [close2=false]]
Thread 2: [[send2=java.io.IOException: close1], [send1=kotlin.Unit, receive1=1]]
Op map: {close1=[true], receive2=[java.io.IOException: close1], close2=[false], send2=[java.io.IOException: close1], send1=[kotlin.Unit], receive1=[1]}

[elizarov]

ChannelLCStressTest.testConflatedChannelLinearizability
https://teamcity.jetbrains.com/viewLog.html?buildId=2513716&buildTypeId=KotlinTools_KotlinxCoroutines_NightlyStressWindows

Non-linearizable execution:
Thread 0: [[close2=true, receive1=java.io.IOException: close2], [close1=false]]
Thread 1: [[receive2=COROUTINE_SUSPENDED], [receive1=COROUTINE_SUSPENDED]]
Thread 2: [[send2=java.io.IOException: close2], [send1=kotlin.Unit, receive2=1]]
Op map: {close2=[true], receive1=[java.io.IOException: close2], close1=[false], send2=[java.io.IOException: close2], send1=[kotlin.Unit], receive2=[1]}

[elizarov]

Here's the problematic scenario that happens here. We have two queued (suspended) receive calls and a completed close calls that had not yet notified receivers, so the channels queue looks like this:

Rcv1 -> Rcv2 -> Closed

Now, we have two sequential send operations in the other thread:

The first send call starts early (before Rcv1 was queued) and fails to perform an offer, so it switches to sendBuffered strategy trying to add an element to the buffer, but finds that the channel is already closed, so it throws closed exception.

The second send tries to offer and succeeds, making rendezvous with Rcv1.

For from the standpoint of those sends the execution is not linearizable -- first we observe a channel that is already closed, then we observe a channel that is not closed yet.

[elizarov]

The fix is that send operation that observed that the channel was closed must help complete the close operation before throwing an exception.