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 #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 #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.
This PR proposes a simple refactoring of the
Strategy
class API.Motivation
Currently, the
Strategy
API provides the following method to run the scenario: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.
This PR proposes to change the API, so that the
Strategy
instead provides the method to run single invocation: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:
Thus, the pattern to run the strategy becomes as follows:
For deterministic strategies (like model checking strategy), consecutive calls of
runInvocation
withouthnextInvocation
calls, should lead to the same results:This change also simplifies implementation of the new features.
In #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 #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 thePlanner
class. Again, with the new API this becomes trivial.