Add an option to check whether equals/hashCode methods (used for stat…

…es equivalence relation in verifiers) are defined correctly

Co-authored-by: sokolova <[email protected]>

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDequeTest.kt

@@ -6,7 +6,7 @@ import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.RandomSwitchCTest
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest
 import org.junit.Test
 
-@StressCTest
+@StressCTest(requireStateEquivalenceImplCheck = false)
 class DequeLinearizabilityTest {
     private val deque = LockFreeDeque<Int>();
 

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterGetTest.java

@@ -25,11 +25,12 @@
 import org.jetbrains.kotlinx.lincheck.LinChecker;
 import org.jetbrains.kotlinx.lincheck.annotations.Operation;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
+import org.jetbrains.kotlinx.lincheck.verifier.VerifierState;
 import org.junit.Test;
 import tests.custom.counter.CounterGet;
 
 @StressCTest
-public class CounterGetTest {
+public class CounterGetTest extends VerifierState {
     private CounterGet counter = new CounterGet();;
 
     @Operation
@@ -46,4 +47,9 @@ public int get() {
     public void test() {
         LinChecker.check(CounterGetTest.class);
     }
+
+    @Override
+    protected Object extractState() {
+        return counter.get();
+    }
 }

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong3.java

@@ -32,7 +32,7 @@
 import tests.custom.queue.QueueEmptyException;
 import tests.custom.queue.QueueWrong3;
 
-@StressCTest
+@StressCTest(requireStateEquivalenceImplCheck = false)
 public class WrapperQueueWrong3 {
     private Queue queue = new QueueWrong3(10);
 

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/transfer/AccountsTest.java

@@ -58,7 +58,7 @@ public AccountsTest(Supplier<Accounts> accountCreator, String desc) {
         AccountsTest.accountCreator = accountCreator;
     }
 
-    @StressCTest(threads = 3)
+    @StressCTest(threads = 3, requireStateEquivalenceImplCheck = false)
     @Param(name = "id", gen = IntGen.class, conf = "1:4")
     @Param(name = "amount", gen = IntGen.class)
     public static class AccountsLinearizabilityTest {

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/hash_map/HashMapTest.java

@@ -22,11 +22,13 @@
  * #L%
  */
 
+import org.jetbrains.annotations.NotNull;
 import org.jetbrains.kotlinx.lincheck.LinChecker;
 import org.jetbrains.kotlinx.lincheck.annotations.Operation;
 import org.jetbrains.kotlinx.lincheck.annotations.Param;
 import org.jetbrains.kotlinx.lincheck.paramgen.IntGen;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
+import org.jetbrains.kotlinx.lincheck.verifier.VerifierState;
 import org.junit.Test;
 
 import java.util.HashMap;
@@ -35,7 +37,7 @@
 @StressCTest
 @Param(name = "key", gen = IntGen.class)
 @Param(name = "value", gen = IntGen.class)
-public class HashMapTest {
+public class HashMapTest extends VerifierState {
     private Map<Integer, Integer> m = new HashMap<>();
 
     @Operation(params = {"key", "value"})
@@ -52,5 +54,10 @@ public Integer get(@Param(name = "key") Integer key) {
     public void test() throws Exception {
         LinChecker.check(HashMapTest.class);
     }
+
+    @Override
+    protected Object extractState() {
+        return m;
+    }
 }
 

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/ConcurrentDequeStressTest.kt

@@ -30,5 +30,5 @@ class ConcurrentDequeStressTest : VerifierState() {
     @Test(expected = AssertionError::class)
     fun test() = LinChecker.check(ConcurrentDequeStressTest::class.java)
 
-    override fun extractState() = deque
+    override fun extractState() = deque.toList()
 }

libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/MutexStressTest.kt

@@ -13,7 +13,7 @@ import org.junit.Test
 import java.lang.IllegalStateException
 
 @Param(name = "value", gen = IntGen::class, conf = "1:5")
-@StressCTest(actorsPerThread = 10, threads = 2, invocationsPerIteration = 10000, iterations = 100, actorsBefore = 10, actorsAfter = 0)
+@StressCTest(actorsPerThread = 10, threads = 2, invocationsPerIteration = 10000, iterations = 100, actorsBefore = 10, actorsAfter = 0, requireStateEquivalenceImplCheck = false)
 class MutexStressTest : VerifierState() {
     val mutex = Mutex(true)
 

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/CTestConfiguration.java

@@ -22,15 +22,15 @@
  * #L%
  */
 
+import org.jetbrains.kotlinx.lincheck.annotations.Operation;
 import org.jetbrains.kotlinx.lincheck.execution.ExecutionGenerator;
 import org.jetbrains.kotlinx.lincheck.execution.RandomExecutionGenerator;
 import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.RandomSwitchCTest;
 import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.RandomSwitchCTestConfiguration;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest;
 import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTestConfiguration;
-import org.jetbrains.kotlinx.lincheck.annotations.*;
 import org.jetbrains.kotlinx.lincheck.verifier.Verifier;
-import org.jetbrains.kotlinx.lincheck.verifier.quantitative.QuantitativelyRelaxedLinearizabilityVerifier;
+import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier;
 
 import java.util.Arrays;
 import java.util.List;
@@ -48,7 +48,7 @@ public abstract class CTestConfiguration {
     public static final int DEFAULT_ACTORS_BEFORE = 5;
     public static final int DEFAULT_ACTORS_AFTER = 5;
     public static final Class<? extends ExecutionGenerator> DEFAULT_EXECUTION_GENERATOR = RandomExecutionGenerator.class;
-    public static final Class<? extends Verifier> DEFAULT_VERIFIER = QuantitativelyRelaxedLinearizabilityVerifier.class;
+    public static final Class<? extends Verifier> DEFAULT_VERIFIER = LinearizabilityVerifier.class;
 
     public final int iterations;
     public final int threads;
@@ -58,9 +58,10 @@ public abstract class CTestConfiguration {
     public final Class<? extends ExecutionGenerator> generatorClass;
     public final Class<? extends Verifier> verifierClass;
     public boolean hasTestClassSuspendableActors;
+    public final boolean requireStateEquivalenceImplCheck;
 
     protected CTestConfiguration(int iterations, int threads, int actorsPerThread, int actorsBefore, int actorsAfter,
-        Class<? extends ExecutionGenerator> generatorClass, Class<? extends Verifier> verifierClass)
+        Class<? extends ExecutionGenerator> generatorClass, Class<? extends Verifier> verifierClass, boolean requireStateEquivalenceImplCheck)
     {
         this.iterations = iterations;
         this.threads = threads;
@@ -69,6 +70,7 @@ protected CTestConfiguration(int iterations, int threads, int actorsPerThread, i
         this.actorsAfter = actorsAfter;
         this.generatorClass = generatorClass;
         this.verifierClass = verifierClass;
+        this.requireStateEquivalenceImplCheck = requireStateEquivalenceImplCheck;
     }
 
     static List<CTestConfiguration> createFromTestClass(Class<?> testClass) {
@@ -81,7 +83,7 @@ static List<CTestConfiguration> createFromTestClass(Class<?> testClass) {
                 }
                 return new StressCTestConfiguration(ann.iterations(),
                         ann.threads(), ann.actorsPerThread(), ann.actorsBefore(), ann.actorsAfter(),
-                        ann.generator(), ann.verifier(), ann.invocationsPerIteration(), true);
+                        ann.generator(), ann.verifier(), ann.invocationsPerIteration(), true, ann.requireStateEquivalenceImplCheck());
             });
         Stream<RandomSwitchCTestConfiguration> randomSwitchConfigurations = Arrays.stream(testClass.getAnnotationsByType(RandomSwitchCTest.class))
             .map(ann -> {
@@ -90,7 +92,7 @@ static List<CTestConfiguration> createFromTestClass(Class<?> testClass) {
                 }
                 return new RandomSwitchCTestConfiguration(ann.iterations(),
                         ann.threads(), ann.actorsPerThread(), ann.actorsBefore(), ann.actorsAfter(),
-                        ann.generator(), ann.verifier(), ann.invocationsPerIteration());
+                        ann.generator(), ann.verifier(), ann.invocationsPerIteration(), ann.requireStateEquivalenceImplCheck());
             });
         return Stream.concat(stressConfigurations, randomSwitchConfigurations).collect(Collectors.toList());
     }

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.java

@@ -10,28 +10,27 @@
  * it under the terms of the GNU Lesser General Public License as
  * published by the Free Software Foundation, either version 3 of the
  * License, or (at your option) any later version.
- * 
+ *
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Lesser Public License for more details.
- * 
+ *
  * You should have received a copy of the GNU General Lesser Public
  * License along with this program.  If not, see
  * <http://www.gnu.org/licenses/lgpl-3.0.html>.
  * #L%
  */
 
 import org.jetbrains.kotlinx.lincheck.annotations.LogLevel;
-import org.jetbrains.kotlinx.lincheck.execution.ExecutionGenerator;
-import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario;
+import org.jetbrains.kotlinx.lincheck.execution.*;
 import org.jetbrains.kotlinx.lincheck.strategy.Strategy;
-import org.jetbrains.kotlinx.lincheck.verifier.Verifier;
-
-import java.util.*;
-
+import org.jetbrains.kotlinx.lincheck.verifier.*;
+import org.jetbrains.kotlinx.lincheck.verifier.quantitative.QuantitativeRelaxationVerifierConf;
 import static org.jetbrains.kotlinx.lincheck.ActorKt.isSuspendable;
 import static org.jetbrains.kotlinx.lincheck.ReporterKt.DEFAULT_LOG_LEVEL;
+import static org.jetbrains.kotlinx.lincheck.UtilsKt.createTestInstance;
+import java.util.*;
 
 
 /**
@@ -49,7 +48,7 @@ private LinChecker(Class<?> testClass, Options options) {
         this.testStructure = CTestStructure.getFromTestClass(testClass);
         LoggingLevel logLevel;
         if (options != null) {
-            logLevel= options.logLevel;
+            logLevel = options.logLevel;
             this.testConfigurations = Collections.singletonList(options.createTestConfigurations());
         } else {
             logLevel = getLogLevelFromAnnotation();
@@ -97,6 +96,7 @@ private void check() throws AssertionError {
     }
 
     private void checkImpl(CTestConfiguration testCfg) throws AssertionError, Exception {
+        if (testCfg.requireStateEquivalenceImplCheck) checkStateEquivalenceImpl(testClass);
         ExecutionGenerator exGen = createExecutionGenerator(testCfg.generatorClass, testCfg);
         // Run iterations
         for (int iteration = 1; iteration <= testCfg.iterations; iteration++) {
@@ -110,6 +110,20 @@ private void checkImpl(CTestConfiguration testCfg) throws AssertionError, Except
         }
     }
 
+    private void checkStateEquivalenceImpl(Class<?> testClass) {
+        if (!testClass.isAnnotationPresent(QuantitativeRelaxationVerifierConf.class)) {
+            Object i1 = createTestInstance(testClass);
+            Object i2 = createTestInstance(testClass);
+            if (i1.hashCode() != i2.hashCode() || !i1.equals(i2)) {
+                throw new IllegalStateException(
+                    "equals() and hashCode() methods for this test are not defined or defined incorrectly.\n" +
+                    "It is more convenient to make the test class extend `VerifierState` class and override `extractState()` function to define equals() and hashCode() methods.\n" +
+                    "This check may be suppressed by setting the requireStateEquivalenceImplementationCheck option to false."
+                );
+            }
+        }
+    }
+
     private void validateScenario(CTestConfiguration testCfg, ExecutionScenario scenario) {
         if (testCfg.hasTestClassSuspendableActors) {
             if (scenario.initExecution.stream().anyMatch(actor -> isSuspendable(actor.getMethod())))
@@ -120,17 +134,15 @@ private void validateScenario(CTestConfiguration testCfg, ExecutionScenario scen
     }
 
     private Verifier createVerifier(Class<? extends Verifier> verifierClass, ExecutionScenario scenario,
-        Class<?> testClass) throws Exception
-    {
+                                    Class<?> testClass) throws Exception {
         return verifierClass.getConstructor(ExecutionScenario.class, Class.class)
-            .newInstance(scenario, testClass);
+                .newInstance(scenario, testClass);
     }
 
     private ExecutionGenerator createExecutionGenerator(Class<? extends ExecutionGenerator> generatorClass,
-        CTestConfiguration testConfiguration) throws Exception
-    {
+                                                        CTestConfiguration testConfiguration) throws Exception {
         return generatorClass.getConstructor(CTestConfiguration.class, CTestStructure.class)
-            .newInstance(testConfiguration, testStructure);
+                .newInstance(testConfiguration, testStructure);
     }
 
     private LoggingLevel getLogLevelFromAnnotation() {

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Options.java

@@ -41,6 +41,7 @@ public abstract class Options<OPT extends Options, CTEST extends CTestConfigurat
     protected int actorsAfter = CTestConfiguration.DEFAULT_ACTORS_AFTER;
     protected Class<? extends ExecutionGenerator> executionGenerator = CTestConfiguration.DEFAULT_EXECUTION_GENERATOR;
     protected Class<? extends Verifier> verifier = CTestConfiguration.DEFAULT_VERIFIER;
+    protected boolean requireStateEquivalenceImplementationCheck = true;
 
     /**
      * Number of different test scenarios to be executed
@@ -118,6 +119,16 @@ public OPT verifier(Class<? extends Verifier> verifier) {
         return (OPT) this;
     }
 
+    /**
+     * Require correctness check of test instance state equivalency relation defined by the user.
+     * It checks whether two new instances of a test class are equal.
+     * If the check fails [{@link IllegalStateException}] is thrown.
+     */
+    public OPT requireStateEquivalenceImplCheck(boolean require) {
+        this.requireStateEquivalenceImplementationCheck = require;
+        return (OPT) this;
+    }
+
     public abstract CTEST createTestConfigurations();
 
     /**

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchCTest.java

@@ -100,6 +100,13 @@
      */
     Class<? extends Verifier> verifier() default LinearizabilityVerifier.class;
 
+    /**
+     * Require correctness check of test instance state equivalency relation, which is defined by the user.
+     * Essentially, it checks whether two new instances of the test class are equal.
+     * If the check fails. an [{@link IllegalStateException}] is thrown.
+     */
+    boolean requireStateEquivalenceImplCheck() default true;
+
     /**
      * Holder annotation for {@link RandomSwitchCTest}.
      * Not a public API.

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchCTestConfiguration.java

@@ -35,9 +35,9 @@ public class RandomSwitchCTestConfiguration extends CTestConfiguration {
 
     public RandomSwitchCTestConfiguration(int iterations, int threads, int actorsPerThread, int actorsBefore,
         int actorsAfter, Class<? extends ExecutionGenerator> generatorClass, Class<? extends Verifier> verifierClass,
-        int invocationsPerIteration)
+        int invocationsPerIteration, boolean requireStateEquivalenceCheck)
     {
-        super(iterations, threads, actorsPerThread, actorsBefore, actorsAfter, generatorClass, verifierClass);
+        super(iterations, threads, actorsPerThread, actorsBefore, actorsAfter, generatorClass, verifierClass, requireStateEquivalenceCheck);
         this.invocationsPerIteration = invocationsPerIteration;
     }
 }

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchOptions.java

@@ -41,6 +41,6 @@ public RandomSwitchOptions invocationsPerIteration(int invocations) {
     @Override
     public RandomSwitchCTestConfiguration createTestConfigurations() {
         return new RandomSwitchCTestConfiguration(iterations, threads, actorsPerThread, actorsBefore, actorsAfter,
-            executionGenerator, verifier, invocationsPerIteration);
+            executionGenerator, verifier, invocationsPerIteration, requireStateEquivalenceImplementationCheck);
     }
 }

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTest.java

@@ -100,6 +100,13 @@
      */
     Class<? extends Verifier> verifier() default LinearizabilityVerifier.class;
 
+    /**
+     * Require correctness check of test instance state equivalency relation, which is defined by the user.
+     * Essentially, it checks whether two new instances of the test class are equal.
+     * If the check fails. an [{@link IllegalStateException}] is thrown.
+     */
+    boolean requireStateEquivalenceImplCheck() default true;
+
     /**
      * Holder annotation for {@link StressCTest}.
      * Not a public API.

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressCTestConfiguration.java

@@ -37,9 +37,9 @@ public class StressCTestConfiguration extends CTestConfiguration {
 
     public StressCTestConfiguration(int iterations, int threads, int actorsPerThread, int actorsBefore, int actorsAfter,
         Class<? extends ExecutionGenerator> generatorClass, Class<? extends Verifier> verifierClass,
-        int invocationsPerIteration, boolean addWaits)
+        int invocationsPerIteration, boolean addWaits, boolean requireStateEquivalenceCheck)
     {
-        super(iterations, threads, actorsPerThread, actorsBefore, actorsAfter, generatorClass, verifierClass);
+        super(iterations, threads, actorsPerThread, actorsBefore, actorsAfter, generatorClass, verifierClass, requireStateEquivalenceCheck);
         this.invocationsPerIteration = invocationsPerIteration;
         this.addWaits = addWaits;
     }

lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressOptions.java

@@ -50,6 +50,6 @@ public StressOptions addWaits(boolean value) {
     @Override
     public StressCTestConfiguration createTestConfigurations() {
         return new StressCTestConfiguration(iterations, threads, actorsPerThread, actorsBefore, actorsAfter,
-            executionGenerator, verifier, invocationsPerIteration, addWaits);
+            executionGenerator, verifier, invocationsPerIteration, addWaits, requireStateEquivalenceImplementationCheck);
     }
 }

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ExceptionAsResultTest.java

@@ -29,7 +29,7 @@
 
 import java.io.IOException;
 
-@StressCTest(iterations = 1)
+@StressCTest(iterations = 1, requireStateEquivalenceImplCheck = false)
 public class ExceptionAsResultTest {
     @Operation(handleExceptionsAsResult = NullPointerException.class)
     public void npeIsOk() {

lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/NonParallelOpGroupTest.java

@@ -37,7 +37,7 @@
 
 @OpGroupConfig(name = "producer", nonParallel = true)
 @OpGroupConfig(name = "consumer", nonParallel = true)
-@StressCTest
+@StressCTest(requireStateEquivalenceImplCheck = false)
 @LogLevel(LoggingLevel.DEBUG)
 public class NonParallelOpGroupTest {
     private SpscLinkedAtomicQueue<Integer> queue = new SpscLinkedAtomicQueue<>();