JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
564 stars 33 forks source link

Single Lincheck options class with `testingTime(..)` option #158

Open eupp opened 1 year ago

eupp commented 1 year ago

Closes #137, #150, #151

This PR deprecates StressOptions, ModelCheckingOption, and also StressCTest, ModelCheckingCTest annotations. Instead, new class LincheckOptions is 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 testingTime option.

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 mode option to LincheckOptions. 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 AbstractLincheckTest we can easily add new subset of tests for new behavior called testWithHybridStrategy. It will allow us to test each strategy individually, as well as hybrid automatic strategy implemented in this PR.

eupp commented 1 year ago

@ndkoval ready for re-review

eupp commented 1 year ago

@ndkoval

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, LincheckInternalOptions is renamed LincheckOptionsImpl class that implements LincheckOptions interface.