override fun nextContext()

in src/jvm/main/org/jetbrains/lincheck/datastructures/verifier/LinearizabilityVerifier.kt [44:67]

• 16 lines of code
• 9 McCabe index (conditional complexity)

    override fun nextContext(threadId: Int): LinearizabilityContext? {
        if (isCompleted(threadId)) return null
        // Check whether an actorWithToken from the specified thread can be executed
        // in accordance with the rule that all actors from init part should be
        // executed at first, after that all actors from parallel part, and
        // all actors from post part should be executed at last.
        if (!hblegal(threadId))
            return null
        val actorId = executed[threadId]
        val actor = scenario.threads[threadId][actorId]
        // null result is not impossible here as if the execution has hung, we won't check its result
        val expectedResult = results.threadsResults[threadId][actorId]!!
        // Check whether the operation has been suspended and should be followed by cancellation
        val ticket = tickets[threadId]
        val promptCancel = actor.promptCancellation && ticket != NO_TICKET && expectedResult === Cancelled
        if (suspended[threadId] || promptCancel) {
            return if (actor.cancelOnSuspension && expectedResult === Cancelled)
                state.nextByCancellation(actor, ticket).createContext(threadId)
            else null
        }
        // Try to make a transition by the next actor from the current thread,
        // passing the ticket corresponding to the current thread.
        return state.next(actor, expectedResult, tickets[threadId])?.createContext(threadId)
    }