Как тестировать структуры данных

Процесс тестирования

При тестировании структуры данных Lincheck генерирует список сценариев выполнения, запускает их и анализирует результаты.

Рассмотрим эту структуру данных Counter:

Чтобы протестировать её, Lincheck выполняет следующие шаги:

1. Генерирует список случайных сценариев выполнения, случайным образом распределяя объявленные операции по разным потокам:

   

   Количество потоков и операций в каждом потоке можно задать с помощью параметров конфигурации, предоставляемых Lincheck.

2. Выполняет сгенерированные сценарии с использованием выбранной стратегии тестирования: проверки модели или стресс-тестирования. Каждый сгенерированный сценарий выполняется несколько раз, чтобы исследовать различные расписания выполнения:

   

3. Проверяет результаты выполнения на соответствие свойству корректности. По умолчанию это линеаризуемость.

   

   На этом шаге Lincheck также может проверить структуру, если ему передана функция проверки.

Пример: тестирование реализации стека Трайбера

Рассмотрим эту некорректную реализацию стека Трайбера:

class TreiberStack<E> {
    private val top = AtomicReference<Node<E>?>(null)

    fun push(item: E) {
        val newHead = Node(item)
        var oldHead: Node<E>?

        do {
            oldHead = top.get()
            newHead.next = oldHead
        } while (!top.compareAndSet(oldHead, newHead))
    }

    fun pop(): E? {
        val oldHead = top.get()

        if (oldHead == null) {
            return null
        }

        val newHead = oldHead.next
        top.compareAndSet(oldHead, newHead)

        // Bug: by the time `pop()` finishes execution,
        // another thread might have already popped this item.
        return oldHead.item
    }

    private class Node<E>(
        val item: E,
        var next: Node<E>? = null
    )
}

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

1. Создайте тестовую структуру:

   class TreiberStackTest {
       private val stack = TreiberStack<Int>()
   
       @Operation
       fun push(value: Int) = stack.push(value)
   
       @Operation
       fun pop(): Int? = stack.pop()
   
       @Test
       fun modelCheckingTest() = ModelCheckingOptions()
           .check(this::class)
   }
   

2. Запустите тест. Lincheck сформирует отчет об ошибке и укажет сценарий выполнения, который приводит к некорректному поведению:

   | ------------------------------ |
   |   Thread 1    |    Thread 2    |
   | ------------------------------ |
   | push(1): void |                |
   | ------------------------------ |
   | pop(): 1      | push(-1): void |
   | ------------------------------ |
   | pop(): -1     |                |
   | pop(): 1      |                |
   | ------------------------------ |
   

   На этой диаграмме показано, как операции распределены по разным потокам, а также значения, возвращаемые операциями. Lincheck также показывает конкретное чередование потоков, приводящее к некорректным результатам:

   | ----------------------------------------------------- |
   |                  Thread 1                  | Thread 2 |
   | ----------------------------------------------------- |
   | push(1)                                    |          |
   | ----------------------------------------------------- |
   | pop(): 1                                   |          |
   |   stack.pop(): 1                           |          |
   |     top.get(): Node#1                      |          |
   |     switch                                 |          |
   |                                            | push(-1) |
   |     oldHead.getNext(): null                |          |
   |     top.compareAndSet(Node#1, null): false |          |
   |     oldHead.getItem(): 1                   |          |
   |   result: 1                                |          |
   | ----------------------------------------------------- |
   | pop(): -1                                  |          |
   | pop(): 1                                   |          |
   | ----------------------------------------------------- |
   

   Поскольку реализация не учитывает возможность прерывания функции pop() другим потоком, pop() возвращает 1 дважды, чего происходить не должно.

3. Исправьте структуру данных. Корректная реализация обновляет переменную oldHead до последнего значения перед возвратом результатов:

       fun pop(): E? {
           var oldHead: Node<E>?
           var newHead: Node<E>?
   
           do {
               oldHead = top.get()
               if (oldHead == null) return null
               newHead = oldHead.next
           } while (!top.compareAndSet(oldHead, newHead))
   
           return oldHead.item
        }
   

Что дальше

Узнайте о стратегиях тестирования, доступных в Lincheck.

См. также

• Генерация аргументов операций

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

• Проверка гарантий неблокирующего прогресса

• Определение последовательной спецификации алгоритма