[1]
       
            * Product Blogs
       
            * 
       
            *   
       
                * 
       
                  IDEs
       
                    * [2][IMAGE]AppCode
       
                    * [3][IMAGE]CLion
       
                    * [4][IMAGE]DataGrip
       
                    * [5][IMAGE]GoLand
       
                    * [6][IMAGE]IntelliJ IDEA
       
                    * [7][IMAGE]MPS
       
                    * [8][IMAGE]PhpStorm
       
                    * [9][IMAGE]PyCharm
       
                    * [10][IMAGE]Rider
       
                    * [11][IMAGE]RubyMine
       
                    * [12][IMAGE]WebStorm
       
                    * [13][IMAGE]Toolbox App
       
            *   
       
                * 
       
                  Team Tools
       
                    * [14][IMAGE]Space
       
                    * [15][IMAGE]TeamCity
       
                    * [16][IMAGE]Upsource
       
                    * [17][IMAGE]YouTrack
       
                    * [18][IMAGE]Datalore
       
                    * [19][IMAGE]Hub
       
            *   
       
                * 
       
                  .NET & Visual Studio
       
                    * [20][IMAGE].NET Tools
       
                    * [21][IMAGE]ReSharper C++
       
                * 
       
                  Languages
       
                    * [22][IMAGE]Kotlin
       
                    * [23][IMAGE]Ktor
       
            *   
       
                * 
       
                  Education
       
                    * [24]Edu Products
       
                * 
       
                  Company
       
                    * [25][IMAGE]News
       
                    * [26][IMAGE]Team
       
                    * [27][IMAGE]JetBrains Platform
       
          [22] Kotlin logo
       
          The Kotlin Blog
          ---------------
       
          Kotlin Programming Language by JetBrains
       
            * [28]Releases
       
            * [29]Server
       
            * [30]JavaScript
       
            * [31]Mobile
       
            * [32]Community
       
            * [33]iOS
       
          [34]Visit the Kotlin Site Kotlin logo How We Test Concurrent
          Primitives in Kotlin Coroutines[35]
       
          How We Test Concurrent Primitives in Kotlin Coroutines
          ======================================================
       
          [36]Nikita Koval
       
          Today we would like to share how we test concurrency primitives in
          Kotlin Coroutines.
       
          Many of our users are delighted with the experience of using
          coroutines to write asynchronous code. This does not come as a
          surprise, since with coroutines we are able to write straightforward
          and readable code, with almost all the asynchronicity happening under
          the hood. For simplicity, we can think of coroutines in Kotlin as
          super-lightweight threads with some additional power, such as
          cancellability and structured concurrency. However, coroutines also
          make the code much safer. Traditional concurrent programming involves
          manipulating a shared mutable state, which is arguably error-prone. As
          an alternative, coroutines provide special communicating primitives,
          such as Channel, to perform the synchronization. Using channels and a
          couple of other primitives as building blocks, we can construct
          extremely powerful things, such as the recently introduced [37]Flows.
          However, nothing is free. While the message passing approach is
          typically safer, the required primitives are not trivial to implement
          and, therefore, have to be tested as thoroughly as possible.
          Simultaneously, testing concurrent code may be as complicated as
          writing it.
       
          That is why we have Lincheck – a special framework for testing
          concurrent data structures on the JVM. This framework’s main advantage
          is that it provides a simple and declarative way to write concurrent
          tests. Instead of describing how to perform the test, you specify what
          to test by declaring all the operations to examine along with the
          required correctness property (linearizability is the default one, but
          various extensions are supported as well) and restrictions (e.g.
          “single-consumer” for queues).
       
          Lincheck Overview
          -----------------
       
          Let’s consider a simple concurrent data structure, such as the stack
          algorithm presented below. In addition to the standard push(value) and
          pop() operations, we also implement a non-linearizable (thus,
          incorrect) size(), which increases and decreases the corresponding
          field following successful push and pop invocations.
       
          class Stack<T> {
              private val top  = atomic<Node<T>?>(null)
              private val _size = atomic(0)
          
             fun push(value: T): Unit = top.loop { cur ->
                  val newTop = Node(cur, value)
                  if (top.compareAndSet(cur, newTop)) { // try to add
                      _size.incrementAndGet() // <-- INCREMENT SIZE
                      return
                  }
              }
          
             fun pop(): T? = top.loop { cur ->
                  if (cur == null) return null // is stack empty?
                  if (top.compareAndSet(cur, cur.next)) { // try to retrieve
                      _size.decrementAndGet() // <-- DECREMENT SIZE
                      return cur.value
                  }
              }
          
             val size: Int get() = _size.value
          }
          class Node<T>(val next: Node<T>?, val value: T)   
       
          To write a concurrent test for this stack without any tool, you have
          to manually run parallel threads, invoke the stack operations, and
          finally check that some sequential history can explain the obtained
          results. We have used such manual tests in the past, and all of them
          contained at least a hundred lines of boilerplate code. But with
          Lincheck, this machinery is automated, and tests become short and
          informative.
       
          To write a concurrent test with Lincheck, you need to list the data
          structure operations and mark them with a special @Operation
          annotation. The initial state is specified in the constructor (here,
          we create a new TriebeStack<Int> instance). After that, we need to
          configure the testing modes, which can be done using special
          annotations on the test class – @StressCTest for stress testing and
          @ModelCheckingCTest for model checking mode. Finally, we can run the
          analysis by invoking the Linchecker.check(..) function on the testing
          class.
       
          Let’s write a test for our incorrect stack:
       
          @StressCTest
          @ModelCheckingCTest
          class StackTest {
              private val s = TrieberStack<Int>()
          
             @Operation fun push(value: Int) = s.push(value)
              @Operation fun pop() = s.pop()
              @Operation fun size() = s.size
          
             @Test fun runTest() = LinChecker.check(this::class)
          }   
       
          There are just 12 lines of easy-to-follow code that describe the
          testing data structure, and that is all you need to do with Lincheck!
          It automatically:
       
            1. Generates several random concurrent scenarios.
       
            2. Examines each of them using either the stress or the model
              checking strategy, performing the number of scenario invocations
              specified by the user.
       
            3. Verifies that each of the invocation results satisfies the
              required correctness property (e.g. linearizability).For this
              step, we use a sequential specification, which is defined with the
              testing data structure by default; though, a custom sequential
              specification can be set.
       
          If an invocation hangs, fails with an exception, or the result is
          incorrect, the test fails with an error similar to the one below. Here
          we smoothly come to the main advantage of the model checking mode.
          While Lincheck always provides a failure scenario with the incorrect
          results (if any are found), the model checking mode also provides a
          trace to reproduce the error. In the example below, the failing
          execution starts with the first thread, pushes 7 into the stack, and
          stops before incrementing the size. The execution switches to the
          second thread, which retrieves the already pushed 2 from the stack and
          decreases the size to -1. The following size() invocation returns -1,
          which is incorrect since it is negative. While the error seems obvious
          even without a trace, having the trace helps considerably when you are
          working on real-world concurrent algorithms, such as synchronization
          primitives in Kotlin Coroutines.
       
          = Invalid execution results =
          | push(7): void | pop():  7  |
          |               | size(): -1 |
          
          = The following interleaving leads to the error =
          | push(7)                                |                      |
          |   top.READ: null                       |                      |
          |       at Stack.push(Stack.kt:5)        |                      |
          |   top.compareAndSet(null,Node@1): true |                      |
          |       at Stack.push(Stack.kt:7)        |                      |
          |   switch                               |                      |
          |                                        | pop(): 7             |
          |                                        | size(): -1           |
          |                                        |   thread is finished |
          |   _size.incrementAndGet(): 0           |                      |
          |       at Stack.push(Stack.kt:8)        |                      |
          |   result: void                         |                      |
          |   thread is finished                   |                      |
          
       
          Scenario Generation
          In Lincheck, we provide the numbers of parallel threads and operations
          within them that can be configured in @<Mode>CTest annotations.
          Lincheck generates the specified number of scenarios by filling the
          threads with randomly chosen operations. Note that the push(..)
          operation on the stack above takes an integer parameter value, which
          specifies the element to be inserted. Simultaneously, the error
          message provides a specific scenario with an input value to the
          push(..) invocation. This parameter is also randomly generated in a
          specified range, which can also be configured. It is also possible to
          add restrictions like "single-consumer" so that the corresponding
          operations cannot be invoked concurrently.
       
          Testing Modes
          Lincheck runs the generated scenario in either stress testing or model
          checking mode. In stress testing mode, the scenario is executed on
          parallel threads many times to detect interleavings that yield
          incorrect results. In model checking mode, Lincheck examines many
          different interleavings with a bounded number of context switches.
          Compared to stress testing, model checking increases test coverage as
          well as the failing execution trace of the found incorrect behavior.
          However, it assumes the sequential consistency memory model, which
          means it ignores weak memory model effects. In particular, it cannot
          find a bug caused by a missed @Volatile. Therefore, in practice we use
          both stress testing and model checking mode.
       
          Minimizing Failing Scenarios
          When writing a test, it makes sense to configure it so that several
          threads are executed, each with several operations. However, most bugs
          can be reproduced with fewer threads and operations. Thus, Lincheck
          “minimizes” the failing scenario by trying to remove an operation from
          it and checking whether the test still fails. It continues to remove
          operations until it is no longer possible to do so without also
          causing the test not to fail. While this greedy approach is not
          theoretically optimal, we find it works well enough in practice.
       
          Model Checking Details
          ----------------------
       
          Let’s dig deeper into model checking,one of Lincheck’s most impressive
          features, and see how everything works under the hood. If you want to
          try Lincheck before going further, just add the [38]org.jetbrains.kotlinx:lincheck:2.12
          dependency to your Gradle or Maven project!
       
          Before we started working on model checking, we already had Lincheck
          with stress testing mode. While it provided a nice way to write tests
          and significantly improved their quality, we were still spending
          countless hours trying to understand how to reproduce a discovered
          bug. Spending all this time motivated us to find a way to automate the
          process. That is how we came to adopt the bounded model checking
          approach to our practical Lincheck. The idea was simple — once we
          implemented model checking, Lincheck would be able to provide an
          interleaving that re-produced the found bug automatically, meaning we
          would no longer need to spend hours trying to understand it. One of
          the main challenges was finding a way to make everything work without
          having to change the code.
       
          In our experience, most bugs in complicated concurrent algorithms can
          be reproduced using the sequential consistency memory model.
          Simultaneously, the model-checking approaches for weak memory models
          are very complicated, so we decided to use a bounded model checking
          under the sequential consistency memory model. This was originally
          inspired by the one used in the CHESS framework for C#, which studies
          all possible schedules with a bounded number of context switches by
          fully controlling the execution and putting context switches in
          different locations in threads. In contrast to CHESS, Lincheck bounds
          the number of schedules to be studied instead of the number of context
          switches. This way, the test time is predictable independently of
          scenario size and algorithm complexity.
       
          In short, Lincheck starts by studying all interleavings with one
          context switch but does this evenly, trying to explore a variety of
          interleavings simultaneously. This way, we increase the total coverage
          if the number of available invocations is not sufficient to cover all
          the interleavings. Once all the interleavings with one context switch
          have been reviewed, Lincheck starts examining interleavings with two
          context switches, and repeats the process, increasing the number of
          context switches each time, until the available invocations exceed the
          maximum or all possible interleavings are covered. This strategy
          increases the testing coverage and allows you to find an incorrect
          schedule with the lowest number of context switches possible, marking
          a significant improvement for bug investigation.
       
          Switch Points
          Lincheck inserts switch points into the testing code to control the
          execution. These points identify where a context switch can be
          performed. The interesting switch point locations are shared memory
          accesses, such as field and array element reads or updates in the JVM.
          These reads or updates can be performed by either the corresponding
          byte-code instructions or special methods, like the ones in
          AtomicFieldUpdater or Unsafe classes. To insert a switch point, we
          transform the testing code via the ASM framework and add our internal
          function invocations before each access. The transformation is
          performed on the fly using a custom class loader, which means that
          technically we’ve created a transformed copy of the testing code.
       
          Interleaving Tree
          To explore different possible schedules, Lincheck constructs an
          interleaving tree, the edges of which represent choices that can be
          performed by the scheduler. The figure below presents a partially
          built interleaving tree with one context switch for the scenario from
          the overview. First, Lincheck decides where the execution should be
          started. From there, several switch points are available to be
          examined. In the figure, only the first switch point related to
          top.READ is fully explored.
       
          To explore interleavings evenly, Lincheck tracks the percentage of
          explored interleavings for each subtree, using weighted randomness to
          make its choices about where to go. The weights are proportional to
          the ratios of unobserved interleavings. In our example above, Lincheck
          is more likely to start the next interleaving from the second thread.
          Since the exact number of interleavings is unknown, all children have
          equal weights initially. After all the current tree’s interleavings
          have been explored, Lincheck increases the number of context switches,
          thus increasing the tree depth.
       
          Execution Trace
          The key advantage of model checking mode is that it provides an
          execution trace that reproduces the error. To increase its
          readability, Lincheck captures the arguments and the results of each
          of the shared variable accesses (such as reads, writes, and CAS-s) and
          the information about the fields. For example, in the trace in the
          listing from the overview, the first event is a reading of null from
          the top field, and the source code location is also provided. At the
          same time, if a function with multiple shared variable accesses is
          executed without a context switch in the middle, Lincheck shows this
          function invocation with the corresponding arguments and result
          instead of the events inside it. This also makes the trace easier to
          follow, as evidenced in the second thread in the trace.
       
          To Sum Up
          ---------
       
          We hope you enjoyed reading this post and found Lincheck interesting
          and useful. In Kotlin, we successfully use Lincheck both to test
          existing concurrent data structures in Kotlin Coroutines and to
          develop new algorithms more productively and enjoyably. As a final
          note, we would like to say that Lincheck tests should be treated like
          regular unit tests — they can check your data structure for the
          specified correctness contract, nothing more and nothing else. So,
          even if you have Lincheck tests, do not hesitate to add integration
          tests when your data structure is used in the real world.
       
          Want to try Lincheck? Just add the [38]org.jetbrains.kotlinx:lincheck:2.12
          dependency to your Gradle or Maven project and enjoy!
       
          [39]Lincheck on Github
          ======================
       
            * Share
       
            * [40]
       
            * [41]
       
            * [42]
       
          [43] Jetpack Compose for Desktop: Milestone 3 Released
       
          Discover more
          -------------
       
          [43]
       
          Jetpack Compose for Desktop: Milestone 3 Released
       
          The Compose for Desktop journey continues! Since the last milestone
          release of Compose for Desktop, we’ve done our best to bring you an
          even better experience when building desktop UIs in a modern and
          declarative style. Today we’re publishing Compose for Desktop
          Milestone 3, which introduces significant rendering and
          interoperability improvements, and makes it even easier to integrate
          and distribute Compose for Desktop applications.
       
          Sebastian Aigner[44]
       
          Leroy Merlin Case Study: Building Customer-Facing Flagship App with
          KMM
       
          Leroy Merlin helps people all around the world improve their living
          environment and lifestyle by helping them design the homes of their
          dreams and make them a reality. The Leroy Merlin mobile app helps
          customers search for products, shop online and find their nearest
          store. The Russian branch of Leroy Merlin has stores in 64 cities, and
          1.5 million people use the mobile app monthly. Visit the Ko
       
          Alex Anisimov[45]
       
          Multik: Multidimensional Arrays in Kotlin
       
          A lot of data-heavy tasks, as well as optimization problems, boil down
          to performing computations over multidimensional arrays. Today we’d
          like to share with you the first preview of a library that aims to
          serve as a foundation for such computations – Multik. Multik offers
          both multidimensional array data structures and implementations of
          mathematical operations over them. The library has a simpl
       
          Maria Khalusova[46]
       
          Server-side With Kotlin Webinar Series, Vol 2
       
          We continue our series of Kotlin for server-side webinars. Between
          February 18 and March 18 we will host 4 webinars to explore applied
          software development with Kotlin on server-side through live-coding
          sessions. Speakers from JetBrains, VMware, Confluent, and Oracle will
          cover reactive programming, asynchronous applications with the Ktor
          framework, building microservices with Helidon, and other a
       
          Alina Dolgikh
       
            * [47]JetBrains
       
            * [48]Contacts
       
            * [49]Careers
       
            * [50]
       
            * [51]
       
            * [52]
       
            * [53]
       
            * [54]
       
            * [55]
       
            * [56]
       
            * [57]Privacy & Security
       
            * [58]Terms of Use
       
            * [59]Legal
       
            * [60]Genuine tools
       
          Copyright © 2000–2021 JetBrains s.r.o.
       
          1. https://blog.jetbrains.com/
          2. https://blog.jetbrains.com/objc/
          3. https://blog.jetbrains.com/clion/
          4. https://blog.jetbrains.com/datagrip/
          5. https://blog.jetbrains.com/go/
          6. https://blog.jetbrains.com/idea/
          7. https://blog.jetbrains.com/mps/
          8. https://blog.jetbrains.com/phpstorm/
          9. https://blog.jetbrains.com/pycharm/
          10. https://blog.jetbrains.com/dotnet/tag/rider/
          11. https://blog.jetbrains.com/ruby/
          12. https://blog.jetbrains.com/webstorm/
          13. https://blog.jetbrains.com/blog/tag/jetbrains-toolbox/
          14. https://blog.jetbrains.com/space/
          15. https://blog.jetbrains.com/teamcity/
          16. https://blog.jetbrains.com/upsource/
          17. https://blog.jetbrains.com/youtrack/
          18. https://blog.jetbrains.com/datalore/
          19. https://blog.jetbrains.com/hub/
          20. https://blog.jetbrains.com/dotnet/
          21. https://blog.jetbrains.com/rscpp/
          22. https://blog.jetbrains.com/kotlin/
          23. https://blog.jetbrains.com/ktor/
          24. https://blog.jetbrains.com/education/
          25. https://blog.jetbrains.com/blog/
          26. https://blog.jetbrains.com/team/
          27. https://blog.jetbrains.com/platform/
          28. https://blog.jetbrains.com/kotlin/category/releases/
          29. https://blog.jetbrains.com/kotlin/category/server/
          30. https://blog.jetbrains.com/kotlin/category/javascript/
          31. https://blog.jetbrains.com/kotlin/category/mobile/
          32. https://blog.jetbrains.com/kotlin/category/community/
          33. https://blog.jetbrains.com/kotlin/category/ios/
          34. https://kotlinlang.org/
          35. https://twitter.com/kotlin
          36. https://blog.jetbrains.com/author/nikita-koval-jetbrains-com
          37. https://kotlin.github.io/kotlinx.coroutines/kotlinx-coroutines-core/kotlinx.coroutines.flow/-flow/
          38. https://bintray.com/kotlin/kotlinx/kotlinx.lincheck/2.12
          39. https://github.com/Kotlin/kotlinx-lincheck
          40. https://www.facebook.com/sharer.php?u=https%3A%2F%2Fblog.jetbrains.com%2Fkotlin%2F2021%2F02%2Fhow-we-test-concurrent-primitives-in-kotlin-coroutines%2F
          41. https://twitter.com/intent/tweet?source=https%3A%2F%2Fblog.jetbrains.com%2Fkotlin%2F2021%2F02%2Fhow-we-test-concurrent-primitives-in-kotlin-coroutines%2F&text=Here%20is%20a%20great%20read: https%3A%2F%2Fblog.jetbrains.com%2Fkotlin%2F2021%2F02%2Fhow-we-test-concurrent-primitives-in-kotlin-coroutines%2F&via=kotlin
          42. http://www.linkedin.com/shareArticle?mini=true&url=https%3A%2F%2Fblog.jetbrains.com%2Fkotlin%2F2021%2F02%2Fhow-we-test-concurrent-primitives-in-kotlin-coroutines%2F
          43. https://blog.jetbrains.com/kotlin/2021/02/jetpack-compose-for-desktop-milestone-3-released/
          44. https://blog.jetbrains.com/kotlin/2021/02/leroy-merlin-case-study-building-customer-facing-flagship-app-with-kmm/
          45. https://blog.jetbrains.com/kotlin/2021/02/multik-multidimensional-arrays-in-kotlin/
          46. https://blog.jetbrains.com/kotlin/2021/02/server-side-with-kotlin-webinar-series-vol-2/
          47. https://www.jetbrains.com/
          48. https://www.jetbrains.com/company/contacts/
          49. https://www.jetbrains.com/careers/apply/
          50. https://twitter.com/jetbrains
          51. https://www.facebook.com/JetBrains
          52. https://www.linkedin.com/company/jetbrains
          53. https://www.instagram.com/jetbrains/
          54. https://www.youtube.com/user/JetBrainsTV
          55. https://vk.com/jetbrains/
          56. https://blog.jetbrains.com/feed/
          57. https://www.jetbrains.com/company/privacy.html
          58. https://www.jetbrains.com/company/useterms.html
          59. https://www.jetbrains.com/legal/
          60. https://www.jetbrains.com/genuine-tools/