IndexOutOfBoundsException from ManagedStrategy.getConcurrentActorCausesBlocking
#275
Comments
|
I've locally modified Lincheck to not filter stacktraces. This way I've got the full stacktrace of the So it is indeed coming from Lincheck itself. |
durban
changed the title
IndexOutOfBoundsException from unclear sourceIndexOutOfBoundsException from ManagedStrategy.getConcurrentActorCausesBlocking
|
Hi @durban! Could you please check whether the issue still occurs with Lincheck 2.26? |
|
I've tried 2.26, and it fails the same way. The (unfiltered) stacktrace is this: So essentially the same as before, although some line numbers changed. |
|
Hi @durban ! PR #277 should fix the As you might see, the log contains the following line: I suspect it might be caused by the usage of Nevertheless, it can be seen, that the first issue detected by Lincheck is an active spin lock: This could be a sign of an actual live-lock, or a false positive bug report. No matter what, you can effectively disable live-lock detection by setting larger value for parameter def defaultModelCheckingOptions(): ModelCheckingOptions = {
....
increaseTimeout(new ModelCheckingOptions())
.addGuarantee(assumedAtomic)
.checkObstructionFreedom(true)
// this is the "fast" configuration from the Lincheck paper:
.iterations(30) // scenarios
.threads(2)
.actorsPerThread(3) // operations per thread
.invocationsPerIteration(1000) // run each scenario this much time (FIXME)
// end of "fast" configuration
.actorsBefore(2) // so that we don't work with empty data structures
.actorsAfter(1) // to have a chance of detecting inconsistent state left
.hangingDetectionThreshold(200)
}
If you think this live-lock is false positive, please report back so we can investigate further. |
|
For weak references support, we added a new tracking issue #279 |
|
Thanks for looking into this! I've looked at the output.txt you've attached, and some things are not clear to me: The There is also this part in the log: This looks like it shouldn't happen, regardless of the behavior of the tested code. Could this be the reason for the Finally about the |
Model checking mode generally relies on the fact that it can deterministically reproduce any execution of the program. It stores some data structure internally, that allows to do that, and the bytecode transformations ensure that we track all the events in the program that may cause non-determinism (like calls to
What happens with your test, is that the model checker discovers what it thinks is an active lock. In general, when the MC discovers some bug, it attempts to run the same interleaving leading to a bug yet another time -- but this time collecting the program trace on the road. Because of non-determinism it cannot replay the same execution, and thus the second time it obtains different results.
At least for now, the active lock detector suspects that program entered active lock whenever same operation hits specific code location N times (it usually happens when the code spins in a loop). The |
|
Thanks, that makes a lot of things much more clear to me. I'll try to look into what could be this spinlock (or spinlock-like thing). |
|
Thanks, that's good to hear! I'll recheck when the fix is released. |
|
The new release lincheck-2.27 should fix this issue. |
I think an
IndexOutOfBoundsExceptionmight be somehow thrown by Lincheck. I see in the code, that stacktraces are filtered; maybe that hides the exact source. EDIT: It is indeed thrown by Linchek, see below.Steps to reproduce (unfortunately I don't know how to minimize):
The
IndexOutOfBoundsExceptionlooks like this:Now, this doesn't make a lot of sense, I suspect due to the stacktrace filtering. To the best of my knowledge, my code doesn't use
ArrayListanywhere.For reference, more output:
The text was updated successfully, but these errors were encountered: