treating semaphore as atomic hangs operations

[btwilk]

Version: 2.15 The model checker incorrectly detects hung operations when treating a java.util.concurrent.Semaphore as atomic. Minimal example:

class SemaLinTest {

    private val sema = Semaphore(1, true)
    private var x = 0

    @Operation
    fun getAndInc(): Int {
        sema.acquire()
        val result = x
        x += 1
        sema.release()
        return result
    }

    @Test
    fun test() = ModelCheckingOptions()
        .addGuarantee(forClasses("java.util.concurrent.Semaphore").allMethods().treatAsAtomic())
        .check(this::class)
}

Output:

org.jetbrains.kotlinx.lincheck.LincheckAssertionError: 
= The execution has hung, see the thread dump =
Execution scenario (parallel part):
| getAndInc() | getAndInc() |

Thread-1:
    java.lang.Thread.yield(Native Method)
    SemaLinTest.getAndInc(SemaLinTest.kt:21)
    java.lang.Thread.run(Thread.java:748)
Thread-0:
    java.util.concurrent.locks.AbstractQueuedSynchronizer.doAcquireSharedInterruptibly(AbstractQueuedSynchronizer.java:996)
    java.util.concurrent.locks.AbstractQueuedSynchronizer.acquireSharedInterruptibly(AbstractQueuedSynchronizer.java:1304)
    java.util.concurrent.Semaphore.acquire(Semaphore.java:312)
    SemaLinTest.getAndInc(SemaLinTest.kt:18)
    java.lang.Thread.run(Thread.java:748)

[ndkoval]

We will remove the atomic guarantees support, as no real-world concurrent tests utilize it. Thus, I'm closing this issue.

[btwilk]

For the record, I am using the atomic guarantees support. I'm modelling a complex system with multiple subcomponents that I can independently lincheck. I can then model check the aggregate system more deeply with atomic guarantees for the subcomponents. I'm worried that model checking my system will become infeasible without atomic guarantees support.