[LL] CleanableSoftValueCacheLincheckTest: Check cleanup state of removed values

- Now it's checked that cleanup behaves as expected in a concurrent setting for `put` and `remove`. Note that Lincheck never checks that a value is actually cleaned up. Instead, it compares the result with the single-threaded execution of a scenario. Hence, the non-concurrent `CleanableSoftValueCacheTest` is crucial, as it separately ensures correct deterministic cleanup in a single-threaded environment. - We cannot test that operations returning a new value (such as `get`) always return values which haven't been cleaned up yet, because the value might be cleaned up by another thread between the return point of the operation and cleanup checking. ^KT-62136
2024-02-07 21:02:43 +01:00
parent d4b0dfee0a
commit f7a0e1f7c1
3 changed files with 111 additions and 37 deletions
@@ -5,16 +5,26 @@

 package org.jetbrains.kotlin.analysis.low.level.api.fir.caches

+import org.jetbrains.kotlinx.lincheck.RandomProvider
 import org.jetbrains.kotlinx.lincheck.annotations.Operation
+import org.jetbrains.kotlinx.lincheck.annotations.Param
 import org.jetbrains.kotlinx.lincheck.check
+import org.jetbrains.kotlinx.lincheck.paramgen.ParameterGenerator
+import org.jetbrains.kotlinx.lincheck.paramgen.StringGen
 import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions
 import org.junit.jupiter.api.Test
+import java.io.Serializable

 /**
 * Verifies the linearizability of [CleanableSoftValueCache].
 *
- * This test cannot rely on garbage collector and soft reference queue semantics, so we associate no cleaning operations with it.
+ * While this test cannot rely on garbage collector and soft reference queue semantics to test cleanup after garbage collection, it still
+ * verifies that values are cleaned up after they have been removed with [remove] and [put]. We can't check the same for the compute
+ * functions as they don't return the removed value.
+ *
+ * Also, we cannot test that operations returning a new value always return values which haven't been cleaned up yet, because the value
+ * might be cleaned up by another thread between the return point of the operation and cleanup checking.
 *
 * Various functions of the cache are not checked by Lincheck:
 *
@@ -25,23 +35,66 @@ import org.junit.jupiter.api.Test
 * - [CleanableSoftValueCache.keys] is not checked for linearizability because it is only weakly consistent via the underlying concurrent
 *   hash map implementation.
 */
