New model checker

[ndkoval]

We need to implement a better model checker with partial order reduction and weak memory models support.

The prototype is already available in eventstruct-mc. The remaining subtasks are listed below.

Refactorings and code maintanace:

• [x] Refactor LoopDetector (encapsulate code, moving most of it from ManagedStrategy.kt). Create a separate issue/pr for that. 3d.
• [x] Rebase on develop after #249 is merged and review the byte-code transformation. 5d.
• [x] Add an option (system property?) to use the new model checker instead of the current one. 1d.

Performance:

• [x] Optimize the consistency check: reduce the size of checked execution graphs (for example, remove events accessing thread-local objects, remove events accessing race-free variables, etc). 5d.
• [x] Add indexes for queries such as “get all events of type X for the variable Y starting from the event E”. 2.5d.
• [ ] Check whether specific byte-code generation for the primitive types (int, long, …) to avoid boxing/unboxing improves the performance. 2d.
• [ ] How many consistency checks fail? Should we optimize the interleaving generation phase or the consistency check itself?

Other:

• [ ] Repair trace collection in the new model checker (tests inside representation folder). This feature was temporarily disabled to simplify development. 3d.
• [ ] Check on the Kotlin Coroutines build. 5d.
• [x] Decide what the number of invocations should reflect: "consistent + inconsistent" or "consistent only". Decided: "consistent only".
• [ ] Code review. 5d.

Later:

• [ ] Evaluate the number of interleavings encoded by execution graphs (to compare with the current model checker)
• [ ] Write a technical report (white paper)
• [ ] Add reflection support
• [ ] Support weak memory model

[eupp]

New branch name for the strategy (after rebase to the new bytecode transformation): https://github.com/JetBrains/lincheck/tree/new-mc

[eupp]

Draft PR #410 (for tracking merge progress)