时序规范

To be sure that the algorithm provides correct sequential behavior, you can define its sequential specification by writing a straightforward sequential implementation of the testing data structure.

This feature also allows you to write a single test instead of two separate sequential and concurrent tests.

时序规范 - 图1

To provide a sequential specification of the algorithm for verification:

  1. Implement a sequential version of all the testing methods.
  2. Pass the class with sequential implementation to the sequentialSpecification() option:

    1. StressOptions().sequentialSpecification(SequentialQueue::class)

For example, here is the test to check correctness of j.u.c.ConcurrentLinkedQueue from the Java standard library.

  1. import org.jetbrains.kotlinx.lincheck.*
  2. import org.jetbrains.kotlinx.lincheck.annotations.*
  3. import org.jetbrains.kotlinx.lincheck.strategy.stress.*
  4. import org.junit.*
  5. import java.util.*
  6. import java.util.concurrent.*
  7. class ConcurrentLinkedQueueTest {
  8. private val s = ConcurrentLinkedQueue<Int>()
  9. @Operation
  10. fun add(value: Int) = s.add(value)
  11. @Operation
  12. fun poll(): Int? = s.poll()
  13. @Test
  14. fun stressTest() = StressOptions()
  15. .sequentialSpecification(SequentialQueue::class.java)
  16. .check(this::class)
  17. }
  18. class SequentialQueue {
  19. private val s = LinkedList<Int>()
  20. fun add(x: Int) = s.add(x)
  21. fun poll(): Int? = s.poll()
  22. }

Get the full code of the examples.

时序规范 - 图2