+@Param(name = "value", gen = ValueWithCleanupGenerator::class)
 class CleanableSoftValueCacheLincheckTest {
-    private val cache = CleanableSoftValueCache<Int, Int> { SoftValueCleaner { } }
+    private val cache = CleanableSoftValueCache<Int, ValueWithCleanup> { it.cleanupMarker }

    @Operation
-    fun get(key: Int): Int? = cache.get(key)
+    fun get(key: Int): ValueWithCleanup? = cache.get(key)

    @Operation
-    fun computeIfAbsent(key: Int, value: Int): Int = cache.computeIfAbsent(key) { value }
+    fun computeIfAbsent(
+        key: Int,
+        @Param(name = "value") value: ValueWithCleanup,
+    ): ValueWithCleanup = cache.computeIfAbsent(key) { value }
+
+    /**
+     * Models a computation that replaces the cache's existing value for [key] with [newValue].
+     */
+    @Operation
+    fun computeReplaceValue(
+        key: Int,
+        @Param(name = "value") newValue: ValueWithCleanup,
+    ): ValueWithCleanup? = cache.compute(key) { _, _ -> newValue }
+
+    /**
+     * Models a computation that keeps the cache's existing value for [key].
+     */
+    @Operation
+    fun computeKeepValue(key: Int): ValueWithCleanup? = cache.compute(key) { _, existingValue -> existingValue }
+
+    /**
+     * Models a computation that removes the cache's existing value for [key] (if any).
+     */
+    @Operation
+    fun computeRemoveValue(key: Int): ValueWithCleanup? = cache.compute(key) { _, _ -> null }

    @Operation
-    fun compute(key: Int, offset: Int): Int? = cache.compute(key) { _, base -> (base ?: 0) + offset }
+    fun put(
+        key: Int,
+        @Param(name = "value") value: ValueWithCleanup,
+    ): RemovalResult? = withRemovalResult { cache.put(key, value) }

    @Operation
-    fun put(key: Int, value: Int): Int? = cache.put(key, value)
+    fun remove(key: Int): RemovalResult? = withRemovalResult { cache.remove(key) }

-    @Operation
-    fun remove(key: Int): Int? = cache.remove(key)
+    /**
+     * [RemovalResult] makes the cleanup state of [value] explicit, allowing Lincheck to detect differences between the cleanup state of a
+     * single-threaded and concurrent execution.
+     *
+     * [CleanableSoftValueCacheTest] separately ensures that deterministic cleanup behaves correctly in non-concurrent scenarios.
+     *
+     * This class implements [Serializable] so that it can be contained in scenarios generated by Lincheck.
+     */
+    data class RemovalResult(
+        val value: ValueWithCleanup,
+        val isCleanedUp: Boolean,
+    ) : Serializable
+
+    private fun withRemovalResult(operation: () -> ValueWithCleanup?): RemovalResult? {
+        val value = operation() ?: return null
+        return RemovalResult(value, value.isCleanedUp)
+    }

    @Test
    fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
@@ -49,3 +102,9 @@ class CleanableSoftValueCacheLincheckTest {
    @Test
    fun stressTest() = StressOptions().check(this::class)
 }
+
+class ValueWithCleanupGenerator(randomProvider: RandomProvider, configuration: String) : ParameterGenerator<ValueWithCleanup> {
+    private val stringGenerator: StringGen = StringGen(randomProvider, "")
+
+    override fun generate(): ValueWithCleanup = ValueWithCleanup(stringGenerator.generate())
+}
@@ -197,35 +197,6 @@ class CleanableSoftValueCacheTest {
        assertTrue(value3.isCleanedUp)
    }

-    class ValueWithCleanup(val name: String) {
-        val cleanupMarker: CleanupMarker = CleanupMarker()
-
-        val isCleanedUp: Boolean get() = cleanupMarker.isCleanedUp
-
-        // This equality implementation is needed as we want to check that `compute` doesn't clean up a replaced value that is referentially
-        // equal to the new value, but does clean up a replaced value that is only equal to the new value by `equals`, not reference.
-        override fun equals(other: Any?): Boolean = (other as? ValueWithCleanup)?.name == name
-
-        override fun hashCode(): Int = name.hashCode()
-
-        override fun toString(): String = "ValueWithCleanup:$name"
-    }
-
-    /**
-     * [ValueWithCleanup] shouldn't be referenced from its [SoftValueCleaner], because this would make the value strongly reachable from the
-     * reference held by [CleanableSoftValueCache]. Instead, we need to keep [isCleanedUp] in this separate class.
-     *
-     * We cannot check the cleanup count in this test because `CleanableSoftValueCache` does not guarantee any specific number of cleanup
-     * calls.
-     */
-    class CleanupMarker : SoftValueCleaner<ValueWithCleanup> {
-        var isCleanedUp: Boolean = false
-
-        override fun cleanUp(value: ValueWithCleanup?) {
-            isCleanedUp = true
-        }
-    }
-
    private fun createCache(): CleanableSoftValueCache<String, ValueWithCleanup> = CleanableSoftValueCache { it.cleanupMarker }

    private fun setUpCache(vararg values: ValueWithCleanup): CleanableSoftValueCache<String, ValueWithCleanup> {
@@ -0,0 +1,44 @@
+/*
+ * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors.
+ * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file.
+ */
+
+package org.jetbrains.kotlin.analysis.low.level.api.fir.caches
+
+import java.io.Serializable
+
+/**
+ * A value with a [CleanupMarker] to be used in [CleanableSoftValueCache] tests.
+ *
+ * This class implements [Serializable] so that it can be contained in scenarios generated by Lincheck.
+ */
+class ValueWithCleanup(val name: String) : Serializable {
+    val cleanupMarker: CleanupMarker = CleanupMarker()
+
+    val isCleanedUp: Boolean get() = cleanupMarker.isCleanedUp
+
+    // This equality implementation is needed as we want to check that `compute` doesn't clean up a replaced value that is referentially
+    // equal to the new value, but does clean up a replaced value that is only equal to the new value by `equals`, not reference.
+    override fun equals(other: Any?): Boolean = (other as? ValueWithCleanup)?.name == name
+
+    override fun hashCode(): Int = name.hashCode()
+
+    override fun toString(): String = "ValueWithCleanup:'$name'"
+}
+
+/**
+ * Tracks whether the associated [ValueWithCleanup] has been cleaned up yet.
+ *
+ * [ValueWithCleanup] shouldn't be referenced from its [SoftValueCleaner], because this would make the value strongly reachable from the
+ * reference held by [CleanableSoftValueCache]. Instead, we need to keep [isCleanedUp] in this separate class.
+ *
+ * We cannot check the cleanup count in this test because `CleanableSoftValueCache` does not guarantee any specific number of cleanup
+ * calls.
+ */
+class CleanupMarker : SoftValueCleaner<ValueWithCleanup>, Serializable {
+    var isCleanedUp: Boolean = false
+
+    override fun cleanUp(value: ValueWithCleanup?) {
+        isCleanedUp = true
+    }
+}