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:

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

Performance:

• 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.
• 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.
• 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)