Гарантии прогресса

Пример: проверка ConcurrentHashMap на obstruction-freedom

В этом примере вы проверите функцию put() структуры ConcurrentHashMap.

1. Создайте файл ConcurrentHashMapTest.kt.

2. Создайте тестовый класс для ConcurrentHashMap, объявите функцию put() и тестовую функцию с включенным параметром checkObstructionFreedom():

   class ConcurrentHashMapTest {
       private val map = ConcurrentHashMap<Int, Int>()
   
       @Operation
       fun put(key: Int, value: Int) = map.put(key, value)
   
       @Test
       fun modelCheckingTest() = ModelCheckingOptions()
           .checkObstructionFreedom()
           .threads(2)
           .actorsPerThread(1)
           .check(this::class)
   }
   

   Параметры threads и actorsPerThread используются для сокращения числа возможных сценариев выполнения. Эти параметры не влияют на результат теста, но значительно сокращают время тестирования.

3. Запустите тест. Он должен завершиться с ошибкой и вывести следующий отчет:

   = The algorithm should be non-blocking, but an active lock is detected =
   | --------------------- |
   | Thread 1  | Thread 2  |
   | --------------------- |
   | put(1, 0) | put(1, 1) |
   | --------------------- |
   
   The following interleaving leads to the error:
   | -------------------------------------------------------------------------------------------------------------- |
   |                                          Thread 1                                          |     Thread 2      |
   | -------------------------------------------------------------------------------------------------------------- |
   | put(1, 0): <hung>                                                                          |                   |
   |   map.put(1, 0)                                                                            |                   |
   |     putVal(1, 0, false)                                                                    |                   |
   |       spread(1): 1                                                                         |                   |
   |       table ➜ null                                                                         |                   |
   |       loop(1 iterations) at ConcurrentHashMap.putVal(ConcurrentHashMap.java:1016)          |                   |
   |         <iteration 1>                                                                      |                   |
   |           initTable()                                                                      |                   |
   |             loop(1 iterations) at ConcurrentHashMap.initTable(ConcurrentHashMap.java:2293) |                   |
   |             table ➜ null                                                                   |                   |
   |             switch                                                                         |                   |
   |                                                                                            | put(1, 1): <hung> |
   | -------------------------------------------------------------------------------------------------------------- |
   

4. Добавьте параметр blocking = true в аннотацию функции put():

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

5. Запустите тест повторно. Он должен завершиться успешно.

Пример: проверка ConcurrentSkipListMap на obstruction-freedom

В этом примере вы проверите функцию put() неблокирующей структуры ConcurrentSkipListMap.

1. Создайте файл ConcurrentSkipListMapTest.kt.

2. Создайте тестовый класс для ConcurrentSkipListMap, объявите функцию put() и тестовую функцию с включенным параметром checkObstructionFreedom():

   class ConcurrentSkipListMapTest {
       private val map = ConcurrentSkipListMap<Int, Int>()
   
       @Operation
       fun put(key: Int, value: Int) = map.put(key, value)
   
       @Test
       fun modelCheckingTest() = ModelCheckingOptions()
           .checkObstructionFreedom()
           .check(this::class)
   }
   

3. Запустите тест. Он должен завершиться успешно.

См. также

• Настройка ограничений генерации аргументов

• Настройка выполнения операций

• Проверка и валидация результатов выполнения