Гарантии выполнения

Многие конкуретнтые алгоритмы обеспечивают гарантии выполнения без блокировок, такие как отсутствие блокировок и отсутствие ожидания. Поскольку они обычно нетривиальны, легко добавить ошибку, которая блокирует алгоритм. Lincheck может помочь найти ошибки живучести с помощью стратегии проверки модели.

Чтобы проверить гарантию выполнения алгоритма, включите опцию checkObstructionFreedom в ModelCheckingOptions().

ModelCheckingOptions().checkObstructionFreedom()

Например, рассмотрите ConcurrentHashMap<K, V> из стандартной библиотеки Java. Вот тест Lincheck для обнаружения того, что put(key: K, value: V) является блокирующей операцией:

class ConcurrentHashMapTest {
    private val map = ConcurrentHashMap<Int, Int>()

    @Operation
    public fun put(key: Int, value: Int) = map.put(key, value)

    @Test
    fun modelCheckingTest() = ModelCheckingOptions()
        .actorsBefore(1) // To init the HashMap
        .actorsPerThread(1)
        .actorsAfter(0)
        .minimizeFailedScenario(false)
        .checkObstructionFreedom()
        .check(this::class)
}

Запустите modelCheckingTest(). Вы должны получить следующий результат:

= Obstruction-freedom is required but a lock has been found =
Execution scenario (init part):
[put(2, 6)]
Execution scenario (parallel part):
| put(-6, -8) | put(1, 4) |

= The following interleaving leads to the error =
Parallel part trace:
|                                                                                          | put(1, 4)                                                                                |
|                                                                                          |   put(1,4) at ConcurrentHashMapTest.put(ConcurrentMapTest.kt:34)                         |
|                                                                                          |     putVal(1,4,false) at ConcurrentHashMap.put(ConcurrentHashMap.java:1006)              |
|                                                                                          |       table.READ: Node[]@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1014)      |
|                                                                                          |       tabAt(Node[]@1,0): Node@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1018) |
|                                                                                          |       MONITORENTER at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1031)              |
|                                                                                          |       tabAt(Node[]@1,0): Node@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1032) |
|                                                                                          |       next.READ: null at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1046)           |
|                                                                                          |       switch                                                                             |
| put(-6, -8)                                                                              |                                                                                          |
|   put(-6,-8) at ConcurrentHashMapTest.put(ConcurrentMapTest.kt:34)                       |                                                                                          |
|     putVal(-6,-8,false) at ConcurrentHashMap.put(ConcurrentHashMap.java:1006)            |                                                                                          |
|       table.READ: Node[]@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1014)      |                                                                                          |
|       tabAt(Node[]@1,0): Node@1 at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1018) |                                                                                          |
|       MONITORENTER at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1031)              |                                                                                          |
|                                                                                          |       MONITOREXIT at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1065)               |

Теперь давайте напишем тест для неблокирующей ConcurrentSkipListMap<K, V>, ожидая, что тест пройдет успешно:

class ConcurrentSkipListMapTest {
    private val map = ConcurrentSkipListMap<Int, Int>()

    @Operation
    public fun put(key: Int, value: Int) = map.put(key, value)

    @Test
    fun modelCheckingTest() = ModelCheckingOptions()
        .checkObstructionFreedom()
        .check(this::class)
}

В настоящее время Lincheck поддерживает только гарантии выполнения без препятствий. Однако большинство реальных ошибок живучести добавляют неожиданный блокирующий код, поэтому проверка на свободу от препятствий также поможет с алгоритмами без блокировок и без ожидания.