Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Strategy run API refactoring #262

Merged
merged 11 commits into from
Jun 12, 2024
Merged

Strategy run API refactoring #262

merged 11 commits into from
Jun 12, 2024

Conversation

eupp
Copy link
Collaborator

@eupp eupp commented Jan 22, 2024

This PR proposes a simple refactoring of the Strategy class API.

Motivation

Currently, the Strategy API provides the following method to run the scenario:

abstract fun run(): LincheckFailure?

This method should run the scenario (some) number of times and returns the failure, in case if any invocation fails.

This API leads to code duplication in the current code base.

  • Both stress and model-checking strategies in fact run the scenario fixed number of times in a loop. This loop is duplicated in both implementations.
  • Both strategies run verifier on each invocation result. Again, the implementation of verification method is duplicated in both strategies.

This PR proposes to change the API, so that the Strategy instead provides the method to run single invocation:

abstract fun runInvocation(): InvocationResult

This change allows to implement the previously duplicated functionality in a single place, as a bunch of Strategy interface extension methods.

Note that in addition, the new API adds two (optional) methods to implement:

    /**
     * Sets the internal state of strategy to run the next invocation.
     *
     * @return true if there is next invocation to run, false if all invocations have been studied.
     */
    open fun nextInvocation(): Boolean = true

    /**
     * Initializes the invocation.
     * Should be called before each call to [runInvocation].
     */
    open fun initializeInvocation() {}

Thus, the pattern to run the strategy becomes as follows:

// run single invocation (if available)
with(strategy) {
     if (nextInvocation()) {
        initializeInvocation()
        runInvocation()
     }
}

For deterministic strategies (like model checking strategy), consecutive calls of runInvocation withouth nextInvocation calls, should lead to the same results:

with(strategy) {
     if (nextInvocation()) {
        // first invocation run
        initializeInvocation()
        val r1 = runInvocation()
        // second invocation run
        initializeInvocation()
        val r2 = runInvocation()
        // two invocations should return the same result
        check(r1 == r2)
     }
}

This change also simplifies implementation of the new features.

  • In Lincheck benchmarks #250 we need to collect the statistics of running each invocation (e.g. its running time). With the old API, this again would require the code duplication in all Strategy implementers.

  • In Single Lincheck options class with testingTime(..) option #158 we want to implement the adaptive dynamic selection of the number of invocations to be run. This change requires to offload the decision on how many times to run the scenario from the Strategy class into the Planner class. Again, with the new API this becomes trivial.

@eupp eupp requested a review from ndkoval January 22, 2024 15:30
@ndkoval
Copy link
Collaborator

ndkoval commented Feb 23, 2024

@eupp could you please rebase the PR onto develop?

@ndkoval
Copy link
Collaborator

ndkoval commented May 29, 2024

@eupp could you please rebase the PR?

@eupp eupp force-pushed the strategy-run-api branch from 8553cb5 to 2a7dd77 Compare May 30, 2024 12:28
@eupp
Copy link
Collaborator Author

eupp commented May 30, 2024

@eupp could you please rebase the PR?

Rebased.

@eupp eupp requested a review from ndkoval May 30, 2024 16:16
@ndkoval
Copy link
Collaborator

ndkoval commented Jun 11, 2024

@eupp please address the remaining minor comments and merge the PR 🎉

@eupp eupp force-pushed the strategy-run-api branch from 6071cb7 to 62926f4 Compare June 12, 2024 13:09
@eupp eupp merged commit ee568a5 into develop Jun 12, 2024
15 checks passed
@eupp eupp deleted the strategy-run-api branch June 12, 2024 15:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants