kotlinx-lincheck icon indicating copy to clipboard operation
kotlinx-lincheck copied to clipboard

[2.30] LincheckAssertionError: The execution has hung

Open ben-manes opened this issue 10 months ago • 3 comments

When I attempted to upgrade from 2.29 to 2.30 and the caffeine tests failed. I then reduced the test to use ConcurrentHashMap directly which produced different errors, but may have the same root cause. I can say that while the table operations are atomic, the size counter is not so addCount is not linearizable, but that shouldn't be a problem since Map.size() is not an observed operation.

Minimal Test
import java.util.Map;
import java.util.concurrent.ConcurrentHashMap;
import java.util.concurrent.ConcurrentMap;

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.managed.modelchecking.ModelCheckingOptions;
import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions;
import org.testng.annotations.Test;

/**
 * Linearizability checks. This property is guaranteed for per-key operations in the absence of
 * evictions, refresh, and other non-deterministic features. This property is not supported by
 * operations that span across multiple entries such as {@link Map#isEmpty()}, {@link Map#size()},
 * and {@link Map#clear()}.
 */
@Param(name = "key", gen = IntGen.class, conf = "1:5")
@Param(name = "value", gen = IntGen.class, conf = "1:10")
public final class LincheckMapTest {
  private final ConcurrentMap<Integer, Integer> map;

  public LincheckMapTest() {
    map = new ConcurrentHashMap<>();
  }

  /**
   * This test checks linearizability with bounded model checking. Unlike stress testing, this
   * approach can also provide a trace of an incorrect execution. However, it uses sequential
   * consistency model, so it can not find any low-level bugs (e.g., missing 'volatile'), and thus,
   * it is recommended to have both test modes.
   */
  @Test(groups = "lincheck")
  public void modelCheckingTest() {
    var options = new ModelCheckingOptions()
        .iterations(100)                 // the number of different scenarios
        .invocationsPerIteration(1_000); // how deeply each scenario is tested
    new LinChecker(getClass(), options).check();
  }

  /** This test checks linearizability with stress testing. */
  @Test(groups = "lincheck")
  public void stressTest() {
    var options = new StressOptions()
        .iterations(100)                  // the number of different scenarios
        .invocationsPerIteration(10_000); // how deeply each scenario is tested
    new LinChecker(getClass(), options).check();
  }

  /* --------------- Concurrent Map --------------- */

  @Operation
  public boolean containsKey(@Param(name = "key") int key) {
    return map.containsKey(key);
  }

  @Operation
  public boolean containsValue(@Param(name = "value") int value) {
    return map.containsValue(value);
  }

  @Operation
  public Integer get_asMap(@Param(name = "key") int key) {
    return map.get(key);
  }

  @Operation
  public Integer put_asMap(@Param(name = "key") int key, @Param(name = "value") int value) {
    return map.put(key, value);
  }

  @Operation
  public Integer putIfAbsent(@Param(name = "key") int key, @Param(name = "value") int value) {
    return map.putIfAbsent(key, value);
  }

  @Operation
  public Integer replace(@Param(name = "key") int key, @Param(name = "value") int nextValue) {
    return map.replace(key, nextValue);
  }

  @Operation
  public boolean replaceConditionally(@Param(name = "key") int key,
      @Param(name = "value") int previousValue, @Param(name = "value") int nextValue) {
    return map.replace(key, previousValue, nextValue);
  }

  @Operation
  public Integer remove(@Param(name = "key") int key) {
    return map.remove(key);
  }

  @Operation
  public boolean removeConditionally(@Param(name = "key") int key,
      @Param(name = "value") int previousValue) {
    return map.remove(key, previousValue);
  }

  @Operation
  public Integer computeIfAbsent(@Param(name = "key") int key,
      @Param(name = "value") int nextValue) {
    return map.computeIfAbsent(key, k -> nextValue);
  }

  @Operation
  public Integer computeIfPresent(@Param(name = "key") int key,
      @Param(name = "value") int nextValue) {
    return map.computeIfPresent(key, (k, v) -> nextValue);
  }

  @Operation
  public Integer compute(@Param(name = "key") int key, @Param(name = "value") int nextValue) {
    return map.compute(key, (k, v) -> nextValue);
  }

