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.
[ ] Rebase on develop after #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:
[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)
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:
LoopDetector(encapsulate code, moving most of it from ManagedStrategy.kt). Create a separate issue/pr for that. 3d.developafter #249 is merged and review the byte-code transformation. 5d.Performance:
Other:
representationfolder). This feature was temporarily disabled to simplify development. 3d.Later: