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

Сравнение сериализуемости и линейризуемости

Чтобы понять разницу между этими двумя моделями, рассмотрим, как структура данных может быть сериализуемой, но не линейризуемой:

1. Рассмотрим следующую структуру данных:

   class ConcurrentQueue {
       private val elements: MutableList<Int> = ArrayList()
   
       fun put(x: Int) = synchronized(this) {
           elements += x
       }
   
       fun poll(): Int? = synchronized(this) {
           if (elements.isEmpty()) return null
           elements.shuffle()
           elements.removeAt(0)
       }
   }
   

   Эта конкурентная структура работает некорректно: она сохраняет элементы, как обычная очередь, но возвращает их в случайном порядке.

2. Реализуйте последовательную версию очереди, которая правильно сохраняет и возвращает элементы:

   class CorrectSequentialQueue {
       private val elements: MutableList<Int> = ArrayList()
   
       fun put(x: Int) {
           elements += x
       }
   
       fun poll(): Int? = if (elements.isEmpty()) null else elements.removeAt(0)
   }
   

3. Создайте класс теста и объявите операции put() и poll():

   @Param(name = "value", gen = IntGen::class, conf = "1:2")
   class ConcurrentQueueTest {
       private val q = ConcurrentQueue()
   
       @Operation
       fun put(@Param(name = "value") x: Int) = q.put(x)
   
       @Operation
       fun poll(): Int? = q.poll()
   }

4. Объявите и запустите тест на сериализуемость:

       @Test
       fun serializabilityTest() = ModelCheckingOptions()
           .actorsBefore(0)
           .actorsAfter(0)
           .actorsPerThread(2)
           .threads(2)
           // Use the `SerializabilityVerifier`
           .verifier(SerializabilityVerifier::class.java)
           // Specify the sequential version of the structure
           .sequentialSpecification(CorrectSequentialQueue::class.java)
           .check(this::class.java)
   

   Он должен успешно пройти.

5. Объявите и запустите тест на линейризуемость:

       @Test
       fun linearizabilityTest() = ModelCheckingOptions()
           .actorsBefore(0)
           .actorsAfter(0)
           .actorsPerThread(2)
           .threads(2)
           // Show the full failed scenario
           .minimizeFailedScenario(false)
           // Specify the sequential version of the structure
           .sequentialSpecification(CorrectSequentialQueue::class.java)
           .check(this::class.java)
   

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

   | -------------------- |
   | Thread 1  | Thread 2 |
   | -------------------- |
   |           | put(2)   |
   |           | put(1)   |
   | put(3)    |          |
   | poll(): 1 |          |
   | -------------------- |
   

6. Проанализируйте результаты.

   Поскольку тест на сериализуемость проходит, существует некоторый последовательный порядок операций SequentialQueue, приводящий к poll(): 1, например:

   Однако линейризуемость накладывает дополнительные ограничения на порядок операций: если операция A завершается до начала операции B в конкурентном выполнении, то A должна выполняться до B в последовательном выполнении. Пример линейризуемого выполнения выглядит так:

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