  @Operation
  public Integer merge(@Param(name = "key") int key, @Param(name = "value") int nextValue) {
    return map.merge(key, nextValue, (k, v) -> v + nextValue);
  }
}
Test Failure
org.jetbrains.kotlinx.lincheck.LincheckAssertionError: 
= Invalid execution results =
| ------------------------------------------------------- |
|        Thread 1         |           Thread 2            |
| ------------------------------------------------------- |
| merge(4, 9): 9          |                               |
| ------------------------------------------------------- |
| putIfAbsent(2, 2): null | containsValue(6): false [2,0] |
| replace(4, 6): 9 [1,0]  |                               |
| merge(2, 3): 6 [2,0]    |                               |
| remove(4): 6 [3,0]      |                               |
| ------------------------------------------------------- |

---
All operations above the horizontal line | ----- | happen before those below the line
---
Values in "[..]" brackets indicate the number of completed operations
in each of the parallel threads seen at the beginning of the current operation
---

The following interleaving leads to the error:
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
|                                      Thread 1                                       |                                             Thread 2                                             |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| merge(4, 9): 9                                                                      |                                                                                                  |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| putIfAbsent(2, 2): null                                                             |                                                                                                  |
| replace(4, 6): 9                                                                    |                                                                                                  |
| merge(2, 3): 6                                                                      |                                                                                                  |
|   table.READ: Node[]#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2025)      |                                                                                                  |
|   switch                                                                            |                                                                                                  |
|                                                                                     | containsValue(6): false                                                                          |
|                                                                                     |   table.READ: Node[]#1 at ConcurrentHashMap.containsValue(ConcurrentHashMap.java:981)            |
|                                                                                     |   advance(): Node#1 at ConcurrentHashMap.containsValue(ConcurrentHashMap.java:983)               |
|                                                                                     |   advance(): null at ConcurrentHashMap.containsValue(ConcurrentHashMap.java:983)                 |
|                                                                                     |     tabAt(Node[]#1,3): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     switch                                                                                       |
|   tabAt(Node[]#1,2): Node#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2029) |                                                                                                  |
|   MONITORENTER at ConcurrentHashMap.merge(ConcurrentHashMap.java:2039)              |                                                                                                  |
|   tabAt(Node[]#1,2): Node#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2040) |                                                                                                  |
|   MONITOREXIT at ConcurrentHashMap.merge(ConcurrentHashMap.java:2095)               |                                                                                                  |
|   result: 6                                                                         |                                                                                                  |
| remove(4): 6                                                                        |                                                                                                  |
|                                                                                     |     tabAt(Node[]#1,4): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     tabAt(Node[]#1,5): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     tabAt(Node[]#1,6): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     tabAt(Node[]#1,7): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     tabAt(Node[]#1,8): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     tabAt(Node[]#1,9): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                     |     tabAt(Node[]#1,10): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                     |     tabAt(Node[]#1,11): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                     |     tabAt(Node[]#1,12): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                     |     tabAt(Node[]#1,13): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                     |     tabAt(Node[]#1,14): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                     |     tabAt(Node[]#1,15): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                     |   result: false                                                                                  |
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |

Detailed trace:
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
|                                                Thread 1                                                |                                             Thread 2                                              |
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| merge(4, 9): 9                                                                                         |                                                                                                   |
|   table.READ: null at ConcurrentHashMap.merge(ConcurrentHashMap.java:2025)                             |                                                                                                   |
|   initTable(): Node[]#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2028)                        |                                                                                                   |
|     table.READ: null at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2285)                       |                                                                                                   |
|     sizeCtl.READ: 0 at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2286)                        |                                                                                                   |
|     compareAndSetInt(0,-1): true at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2288)           |                                                                                                   |
|     table.READ: null at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2290)                       |                                                                                                   |
|     table.WRITE(Node[]#1) at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2294)                  |                                                                                                   |
|     sizeCtl.WRITE(12) at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2298)                      |                                                                                                   |
|   tabAt(Node[]#1,4): null at ConcurrentHashMap.merge(ConcurrentHashMap.java:2029)                      |                                                                                                   |
|     getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                    |                                                                                                   |
|   casTabAt(Node[]#1,4,null,Node#2): true at ConcurrentHashMap.merge(ConcurrentHashMap.java:2030)       |                                                                                                   |
|     compareAndSetObject(null,Node#2): true at ConcurrentHashMap.casTabAt(ConcurrentHashMap.java:765)   |                                                                                                   |
|   addCount(1,0) at ConcurrentHashMap.merge(ConcurrentHashMap.java:2104)                                |                                                                                                   |
|     counterCells.READ: null at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2318)                 |                                                                                                   |
|     baseCount.READ: 0 at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2318)                       |                                                                                                   |
|     compareAndSetLong(0,1): true at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2319)            |                                                                                                   |
|     sizeCtl.READ: 12 at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2335)                        |                                                                                                   |
|   result: 9                                                                                            |                                                                                                   |
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| putIfAbsent(2, 2): null                                                                                |                                                                                                   |
|   putVal(2,2,true): null at ConcurrentHashMap.putIfAbsent(ConcurrentHashMap.java:1541)                 |                                                                                                   |
|     table.READ: Node[]#1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1014)                      |                                                                                                   |
|     tabAt(Node[]#1,2): null at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1018)                   |                                                                                                   |
|       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                  |                                                                                                   |
|     casTabAt(Node[]#1,2,null,Node#1): true at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1019)    |                                                                                                   |
|       compareAndSetObject(null,Node#1): true at ConcurrentHashMap.casTabAt(ConcurrentHashMap.java:765) |                                                                                                   |
|     addCount(1,0) at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1075)                             |                                                                                                   |
|       counterCells.READ: null at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2318)               |                                                                                                   |
|       baseCount.READ: 1 at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2318)                     |                                                                                                   |
|       compareAndSetLong(1,2): true at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2319)          |                                                                                                   |
|       sizeCtl.READ: 12 at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2335)                      |                                                                                                   |
|   result: null                                                                                         |                                                                                                   |
| replace(4, 6): 9                                                                                       |                                                                                                   |
|   replaceNode(4,6,null): 9 at ConcurrentHashMap.replace(ConcurrentHashMap.java:1576)                   |                                                                                                   |
|     table.READ: Node[]#1 at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1112)                 |                                                                                                   |
|     tabAt(Node[]#1,4): Node#2 at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1115)            |                                                                                                   |
|       getObjectAcquire(): Node#2 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                |                                                                                                   |
|     MONITORENTER at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1122)                         |                                                                                                   |
|     tabAt(Node[]#1,4): Node#2 at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1123)            |                                                                                                   |
|       getObjectAcquire(): Node#2 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                |                                                                                                   |
|     MONITOREXIT at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1169)                          |                                                                                                   |
|   result: 9                                                                                            |                                                                                                   |
| merge(2, 3): 6                                                                                         |                                                                                                   |
|   table.READ: Node[]#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2025)                         |                                                                                                   |
|   switch                                                                                               |                                                                                                   |
|                                                                                                        | containsValue(6): false                                                                           |
|                                                                                                        |   table.READ: Node[]#1 at ConcurrentHashMap.containsValue(ConcurrentHashMap.java:981)             |
|                                                                                                        |   advance(): Node#1 at ConcurrentHashMap.containsValue(ConcurrentHashMap.java:983)                |
|                                                                                                        |     tabAt(Node[]#1,0): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,1): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,2): Node#1 at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358) |
|                                                                                                        |       getObjectAcquire(): Node#1 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)           |
|                                                                                                        |   advance(): null at ConcurrentHashMap.containsValue(ConcurrentHashMap.java:983)                  |
|                                                                                                        |     tabAt(Node[]#1,3): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     switch                                                                                        |
|   tabAt(Node[]#1,2): Node#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2029)                    |                                                                                                   |
|     getObjectAcquire(): Node#1 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                  |                                                                                                   |
|   MONITORENTER at ConcurrentHashMap.merge(ConcurrentHashMap.java:2039)                                 |                                                                                                   |
|   tabAt(Node[]#1,2): Node#1 at ConcurrentHashMap.merge(ConcurrentHashMap.java:2040)                    |                                                                                                   |
|     getObjectAcquire(): Node#1 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                  |                                                                                                   |
|   MONITOREXIT at ConcurrentHashMap.merge(ConcurrentHashMap.java:2095)                                  |                                                                                                   |
|   result: 6                                                                                            |                                                                                                   |
| remove(4): 6                                                                                           |                                                                                                   |
|   replaceNode(4,null,null): 6 at ConcurrentHashMap.remove(ConcurrentHashMap.java:1102)                 |                                                                                                   |
|     table.READ: Node[]#1 at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1112)                 |                                                                                                   |
|     tabAt(Node[]#1,4): Node#2 at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1115)            |                                                                                                   |
|       getObjectAcquire(): Node#2 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                |                                                                                                   |
|     MONITORENTER at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1122)                         |                                                                                                   |
|     tabAt(Node[]#1,4): Node#2 at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1123)            |                                                                                                   |
|       getObjectAcquire(): Node#2 at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)                |                                                                                                   |
|     setTabAt(Node[]#1,4,null) at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1140)            |                                                                                                   |
|       putObjectRelease(null) at ConcurrentHashMap.setTabAt(ConcurrentHashMap.java:769)                 |                                                                                                   |
|     MONITOREXIT at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1169)                          |                                                                                                   |
|     addCount(-1,-1) at ConcurrentHashMap.replaceNode(ConcurrentHashMap.java:1173)                      |                                                                                                   |
|       counterCells.READ: null at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2318)               |                                                                                                   |
|       baseCount.READ: 2 at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2318)                     |                                                                                                   |
|       compareAndSetLong(2,1): true at ConcurrentHashMap.addCount(ConcurrentHashMap.java:2319)          |                                                                                                   |
|   result: 6                                                                                            |                                                                                                   |
|                                                                                                        |     tabAt(Node[]#1,4): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,5): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,6): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,7): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,8): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,9): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)   |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,10): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,11): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,12): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,13): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,14): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |     tabAt(Node[]#1,15): null at ConcurrentHashMap$Traverser.advance(ConcurrentHashMap.java:3358)  |
|                                                                                                        |       getObjectAcquire(): null at ConcurrentHashMap.tabAt(ConcurrentHashMap.java:760)             |
|                                                                                                        |   result: false                                                                                   |
| ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |

	at app//org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt:45)
	at app//com.github.benmanes.caffeine.lincheck.LincheckMapTest.modelCheckingTest(Unknown Source)
	at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at [email protected]/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at [email protected]/java.lang.reflect.Method.invoke(Method.java:566)
	at app//org.testng.internal.invokers.MethodInvocationHelper.invokeMethod(MethodInvocationHelper.java:141)
	at app//org.testng.internal.invokers.TestInvoker.invokeMethod(TestInvoker.java:686)
	at app//org.testng.internal.invokers.TestInvoker.invokeTestMethod(TestInvoker.java:230)
	at app//org.testng.internal.invokers.MethodRunner.runInSequence(MethodRunner.java:63)
	at app//org.testng.internal.invokers.TestInvoker$MethodInvocationAgent.invoke(TestInvoker.java:992)
	at app//org.testng.internal.invokers.TestInvoker.invokeTestMethods(TestInvoker.java:203)
	at app//org.testng.internal.invokers.TestMethodWorker.invokeTestMethods(TestMethodWorker.java:154)
	at app//org.testng.internal.invokers.TestMethodWorker.run(TestMethodWorker.java:134)
	at [email protected]/java.util.ArrayList.forEach(ArrayList.java:1541)
	at app//org.testng.TestRunner.privateRun(TestRunner.java:739)
	at app//org.testng.TestRunner.run(TestRunner.java:614)
	at app//org.testng.SuiteRunner.runTest(SuiteRunner.java:421)
	at app//org.testng.SuiteRunner.runSequentially(SuiteRunner.java:413)
	at app//org.testng.SuiteRunner.privateRun(SuiteRunner.java:373)
	at app//org.testng.SuiteRunner.run(SuiteRunner.java:312)
	at app//org.testng.SuiteRunnerWorker.runSuite(SuiteRunnerWorker.java:52)
	at app//org.testng.SuiteRunnerWorker.run(SuiteRunnerWorker.java:95)
	at app//org.testng.TestNG.runSuitesSequentially(TestNG.java:1274)
	at app//org.testng.TestNG.runSuitesLocally(TestNG.java:1208)
	at app//org.testng.TestNG.runSuites(TestNG.java:1112)
	at app//org.testng.TestNG.run(TestNG.java:1079)
	at org.gradle.api.internal.tasks.testing.testng.TestNGTestClassProcessor.runTests(TestNGTestClassProcessor.java:153)
	at org.gradle.api.internal.tasks.testing.testng.TestNGTestClassProcessor.stop(TestNGTestClassProcessor.java:96)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62)
	at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at [email protected]/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at [email protected]/java.lang.reflect.Method.invoke(Method.java:566)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
	at com.sun.proxy.$Proxy5.stop(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:193)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)

ben-manes avatar Apr 21 '24 03:04 ben-manes

Hi @ben-manes !

I was debugging your test and discovered a couple of suspicious things.

First, I think there is a typo in the merge operation:

@Operation
public Integer merge(@Param(name = "key") int key, @Param(name = "value") int nextValue) {
    return map.merge(key, nextValue, (k, v) -> v + nextValue);
}

The merge lambda should take not a key and value, but instead old and new values:

@Operation
public Integer merge(@Param(name = "key") int key, @Param(name = "value") int nextValue) {
    return map.merge(key, nextValue, (oldValue, newValue) -> oldValue + newValue);
}

Second, I might be mistaken, but I don't think that containsValue operation is linearizable. It has to iterate through the whole hash table searching for a bucket with the given value --- and thus this "iterative" operation is not "atomic".
Therefore, if the containsValue operation is present in a scenario, the Lincheck correctly discovers some interleaving with a non-linearizable outcome.

I've tried to fix these two problems locally (by fixing merge and removing @Operation annotation from containsValue method), and then the test passes.

Please let me know if this information helps.

eupp avatar Apr 22 '24 17:04 eupp

Oh yeah, thanks for catching the merge usage mistake! just dumb copy-paste from compute, I bet.

I was wondering that too about containsValue, but then I was surprised it passed in prior releases? I had tried the same over the weekend it fixed it for CHM but not with Caffeine, so I was still a bit perplexed. I was kind of hoping it was a bug in the tooling than in my code 😏

What do you think would cause this error, I don't think it is actionable for me to fix?

The execution has hung, see the thread dump
Gradle suite > Gradle test > com.github.benmanes.caffeine.lincheck.CaffeineLincheckTest$BoundedLincheckTest > modelCheckingTest FAILED
    org.jetbrains.kotlinx.lincheck.LincheckAssertionError:
    = The execution has hung, see the thread dump =
    | ------------------------------------------------------------- |
    |           Thread 1            |           Thread 2            |
    | ------------------------------------------------------------- |
    | put_asMap(4, 5)               |                               |
    | replaceConditionally(4, 5, 5) |                               |
    | get(4)                        |                               |
    | replaceConditionally(3, 5, 6) |                               |
    | invalidate(3)                 |                               |
    | ------------------------------------------------------------- |
    | compute(4, 4)                 | removeConditionally(3, 7)     |
    | get_function(4, 6)            | containsKey(4)                |
    | get_asMap(3)                  | replaceConditionally(2, 4, 3) |
    | get_function(2, 6)            | put_asMap(4, 4)               |
    | computeIfAbsent(5, 8)         | get_function(1, 2)            |
    | ------------------------------------------------------------- |
    | containsKey(4)                |                               |
    | compute(5, 3)                 |                               |
    | getIfPresent(1)               |                               |
    | get(5)                        |                               |
    | get_function(2, 6)            |                               |
    | ------------------------------------------------------------- |
        at app//org.jetbrains.kotlinx.lincheck.LinChecker.check(LinChecker.kt:45)
        at app//com.github.benmanes.caffeine.lincheck.AbstractLincheckCacheTest.modelCheckingTest(Unknown Source)
        at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
        at [email protected]/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at [email protected]/java.lang.reflect.Method.invoke(Method.java:566)
        at app//org.testng.internal.invokers.MethodInvocationHelper.invokeMethod(MethodInvocationHelper.java:141)
        at app//org.testng.internal.invokers.TestInvoker.invokeMethod(TestInvoker.java:686)
        at app//org.testng.internal.invokers.TestInvoker.invokeTestMethod(TestInvoker.java:230)
        at app//org.testng.internal.invokers.MethodRunner.runInSequence(MethodRunner.java:63)
        at app//org.testng.internal.invokers.TestInvoker$MethodInvocationAgent.invoke(TestInvoker.java:992)
        at app//org.testng.internal.invokers.TestInvoker.invokeTestMethods(TestInvoker.java:203)
        at app//org.testng.internal.invokers.TestMethodWorker.invokeTestMethods(TestMethodWorker.java:154)
        at app//org.testng.internal.invokers.TestMethodWorker.run(TestMethodWorker.java:134)
        at [email protected]/java.util.ArrayList.forEach(ArrayList.java:1541)
        at app//org.testng.TestRunner.privateRun(Unknown Source)
        at app//org.testng.TestRunner.run(Unknown Source)
        at app//org.testng.SuiteRunner.runTest(Unknown Source)
        at app//org.testng.SuiteRunner.runSequentially(Unknown Source)
        at app//org.testng.SuiteRunner.privateRun(Unknown Source)
        at app//org.testng.SuiteRunner.run(Unknown Source)
        at app//org.testng.SuiteRunnerWorker.runSuite(Unknown Source)
        at app//org.testng.SuiteRunnerWorker.run(Unknown Source)
        at app//org.testng.TestNG.runSuitesSequentially(Unknown Source)
        at app//org.testng.TestNG.runSuitesLocally(Unknown Source)
        at app//org.testng.TestNG.runSuites(Unknown Source)
        at app//org.testng.TestNG.run(Unknown Source)
        at org.gradle.api.internal.tasks.testing.testng.TestNGTestClassProcessor.runTests(TestNGTestClassProcessor.java:153)
        at org.gradle.api.internal.tasks.testing.testng.TestNGTestClassProcessor.stop(TestNGTestClassProcessor.java:96)
        at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62)
        at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at [email protected]/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
        at [email protected]/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at [email protected]/java.lang.reflect.Method.invoke(Method.java:566)
        at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
        at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
        at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
        at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
        at com.sun.proxy.$Proxy5.stop(Unknown Source)
        at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:193)
        at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
        at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
        at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
        at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
        at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
        at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
        at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
        at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)

