Run init/post parts of the scenario in the 1st thread #146

eupp · 2023-03-17T18:50:30Z

Currently init and post parts of the scenario are run in the main thread. If some actor running in init/post part hungs, the lincheck hangs as well. Because of the similar reason, exceptions thrown in init/post part are not handled properly: instead of returning UnexpectedExceptionFailure lincheck fails with the thrown exception.

This PR fixes these problems. It fixes the runner and executor classes, so that init and post parts of the scenario are also run in separate threads.

New tests to check for hung and exception handling in init/post parts are added as well.

eupp · 2023-05-20T00:21:13Z

@ndkoval ready for review

ndkoval

@eupp, great job, thanks! I've suggested several improvements, please address them, and I'll review the PR again. Please also check how this change affects the performance.

src/jvm/test/resources/expected_logs/switch_as_first_method_event.txt

src/jvm/test/resources/expected_logs/state_representation.txt

src/jvm/test/resources/expected_logs/coroutine_cancellation.txt

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt

ndkoval · 2023-06-09T13:17:00Z

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/Runner.kt

+        strategy.beforePart(part)
+    }
+
+    fun afterPart(part: ExecutionPart) {


Can we provide executeInitPart, executeParallelPart, and executePostPart functions? Would it make the API more clear? Are there other solutions?

Yes we can do that.

But then, we have similar methods in the Strategy API. They are used to inform strategy about start of execution of particular scenario part. Currently, implementations of these methods in Strategy inheritors reset some internal state of the strategy between different scenario parts.

So how would you envision this API in Strategy then?
Or should we change Runner API, but left corresponding part of Strategy API as is?

I don't know which design is better. Please think about possible options, and let's discuss them (Slack?).
Also, consider making the strategy responsible for executing the init/post parts -- in this case, the runner API will be simpler.

I revisited it, but failed to completely remove beforePart and afterPart methods from the API.
As for the idea to make strategy responsible for running init/post parts, it seems there is also a couple of problems with it:

Currently, the runner owns the thread pool, it is private property of runner. Strategy cannot directly send tasks to the runner thread pool with the current API.

Both StressStrategy and ModelCheckingStrategy use the same init/post parts running logic (which is placed in ParallelThreadsRunner class that they both use). If we want to move that logic into Strategy we need to add another common class or something for both strategies to share this init/post parts running logic.

I propose to postpone this. Let's collect all the issues with the current Runner API in one places and discuss how they can be solved by some new API.

We now have only beforePart, don't we?

Please document beforePart and leave the rest for the future.

src/jvm/test/resources/expected_logs/state_representation.txt

src/jvm/test/resources/expected_logs/switch_as_first_method_event.txt

ndkoval · 2023-06-15T22:11:36Z

src/jvm/main/org/jetbrains/kotlinx/lincheck/strategy/managed/TraceReporter.kt

@@ -79,14 +70,30 @@ private fun splitToColumns(nThreads: Int, traceRepresentation: List<TraceEventRe
 */
 private fun constructTraceGraph(scenario: ExecutionScenario, results: ExecutionResult?, trace: Trace): TraceNode? {
    val tracePoints = trace.trace
+    // remap scenario actors: put init/post part into first thread
+    val remappedScenario = Array(scenario.threads) { i ->


I see a lot of logic here and there related to the init/post parts. Consider incorporating init/post parts into the first thread scenario part (as you depict when printing an error message), making the strategy responsible for executing init/post parts in the first thread at the beginning/end of the scenario. Would it simplify the overall design?

Would it simplify the overall design?

Yes, for sure. I agree that currently there is a lot of ad-hoc hacks for handling init/post parts in various places.
The only reason I have not fix it is because that would be a huge refactoring affecting a lot of places throughout the codebase.

There are a lot of places in the code that implicitly assume that init/post parts are executed in their own "virtual" threads (e.g. model checking code responsible for counting executed actors).

In order solve this problem nicely, we would also need to modify ExecutionScenario and similar classes (e.g. ExecutionResult, etc), i.e. all classes that mention init/post parts. That, in turn, would also require to review all the places where ExecutionScenario is used (and there are a lot of them), etc.

Besides, there are several possible solutions on how to handle this.
I think this problem is worth openning a separate issue where we can discuss pros/cons of various solutions.

I don't see why you must modify the ExecutionScenario class.

I've tried to address this problem and simplify thread and actors enumeration by putting all the related logic in ExecutionScenario and ExecutionResult classes.

There is still some room for improvement. For example, I was not able to refactor happens-before clock calculation logic --- it just too complicated and convoluted (because of bytecode generation). I think we first need to refactor TestThreadExecutionGenerator class and convert as much code as possible from bytecode generation to regular Kotlin code. I'll open an issue for this problem.

For now I come up with an intermediate solution that just rebuilds clocks inside ExecutionResult class.

Is this discussion up-to-date?

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/FixedActiveThreadsExecutor.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.kt

eupp · 2023-06-23T12:58:29Z

I rebased the branch on recent develop to resolve the conflicts.
Regarding the remaining refactorings, I propose to proceed with them after we will fix #196.

As for the performance, according to the CI builds, master and develop took around 20 mins, while this branch takes ~22 mins, so it looks like there is no significant performance degradation. I also do not see any degradation on my local machine.

CC @ndkoval

ndkoval

Thanks for the updates! Please address the remaining comments from the previous review and several new ones. After that, the PR should be ready to merge.

docs/topics/introduction.md

README.md

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.kt

src/jvm/main/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt

ndkoval · 2023-06-27T14:37:12Z

src/jvm/main/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.kt

+     * List containing for each thread its list of actors.
+     * Init and post parts are placed in the 1st thread.
+     */
+    val threads: List<List<Actor>> = (0 until nThreads).map { i ->


You do not need to copy the scenario. More importantly, you do not need this threads property -- just add a get(threadId, actorId) function.

Unfortunately, this is not that simple :(

In some cases, I also need, for example, to get the size of the particular thread (including init/post parts for the 1st thread). By having threads as a list, I have all the usual API for threads[0], e.g. size, indices, etc.
Otherwise, I need to somehow duplicate this API in ExecutionScenario class.

I actually tried the approach you suggest at first, but the code turned out to be more complicated.

If the memory consumption is a concern, we can also try another approach. We can have init, post and parallel[i] part lists as sub-lists of threads[i] lists.

Ok. Then maybe make ExecutionScenario : List<List<Actor>> by threads. Will it make code easier to read?

I cannot delegate to a property not passed into constructor.
There is a workaround with private primary constructor and public secondary constructor:
https://stackoverflow.com/a/71955281/4676150

Do we want to use it here?

If it makes the code easier to read, yes. You decide.

.../main/org/jetbrains/kotlinx/lincheck/strategy/managed/modelchecking/ModelCheckingStrategy.kt

ndkoval · 2023-06-27T14:40:54Z

Please also rebase on develop

docs/topics/operation-arguments.md

…cenario and trace output formats correspondingly

eupp requested a review from ndkoval March 17, 2023 18:52

ndkoval changed the title ~~Run init/post parts of the scenario in separate threads~~ Run init/post parts of the scenario in the 1st threads May 18, 2023

ndkoval changed the title ~~Run init/post parts of the scenario in the 1st threads~~ Run init/post parts of the scenario in the 1st thread May 18, 2023

eupp force-pushed the runner-fixes branch from e8433f2 to 12a9ff9 Compare May 18, 2023 23:01

eupp changed the base branch from master to develop May 18, 2023 23:02

ndkoval requested changes Jun 15, 2023

View reviewed changes

ndkoval assigned eupp Jun 17, 2023

eupp force-pushed the runner-fixes branch from c593e24 to 3a6eb6a Compare June 19, 2023 19:06

eupp requested a review from ndkoval June 20, 2023 18:14

eupp mentioned this pull request Jun 20, 2023

Simplify bytecode generation in TestThreadExecutionGenerator #196

Open

ndkoval requested changes Jun 21, 2023

View reviewed changes

eupp force-pushed the runner-fixes branch from 18bd044 to 765ed9a Compare June 23, 2023 11:47

ndkoval self-requested a review June 27, 2023 14:15

ndkoval requested changes Jun 27, 2023

View reviewed changes

eupp force-pushed the runner-fixes branch 2 times, most recently from 7e8ed8c to d86a555 Compare June 30, 2023 15:56

ndkoval reviewed Jun 30, 2023

View reviewed changes

docs/topics/operation-arguments.md Outdated Show resolved Hide resolved

ndkoval approved these changes Jun 30, 2023

View reviewed changes

Run init/post parts of the scenario in the 1st thread, changing the s…

3c59521

…cenario and trace output formats correspondingly

ndkoval force-pushed the runner-fixes branch from 1de6540 to 3c59521 Compare June 30, 2023 16:55

Run init/post parts of the scenario in the 1st thread, changing the s…

b238e1c

…cenario and trace output formats correspondingly

ndkoval merged commit 9334d85 into develop Jun 30, 2023

ndkoval deleted the runner-fixes branch June 30, 2023 18:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Run init/post parts of the scenario in the 1st thread #146

Run init/post parts of the scenario in the 1st thread #146

eupp commented Mar 17, 2023

eupp commented May 20, 2023

ndkoval left a comment

ndkoval Jun 9, 2023

eupp Jun 16, 2023

ndkoval Jun 16, 2023

eupp Jun 20, 2023 •

edited

Loading

ndkoval Jun 30, 2023

ndkoval Jun 30, 2023

ndkoval Jun 15, 2023

eupp Jun 16, 2023

ndkoval Jun 16, 2023

eupp Jun 20, 2023

ndkoval Jun 30, 2023

eupp commented Jun 23, 2023

ndkoval left a comment

ndkoval Jun 27, 2023

eupp Jun 29, 2023 •

edited

Loading

ndkoval Jun 30, 2023

eupp Jun 30, 2023

ndkoval Jun 30, 2023

ndkoval commented Jun 27, 2023

Run init/post parts of the scenario in the 1st thread #146

Run init/post parts of the scenario in the 1st thread #146

Conversation

eupp commented Mar 17, 2023

eupp commented May 20, 2023

ndkoval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eupp Jun 20, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eupp commented Jun 23, 2023

ndkoval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eupp Jun 29, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ndkoval commented Jun 27, 2023

eupp Jun 20, 2023 •

edited

Loading

eupp Jun 29, 2023 •

edited

Loading