diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicFieldUpdaterNames.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicFieldUpdaterNames.kt index 04c2d5b76..33292d2d7 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicFieldUpdaterNames.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicFieldUpdaterNames.kt @@ -24,7 +24,7 @@ import java.util.concurrent.atomic.AtomicReferenceFieldUpdater internal object AtomicFieldUpdaterNames { @Suppress("DEPRECATION") - internal fun getAtomicFieldUpdaterName(updater: Any): String? { + internal fun getAtomicFieldUpdaterName(updater: Any): AtomicFieldUpdaterDescriptor? { if (updater !is AtomicIntegerFieldUpdater<*> && updater !is AtomicLongFieldUpdater<*> && updater !is AtomicReferenceFieldUpdater<*, *>) { throw IllegalArgumentException("Provided object is not a recognized Atomic*FieldUpdater type.") } @@ -37,11 +37,26 @@ internal object AtomicFieldUpdaterNames { val offsetField = updater.javaClass.getDeclaredField("offset") val offset = UNSAFE.getLong(updater, UNSAFE.objectFieldOffset(offsetField)) - return findFieldNameByOffsetViaUnsafe(targetType, offset) + return findFieldNameByOffsetViaUnsafe(targetType, offset).let { fieldName -> + if (fieldName != null) { + AtomicFieldUpdaterDescriptor(targetType, fieldName) + } + else { + null + } + } } catch (t: Throwable) { t.printStackTrace() } return null // Field not found } -} \ No newline at end of file +} + +/** + * Descriptor of the Java AFU instance. + */ +internal data class AtomicFieldUpdaterDescriptor( + val targetType: Class<*>, + val fieldName: String +) \ No newline at end of file diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicReferenceNames.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicReferenceNames.kt index e2e0f1dd2..f351722ce 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicReferenceNames.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/AtomicReferenceNames.kt @@ -22,7 +22,7 @@ import java.util.concurrent.atomic.AtomicReferenceArray /** * Provides method call type to create a more convenient trace point - * with a owner of this AtomicReference field and a name if it can be found. + * with an owner of this AtomicReference field and a name if it can be found. * Recursively scans the test object, trying to find the provided AtomicReference * instance as a field. If two or more fields contain this AtomicReference field, then we * fall back to the default behavior. diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt index 169e329fa..5daf46e2b 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/ManagedStrategy.kt @@ -950,6 +950,63 @@ abstract class ManagedStrategy( staticMemorySnapshot.trackObjects(objs) } + + + /** + * Tracks fields that are accessed via System.arraycopy, Unsafe API, VarHandle API, Java AFU API, and kotlinx.atomicfu. + */ + private fun processMethodEffectOnStaticSnapshot(owner: Any?, params: Array) { + when { + // Unsafe API + isUnsafe(owner) -> { + val methodType: UnsafeName = UnsafeNames.getMethodCallType(params) + when (methodType) { + is UnsafeInstanceMethod -> { + staticMemorySnapshot.trackField(methodType.owner, methodType.owner.javaClass, methodType.fieldName) + } + is UnsafeStaticMethod -> { + staticMemorySnapshot.trackField(null, methodType.clazz, methodType.fieldName) + } + is UnsafeArrayMethod -> { + staticMemorySnapshot.trackArrayCell(methodType.array, methodType.index) + } + else -> {} + } + } + // VarHandle API + isVarHandle(owner) && + ( + VarHandleNames.isInstanceVarHandle(owner) && staticMemorySnapshot.isTracked(params.firstOrNull()) || + VarHandleNames.isArrayVarHandle(owner) && staticMemorySnapshot.isTracked(params.firstOrNull()) || + VarHandleNames.isStaticVarHandle(owner) + ) -> { + val methodType: VarHandleMethodType = VarHandleNames.varHandleMethodType(owner, params) + when (methodType) { + is InstanceVarHandleMethod -> { + staticMemorySnapshot.trackField(methodType.owner, methodType.owner.javaClass, methodType.fieldName) + } + is StaticVarHandleMethod -> { + staticMemorySnapshot.trackField(null, methodType.ownerClass, methodType.fieldName) + } + is ArrayVarHandleMethod -> { + staticMemorySnapshot.trackArrayCell(methodType.array, methodType.index) + } + else -> {} + } + } + // Java AFU (this also automatically handles the `kotlinx.atomicfu`, since they are compiled to Java AFU + Java atomic arrays) + isAtomicFieldUpdater(owner) -> { + val obj = params[0] + val afuDesc: AtomicFieldUpdaterDescriptor? = AtomicFieldUpdaterNames.getAtomicFieldUpdaterName(owner!!) + check(afuDesc != null) { "Cannot extract field name referenced by Java AFU object $owner" } + + staticMemorySnapshot.trackField(obj, afuDesc.targetType, afuDesc.fieldName) + } + // TODO: System.arraycopy + // TODO: reflexivity + } + } + private fun methodGuaranteeType(owner: Any?, className: String, methodName: String): ManagedGuaranteeType? = runInIgnoredSection { userDefinedGuarantees?.forEach { guarantee -> val ownerName = owner?.javaClass?.canonicalName ?: className @@ -969,9 +1026,15 @@ abstract class ManagedStrategy( methodId: Int, params: Array ) { - val guarantee = runInIgnoredSection { + var guarantee: ManagedGuaranteeType? = null + + runInIgnoredSection { + // process method effect on the static memory snapshot + processMethodEffectOnStaticSnapshot(owner, params) + + // process known method concurrency guarantee val atomicMethodDescriptor = getAtomicMethodDescriptor(owner, methodName) - val guarantee = when { + guarantee = when { (atomicMethodDescriptor != null) -> ManagedGuaranteeType.TREAT_AS_ATOMIC else -> methodGuaranteeType(owner, className, methodName) } @@ -988,8 +1051,8 @@ abstract class ManagedStrategy( if (guarantee == null) { loopDetector.beforeMethodCall(codeLocation, params) } - guarantee } + if (guarantee == ManagedGuaranteeType.IGNORE || guarantee == ManagedGuaranteeType.TREAT_AS_ATOMIC) { // It's important that this method can't be called inside runInIgnoredSection, as the ignored section @@ -1346,7 +1409,7 @@ abstract class ManagedStrategy( atomicUpdater: Any, parameters: Array, ): MethodCallTracePoint { - getAtomicFieldUpdaterName(atomicUpdater)?.let { tracePoint.initializeOwnerName(it) } + getAtomicFieldUpdaterName(atomicUpdater)?.let { tracePoint.initializeOwnerName(it.fieldName) } tracePoint.initializeParameters(parameters.drop(1).map { adornedStringRepresentation(it) }) return tracePoint } diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/SnapshotTracker.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/SnapshotTracker.kt index 258d2b967..986f21529 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/SnapshotTracker.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/SnapshotTracker.kt @@ -46,10 +46,27 @@ class SnapshotTracker { class ArrayCellNode(val index: Int, initialValue: Any?) : MemoryNode(initialValue) } - fun trackField(obj: Any?, className: String, fieldName: String) { + fun isTracked(obj: Any?): Boolean = obj != null && obj in trackedObjects + + fun trackField(obj: Any?, accessClass: Class<*>, fieldName: String) { if (obj != null && obj !in trackedObjects) return + trackFieldImpl( + obj = obj, + clazz = getDeclaringClass(obj, accessClass, fieldName), + fieldName = fieldName + ) + } + + fun trackField(obj: Any?, accessClassName: String, fieldName: String) { + if (obj != null && obj !in trackedObjects) return + trackFieldImpl( + obj = obj, + clazz = getDeclaringClass(obj, Class.forName(accessClassName), fieldName), + fieldName = fieldName + ) + } - val clazz = getDeclaringClass(obj, className, fieldName) + private fun trackFieldImpl(obj: Any?, clazz: Class<*>, fieldName: String) { val field = clazz.findField(fieldName) val readResult = readFieldSafely(obj, field) @@ -179,9 +196,8 @@ class SnapshotTracker { private fun shouldTrackEagerly(obj: Any?): Boolean { if (obj == null) return false return ( - // TODO: in further development of snapshot restoring feature this check should be removed - // (and only check for java atomic classes should be inserted), see https://github.com/JetBrains/lincheck/pull/418#issue-2595977113 - // right now it is needed for collections to be restored properly (because of missing support for `System.arrayCopy()` and other similar methods) + // TODO: after support for System.arraycopy, + // rewrite to `obj.javaClass.name.startsWith("java.util.concurrent.") && obj.javaClass.name.contains("Atomic")` obj.javaClass.name.startsWith("java.util.") ) } @@ -237,8 +253,8 @@ class SnapshotTracker { ) } - private fun getDeclaringClass(obj: Any?, className: String, fieldName: String): Class<*> { - return Class.forName(className).let { + private fun getDeclaringClass(obj: Any?, clazz: Class<*>, fieldName: String): Class<*> { + return clazz.let { if (obj != null) it else it.findField(fieldName).declaringClass } diff --git a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/VarHandleNames.kt b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/VarHandleNames.kt index 16e1a81a8..a4a0387c0 100644 --- a/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/VarHandleNames.kt +++ b/src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/VarHandleNames.kt @@ -22,59 +22,85 @@ import java.lang.reflect.Field @Suppress("SameParameterValue") internal object VarHandleNames { + private val instanceVarHandles = instanceNameExtractor( + "java.lang.invoke.VarHandleInts\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleDoubles\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleLongs\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleFloats\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleBytes\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleShorts\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleChars\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleBooleans\$FieldInstanceReadOnly" + ) + + private val referenceInstanceVarHandles = referenceExtractor( + "java.lang.invoke.VarHandleReferences\$FieldInstanceReadOnly", + "java.lang.invoke.VarHandleObjects\$FieldInstanceReadOnly", + factory = ::VarHandleInstanceNameExtractor + ) + + private val staticVarHandles = staticNameExtractor( + "java.lang.invoke.VarHandleInts\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleDoubles\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleLongs\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleFloats\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleBytes\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleShorts\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleChars\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleBooleans\$FieldStaticReadOnly", + ) + + private val referenceStaticVarHandles = referenceExtractor( + "java.lang.invoke.VarHandleReferences\$FieldStaticReadOnly", + "java.lang.invoke.VarHandleObjects\$FieldStaticReadOnly", + factory = ::VarHandleStaticNameExtractor + ) + + private val arrayVarHandles = arrayNameExtractor( + "java.lang.invoke.VarHandleInts\$Array", + "java.lang.invoke.VarHandleDoubles\$Array", + "java.lang.invoke.VarHandleLongs\$Array", + "java.lang.invoke.VarHandleFloats\$Array", + "java.lang.invoke.VarHandleBytes\$Array", + "java.lang.invoke.VarHandleShorts\$Array", + "java.lang.invoke.VarHandleChars\$Array", + "java.lang.invoke.VarHandleBooleans\$Array", + ) + + private val referenceArrayVarHandles = referenceExtractor( + "java.lang.invoke.VarHandleReferences\$Array", + "java.lang.invoke.VarHandleObjects\$Array", + factory = ::VarHandeArrayNameExtractor + ) + private val nameExtractors: List = listOf( // Primitive VarHandles - instanceNameExtractor( - "java.lang.invoke.VarHandleInts\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleDoubles\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleLongs\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleFloats\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleBytes\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleShorts\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleChars\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleBooleans\$FieldInstanceReadOnly" - ), - staticNameExtractor( - "java.lang.invoke.VarHandleInts\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleDoubles\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleLongs\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleFloats\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleBytes\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleShorts\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleChars\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleBooleans\$FieldStaticReadOnly", - ), - arrayNameExtractor( - "java.lang.invoke.VarHandleInts\$Array", - "java.lang.invoke.VarHandleDoubles\$Array", - "java.lang.invoke.VarHandleLongs\$Array", - "java.lang.invoke.VarHandleFloats\$Array", - "java.lang.invoke.VarHandleBytes\$Array", - "java.lang.invoke.VarHandleShorts\$Array", - "java.lang.invoke.VarHandleChars\$Array", - "java.lang.invoke.VarHandleBooleans\$Array", - ), + instanceVarHandles, + staticVarHandles, + arrayVarHandles, // Reference type VarHandle. // Many options are present due to different class names in different JDKs. listOfNotNull( - referenceExtractor( - "java.lang.invoke.VarHandleReferences\$FieldInstanceReadOnly", - "java.lang.invoke.VarHandleObjects\$FieldInstanceReadOnly", - factory = ::VarHandleInstanceNameExtractor - ), - referenceExtractor( - "java.lang.invoke.VarHandleReferences\$FieldStaticReadOnly", - "java.lang.invoke.VarHandleObjects\$FieldStaticReadOnly", - factory = ::VarHandleStaticNameExtractor - ), - referenceExtractor( - "java.lang.invoke.VarHandleReferences\$Array", - "java.lang.invoke.VarHandleObjects\$Array", - factory = ::VarHandeArrayNameExtractor - ) + referenceInstanceVarHandles, + referenceStaticVarHandles, + referenceArrayVarHandles ) ).flatten() + internal fun isInstanceVarHandle(varHandle: Any): Boolean { + return instanceVarHandles.any { it.canExtract(varHandle) } || + referenceInstanceVarHandles?.canExtract(varHandle) == true + } + + internal fun isStaticVarHandle(varHandle: Any): Boolean { + return staticVarHandles.any { it.canExtract(varHandle) } || + referenceStaticVarHandles?.canExtract(varHandle) == true + } + + internal fun isArrayVarHandle(varHandle: Any): Boolean { + return arrayVarHandles.any { it.canExtract(varHandle) } || + referenceArrayVarHandles?.canExtract(varHandle) == true + } // varHandle is Any because of Java 8, where VarHandle class does not exist internal fun varHandleMethodType(varHandle: Any, parameters: Array): VarHandleMethodType = runCatching { @@ -117,13 +143,11 @@ internal object VarHandleNames { */ private class VarHandleStaticNameExtractor(varHandleClass: Class<*>) : VarHandleNameExtractor(varHandleClass) { private val fieldOffsetField: Field = varHandleClass.getDeclaredField("fieldOffset") - private val receiverTypeField: Field = varHandleClass.getDeclaredField("base") override fun getMethodType(varHandle: Any, parameters: Array): VarHandleMethodType { val ownerType = readFieldViaUnsafe(varHandle, receiverTypeField, Unsafe::getObject) as Class<*> val fieldOffset = readFieldViaUnsafe(varHandle, fieldOffsetField, Unsafe::getLong) - val fieldName = findFieldNameByOffsetViaUnsafe(ownerType, fieldOffset) ?: return TreatAsDefaultMethod return StaticVarHandleMethod(ownerType, fieldName, parameters.toList()) diff --git a/src/jvm/test-jdk11/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/VarHandleModificationsSnapshotTest.kt b/src/jvm/test-jdk11/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/VarHandleModificationsSnapshotTest.kt new file mode 100644 index 000000000..344bde651 --- /dev/null +++ b/src/jvm/test-jdk11/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/VarHandleModificationsSnapshotTest.kt @@ -0,0 +1,83 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.strategy.modelchecking.snapshot + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedOptions +import java.lang.invoke.MethodHandles +import java.lang.invoke.VarHandle +import kotlin.random.Random + + +class VarHandleModificationsSnapshotTest : AbstractSnapshotTest() { + private class Wrapper(var x: Int) + companion object { + private var value = 1 + private var ref = Wrapper(1) + private var intArray = intArrayOf(1, 2, 3) + + // remember values for restoring + private val initRef = ref + private val initIntArray = intArray + } + + val valueHandle: VarHandle = MethodHandles.lookup() + .`in`(VarHandleModificationsSnapshotTest::class.java) + .findStaticVarHandle(VarHandleModificationsSnapshotTest::class.java, "value", Int::class.java) + val refHandle: VarHandle = MethodHandles.lookup() + .`in`(VarHandleModificationsSnapshotTest::class.java) + .findStaticVarHandle(VarHandleModificationsSnapshotTest::class.java, "ref", Wrapper::class.java) + val intArrayHandle: VarHandle = MethodHandles.lookup() + .`in`(VarHandleModificationsSnapshotTest::class.java) + .findStaticVarHandle(VarHandleModificationsSnapshotTest::class.java, "intArray", IntArray::class.java) + val intArrayElementsHandle: VarHandle = MethodHandles.arrayElementVarHandle(IntArray::class.java) + + class VarHandleModificationsVerifier(@Suppress("UNUSED_PARAMETER") sequentialSpecification: Class<*>) : SnapshotVerifier() { + override fun verifyResults(scenario: ExecutionScenario?, results: ExecutionResult?): Boolean { + checkForExceptions(results) + check(value == 1) + check(ref === initRef && ref.x == 1) + check(intArray === initIntArray && intArray.contentEquals(intArrayOf(1, 2, 3))) + return true + } + } + + override fun > O.customize() { + verifier(VarHandleModificationsVerifier::class.java) + iterations(100) + invocationsPerIteration(1) + threads(1) + actorsPerThread(10) + } + + @Operation + fun putValue() { + valueHandle.set(Random.nextInt()) + } + + @Operation + fun putRef() { + refHandle.set(Wrapper(Random.nextInt())) + } + + @Operation + fun putIntArrayElement() { + val idx = Random.nextInt(0, intArray.size) + intArrayElementsHandle.set(intArray, idx, Random.nextInt()) + } + + @Operation + fun assignIntArray() { + intArrayHandle.set(intArrayOf(Random.nextInt(), Random.nextInt(), Random.nextInt())) + } +} diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/ArraysAPISnapshotTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/ArraysAPISnapshotTest.kt new file mode 100644 index 000000000..4d5c9ab4f --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/ArraysAPISnapshotTest.kt @@ -0,0 +1,112 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.strategy.modelchecking.snapshot + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedOptions +import org.junit.Ignore +import java.util.Arrays +import kotlin.random.Random + +// TODO: parallel operations are not supported because of java.lang.ClassCastException: +// class java.util.concurrent.ForkJoinWorkerThread cannot be cast to class sun.nio.ch.lincheck.TestThread +// (java.util.concurrent.ForkJoinWorkerThread is in module java.base of loader 'bootstrap'; +// sun.nio.ch.lincheck.TestThread is in unnamed module of loader 'bootstrap') +@Ignore("Without support for System.arraycopy, tracking for copy methods will not work") +class ArraysAPISnapshotTest : AbstractSnapshotTest() { + private class Wrapper(var x: Int) + companion object { + private var intArray = intArrayOf(2, 1, 4, 3, 6, 5, 8, 7, 10, 9) + private var refArray = arrayOf(Wrapper(1), Wrapper(3), Wrapper(2)) + + // save values to restore + private val refIntArray = intArray + private val refRefArray = refArray + private val a = refArray[0] + private val b = refArray[1] + private val c = refArray[2] + } + + class ArraysAPIVerifier(@Suppress("UNUSED_PARAMETER") sequentialSpecification: Class<*>) : SnapshotVerifier() { + override fun verifyResults(scenario: ExecutionScenario?, results: ExecutionResult?): Boolean { + checkForExceptions(results) + check(intArray === refIntArray) + check(intArray.contentEquals(intArrayOf(2, 1, 4, 3, 6, 5, 8, 7, 10, 9))) + + check(refArray === refRefArray) + check(refArray[0] == a && refArray[1] == b && refArray[2] == c) + check(a.x == 1 && b.x == 3 && c.x == 2) + return true + } + } + + override fun > O.customize() { + verifier(ArraysAPIVerifier::class.java) + actorsBefore(0) + actorsAfter(0) + iterations(100) + invocationsPerIteration(1) + threads(1) + actorsPerThread(1) + } + + @Operation + fun sort() { + intArray.sort() + refArray.sortBy { it.x } + } + + @Operation + fun arraySort() { + Arrays.sort(intArray) + Arrays.sort(refArray) { a, b -> a.x - b.x } + } + + @Operation + fun reverse() { + intArray.reverse() + refArray.reverse() + } + + @Operation + fun fill() { + intArray.fill(Random.nextInt()) + refArray.fill(Wrapper(Random.nextInt())) + } + + @Operation + fun arraysFill() { + Arrays.fill(intArray, Random.nextInt()) + Arrays.fill(refArray, Wrapper(Random.nextInt())) + } + + @Operation + fun arraysSetAll() { + Arrays.setAll(intArray) { Random.nextInt() } + Arrays.setAll(refArray) { Wrapper(Random.nextInt()) } + } + + @Operation + fun copyOf() { + val otherRefArray = refArray.copyOf() + otherRefArray[Random.nextInt(0, otherRefArray.size)] = Wrapper(Random.nextInt()) + otherRefArray[Random.nextInt(0, otherRefArray.size)].x = Random.nextInt() + } + + @Operation + fun arraysCopyOf() { + val otherRefArray = Arrays.copyOf(refArray, refArray.size + 1) + otherRefArray[Random.nextInt(0, otherRefArray.size)] = Wrapper(Random.nextInt()) + otherRefArray[Random.nextInt(0, otherRefArray.size)].x = Random.nextInt() + } +} \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/AtomicFUSnapshotTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/AtomicFUSnapshotTest.kt index 67b1bd49a..8ec452f8f 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/AtomicFUSnapshotTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/AtomicFUSnapshotTest.kt @@ -119,4 +119,121 @@ class AtomicFUSnapshotTest : AbstractSnapshotTest() { fun modifyAtomicFURefArrayValues() { atomicFURefArray[Random.nextInt(0, atomicFURefArray.size)].value!!.x = Random.nextInt() } +} + +class ImplicitAtomicFUSnapshotTest : AbstractSnapshotTest() { + companion object { + private class Wrapper(var x: Int) + + private val atomicFUInt = kotlinx.atomicfu.atomic(1) + private val atomicFURef = kotlinx.atomicfu.atomic(Wrapper(1)) + + private val atomicFUIntArray = kotlinx.atomicfu.AtomicIntArray(3) + private val atomicFURefArray = kotlinx.atomicfu.atomicArrayOfNulls(3) + + init { + for (i in 0..atomicFUIntArray.size - 1) { + atomicFUIntArray[i].value = i + 1 + } + + for (i in 0..atomicFURefArray.size - 1) { + atomicFURefArray[i].value = Wrapper(i + 1) + } + } + + // remember values to restore + private val atomicFURefValue = atomicFURef.value + private val atomicFUIntValues: List = mutableListOf().apply { + for (i in 0..atomicFUIntArray.size - 1) { + add(atomicFUIntArray[i].value) + } + } + private val atomicFURefArrayValues: List = mutableListOf().apply { + for (i in 0..atomicFURefArray.size - 1) { + add(atomicFURefArray[i].value!!) + } + } + } + + class ImplicitAtomicFUSnapshotVerifier(@Suppress("UNUSED_PARAMETER") sequentialSpecification: Class<*>) : SnapshotVerifier() { + override fun verifyResults(scenario: ExecutionScenario?, results: ExecutionResult?): Boolean { + checkForExceptions(results) + + check(atomicFUInt.value == 1) + + check(atomicFURef.value == atomicFURefValue) + check(atomicFURef.value.x == 1) + + for (i in 0..atomicFUIntArray.size - 1) { + check(atomicFUIntArray[i].value == atomicFUIntValues[i]) + } + + for (i in 0..atomicFURefArray.size - 1) { + check(atomicFURefArray[i].value == atomicFURefArrayValues[i]) + check(atomicFURefArray[i].value!!.x == i + 1) + } + + return true + } + } + + override fun > O.customize() { + verifier(ImplicitAtomicFUSnapshotVerifier::class.java) + threads(1) + iterations(100) + invocationsPerIteration(1) + actorsPerThread(10) + } + + @Operation + fun getAndSetAtomicFUInt() { + atomicFUInt.getAndSet(Random.nextInt()) + } + + @Operation + fun compareAndSetAtomicFUInt() { + atomicFUInt.compareAndSet(atomicFUInt.value, Random.nextInt()) + } + + @Operation + fun getAndIncrementAtomicFUInt() { + atomicFUInt.getAndIncrement() + } + + @Operation + fun getAndSetAtomicFURef() { + atomicFURef.getAndSet(Wrapper(Random.nextInt())) + } + + @Operation + fun compareAndSetAtomicFURef() { + atomicFURef.compareAndSet(atomicFURef.value, Wrapper(Random.nextInt())) + } + + @Operation + fun incrementAndGetAtomicFUIntArray() { + atomicFUIntArray[Random.nextInt(0, atomicFUIntArray.size)].incrementAndGet() + } + + @Operation + fun decrementAndGetAtomicFUIntArray() { + atomicFUIntArray[Random.nextInt(0, atomicFUIntArray.size)].decrementAndGet() + } + + @Operation + fun compareAndSetAtomicFUIntArray() { + val idx = Random.nextInt(0, atomicFUIntArray.size) + atomicFUIntArray[idx].compareAndSet(atomicFUIntArray[idx].value, Random.nextInt()) + } + + @Operation + fun getAndSetAtomicFURefArray() { + atomicFURefArray[Random.nextInt(0, atomicFURefArray.size)].getAndSet(Wrapper(Random.nextInt())) + } + + @Operation + fun compareAndSetAtomicFURefArray() { + val idx = Random.nextInt(0, atomicFURefArray.size) + atomicFURefArray[idx].compareAndSet(atomicFURefArray[idx].value, Wrapper(Random.nextInt())) + } } \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionSnapshotTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionSnapshotTest.kt index 669358aee..567e840e6 100644 --- a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionSnapshotTest.kt +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionSnapshotTest.kt @@ -17,6 +17,7 @@ import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedOptions import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions +import java.util.Collections import java.util.PriorityQueue import java.util.Queue import java.util.concurrent.ConcurrentHashMap diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionsAPISnapshotTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionsAPISnapshotTest.kt new file mode 100644 index 000000000..4caeb9bca --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/CollectionsAPISnapshotTest.kt @@ -0,0 +1,84 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.strategy.modelchecking.snapshot + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedOptions +import java.util.Collections +import kotlin.random.Random + + +class CollectionsAPISnapshotTest : AbstractSnapshotTest() { + private class Wrapper(var x: Int) + companion object { + private var intList = mutableListOf(2, 1, 4, 3, 6, 5, 8, 7, 10, 9) + private var refList = mutableListOf(Wrapper(1), Wrapper(3), Wrapper(2)) + + // save values to restore + private val refIntList = intList + private val refRefList = refList + private val a = refList[0] + private val b = refList[1] + private val c = refList[2] + } + + class CollectionsAPIVerifier(@Suppress("UNUSED_PARAMETER") sequentialSpecification: Class<*>) : SnapshotVerifier() { + override fun verifyResults(scenario: ExecutionScenario?, results: ExecutionResult?): Boolean { + checkForExceptions(results) + check(intList === refIntList) + check(intList.toIntArray().contentEquals(intArrayOf(2, 1, 4, 3, 6, 5, 8, 7, 10, 9))) + + check(refList === refRefList) + check(refList[0] == a && refList[1] == b && refList[2] == c) + check(a.x == 1 && b.x == 3 && c.x == 2) + return true + } + } + + override fun > O.customize() { + verifier(CollectionsAPIVerifier::class.java) + actorsBefore(0) + actorsAfter(0) + iterations(100) + invocationsPerIteration(1) + threads(1) + actorsPerThread(1) + } + + @Operation + fun sort() { + Collections.sort(intList) + Collections.sort(refList) { a, b -> a.x - b.x } + } + + @Operation + fun reverse() { + Collections.reverse(intList) + Collections.reverse(refList) + } + + @Operation + fun fill() { + Collections.fill(intList, Random.nextInt()) + Collections.fill(refList, Wrapper(Random.nextInt())) + } + + @Operation + fun copyOf() { + val otherRefList = MutableList(refList.size) { null } + Collections.copy(otherRefList, refList) + + otherRefList[Random.nextInt(0, otherRefList.size)] = Wrapper(Random.nextInt()) + otherRefList[Random.nextInt(0, otherRefList.size)]!!.x = Random.nextInt() + } +} \ No newline at end of file diff --git a/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/UnsafeModificationsSnapshotTest.kt b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/UnsafeModificationsSnapshotTest.kt new file mode 100644 index 000000000..ed0a0677b --- /dev/null +++ b/src/jvm/test/org/jetbrains/kotlinx/lincheck_test/strategy/modelchecking/snapshot/UnsafeModificationsSnapshotTest.kt @@ -0,0 +1,82 @@ +/* + * Lincheck + * + * Copyright (C) 2019 - 2024 JetBrains s.r.o. + * + * This Source Code Form is subject to the terms of the + * Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed + * with this file, You can obtain one at http://mozilla.org/MPL/2.0/. + */ + +package org.jetbrains.kotlinx.lincheck_test.strategy.modelchecking.snapshot + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult +import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario +import org.jetbrains.kotlinx.lincheck.strategy.managed.ManagedOptions +import org.jetbrains.kotlinx.lincheck.util.UnsafeHolder +import org.jetbrains.kotlinx.lincheck.util.getArrayElementOffsetViaUnsafe +import org.jetbrains.kotlinx.lincheck.util.getFieldOffsetViaUnsafe +import kotlin.random.Random +import kotlin.reflect.jvm.javaField + + +@Suppress("DEPRECATION") // Unsafe +class UnsafeModificationsSnapshotTest : AbstractSnapshotTest() { + private class Wrapper(var x: Int) + companion object { + private var value = 1 + private var ref = Wrapper(1) + private var intArray = intArrayOf(1, 2, 3) + + // remember values for restoring + private val initRef = ref + private val initIntArray = intArray + } + + private val U = UnsafeHolder.UNSAFE + private val valueBase = U.staticFieldBase(UnsafeModificationsSnapshotTest.Companion::value.javaField!!) + private val valueOffset = getFieldOffsetViaUnsafe(UnsafeModificationsSnapshotTest.Companion::value.javaField!!) + + private val refBase = U.staticFieldBase(UnsafeModificationsSnapshotTest.Companion::ref.javaField!!) + private val refOffset = getFieldOffsetViaUnsafe(UnsafeModificationsSnapshotTest.Companion::ref.javaField!!) + + class UnsafeModificationsVerifier(@Suppress("UNUSED_PARAMETER") sequentialSpecification: Class<*>) : SnapshotVerifier() { + override fun verifyResults(scenario: ExecutionScenario?, results: ExecutionResult?): Boolean { + checkForExceptions(results) + check(value == 1) + check(ref === initRef && ref.x == 1) + check(intArray === initIntArray && intArray.contentEquals(intArrayOf(1, 2, 3))) + return true + } + } + + override fun > O.customize() { + verifier(UnsafeModificationsVerifier::class.java) + iterations(100) + invocationsPerIteration(1) + threads(1) + actorsPerThread(10) + } + + @Operation + fun putValue() { + U.putInt(valueBase, valueOffset, Random.nextInt()) + } + + @Operation + fun putRef() { + U.putObject(refBase, refOffset, Wrapper(Random.nextInt())) + } + + @Operation + fun putIntArray() { + val index = Random.nextInt(0, intArray.size) + U.putInt(intArray, getArrayElementOffsetViaUnsafe(intArray, index), Random.nextInt()) + } + + @Operation + fun assignIntArray() { + intArray = intArrayOf(Random.nextInt(), Random.nextInt(), Random.nextInt()) + } +}