ben-manes avatar Apr 22 '24 18:04 ben-manes

I was wondering that too about containsValue, but then I was surprised it passed in prior releases?

The number of invocations is relatively small (1_000). So yes, I guess it could have passed before just by pure (un)luck.

What do you think would cause this error, I don't think it is actionable for me to fix?

This one looks like an internal Lincheck error. I'll take a look.

eupp avatar Apr 23 '24 08:04 eupp

I realized that if I increase hangingDetectionThreshold, e.g. 5 * DEFAULT_HANGING_DETECTION_THRESHOLD, then the model checker passes. The default didn't change between releases, but perhaps other differences means that the current default is too low? Do you think that is the correct solution here?

The number of invocations is relatively small (1_000)

What would you recommend as a good configuration? In the past when I've tried adjusting the iterations and invocationsPerIteration then I'd receive an OutOfMemoryError on the 3gb heap. I'll experiment to see how far these values can be increased on the latest version (3.32). (Edit: Works wonderfully at larger values)

ben-manes avatar May 18 '24 18:05 ben-manes

I realized that if I increase hangingDetectionThreshold, e.g. 5 * DEFAULT_HANGING_DETECTION_THRESHOLD, then the model checker passes. The default didn't change between releases, but perhaps other differences means that the current default is too low? Do you think that is the correct solution here?

The problem might be because the Lincheck detects a false positive live-lock. The hangingDetectionThreshold parameter is used to tune the live-lock detector, so when increased it might help to avoid the false positive live-lock.

Could also be related to #307, CC @avpotapov00

What would you recommend as a good configuration? In the past when I've tried adjusting the iterations and invocationsPerIteration then I'd receive an OutOfMemoryError on the 3gb heap. I'll experiment to see how far these values can be increased on the latest version (3.32). (Edit: Works wonderfully at larger values)

Unfortunately, there is no ideal solution here. We are working on two big features that can eventually help with this problem --- the new model checking algorithm should reduce the memory footprint, and the parameters auto-tuning should pick reasonable number of iterations and invocations automatically. We don't have an ETA of these features though.

eupp avatar May 20 '24 09:05 eupp

Thanks. I’ll close this as no longer blocking.

ben-manes avatar May 20 '24 13:05 ben-manes