时序规范

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.

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.*

8. class ConcurrentLinkedQueueTest {
9. private val s = ConcurrentLinkedQueue<Int>()

11. @Operation
12. fun add(value: Int) = s.add(value)

14. @Operation
15. fun poll(): Int? = s.poll()

17. @Test
18. fun stressTest() = StressOptions()
19. .sequentialSpecification(SequentialQueue::class.java)
20. .check(this::class)
21. }

23. class SequentialQueue {
24. private val s = LinkedList<Int>()

26. fun add(x: Int) = s.add(x)
27. fun poll(): Int? = s.poll()
28. }

Get the full code of the examples.