Single Lincheck options class with testingTime(..) option
#158
Conversation
| import org.jetbrains.kotlinx.lincheck.verifier.* | ||
| import org.jetbrains.kotlinx.lincheck.verifier.linearizability.* | ||
| import java.lang.reflect.* | ||
|
|
||
| /** | ||
| * Abstract configuration for different lincheck modes. | ||
| */ | ||
| @Deprecated( |
There was a problem hiding this comment.
Please also annotate with Kotlin's @Deprecated annotation as well. Let's use the ERROR level, thus, forcing users to update the code. Please also indicate here that both ModelChecking and Stress Options are deprecated and that LincheckOptions incorporates both these functionalities.
| * we print the code location where this atomic method is called | ||
| * instead of going deeper inside it. | ||
| */ | ||
| private fun isTrustedPrimitive(className: String) = |
| * (e.g., due to a switch to another thread), and omits all the details except for | ||
| * the method invocation result. | ||
| */ | ||
| fun verboseTrace(verboseTrace: Boolean = true) = apply { |
| /** | ||
| * Set logging level, [DEFAULT_LOG_LEVEL] is used by default. | ||
| */ | ||
| fun logLevel(logLevel: LoggingLevel) = apply { |
There was a problem hiding this comment.
No need to have it in the API.
| * | ||
| * @see ExecutionScenario.postExecution | ||
| */ | ||
| fun actorsAfter(actorsAfter: Int) = apply { |
There was a problem hiding this comment.
You don't need this parameter.
| * | ||
| * @see ExecutionScenario.initExecution | ||
| */ | ||
| fun actorsBefore(actorsBefore: Int) = apply { |
There was a problem hiding this comment.
You don't need this parameter.
| * | ||
| * @see ExecutionScenario.parallelExecution | ||
| */ | ||
| fun actorsPerThread(actorsPerThread: Int) = apply { |
There was a problem hiding this comment.
It should be operationsPerThread. Let's get rid of the word "actor".
| private const val INVOCATIONS_LOWER_BOUND = 1_000 | ||
|
|
||
| // upper bound of invocations allocated by iteration | ||
| private const val INVOCATIONS_UPPER_BOUND = 100_000 |
There was a problem hiding this comment.
Does it work well with the current model checker? I guess the tests will fail with OutOfMemoryError.
| @Deprecated( |
There was a problem hiding this comment.
Please deprecate with both Java's and Kotlin's @Deprecated annotation.
| if (options.mode == LincheckMode.Hybrid && mode == LincheckMode.Stress) { | ||
| // try to reproduce an error trace with model checking strategy | ||
| createStrategy(LincheckMode.ModelChecking, testClass, minimizedFailure.scenario, testCfg, testStructure) | ||
| .run(verifier, MODEL_CHECKING_INVOCATIONS_COUNT) |
There was a problem hiding this comment.
Please make sure that if the model checking mode fails here (e.g., throws some exception due to non-determinism), the user still can get the output from the stress mode
ndkoval
changed the title
testingTime(..) option
Signed-off-by: Evgenii Moiseenko <[email protected]>
|
@ndkoval ready for re-review |
|
I still have a small concern with respect to extensive use of internal API in tests. Maybe we should consider keeping some common options in public API? Also, currently the following code pattern is used to access internal API in tests: LincheckOptions {
this as LincheckOptionsImpl
maxThreads = 2
maxOperationsInThread = 2
mode = LincheckMode.ModelChecking
}Maybe replace it with the following pattern? In my opinion it better reflects the intention here: LincheckInternalOptions {
maxThreads = 2
maxOperationsInThread = 2
mode = LincheckMode.ModelChecking
}here, |
…with fixed number of iterations and invocations Signed-off-by: Evgenii Moiseenko <[email protected]>
Signed-off-by: Evgenii Moiseenko <[email protected]>
Signed-off-by: Evgenii Moiseenko <[email protected]>
Closes #137, #150, #151
This PR deprecates
StressOptions,ModelCheckingOption, and alsoStressCTest,ModelCheckingCTestannotations.Instead, new class
LincheckOptionsis introduced to configure Lincheck run.Configuration of scenarios number and invocations per iteration number is also deprecated.
Instead, now the preferred way to configure Lincheck run is through single
testingTimeoption.Adaptive strategy to adjust scenarios and invocations numbers dynamically during the run is implemented (see class
Planner).The implementation tracks the average execution time over last N invocations.
Using the average execution time, the estimated remaining time is computed.
If the estimated time is greater (smaller) that allocated testing time by an order of magnitude (K times),
number of invocations is multiplied (divided) by a constant K.
If the estimated time is greater (smaller) that allocated testing time (but not that significantly), number of scenarios is increased (decreased) by a constant I.
For debugging purposes, I also add logging of invocations count and execution time after each iteration.
Besides that, the following logic is implemented:
As a backward compatibility (and for a transition period), I left the possibility to manually set strategy (stress or model checking), number of scenarios and number of invocations per scenario.
To configure strategy, I added
modeoption toLincheckOptions.Currently it is visible to the end user, but perhaps we want to hide it.
Other deprecated options also left visible, we can hide them if necessary.
I have not touch existing tests. Some of them manually set number of scenarios/invocations.
For test classes derived from
AbstractLincheckTestwe can easily add new subset of tests for new behavior calledtestWithHybridStrategy.It will allow us to test each strategy individually, as well as hybrid automatic strategy implemented in this PR.