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)

@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)
}

= 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                   |                      |