JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
545 stars 31 forks source link

Fix potential IndexOutOfBoundsException in curActorIsBlocking and concurrentActorCausesBlocking #277

Closed eupp closed 4 months ago

eupp commented 4 months ago

both properties access the current actor id actorId = currentActorId[iThread] but do not handle the case when actorId = -1, that is the case before any actor has started executing

ndkoval commented 4 months ago

Could you please add a test?

eupp commented 4 months ago

@ndkoval I've looked into this, and it seems it would be hard to trigger the error and make such test deterministic. For this problem to occur, it has to be the case, that one thread has started working and detected deadlock, while other threads has not yet started execution (i.e. did not call onActorStart for the first time). We have no control over threads execution order on this level.

One possible way to write test would be to manually create ModelCheckingStrategy instance and call its methods in specific order to trigger the error. Do you think we should take this path?

ndkoval commented 4 months ago

@eupp, in this case, I would suggest adding a comment describing why the added logic is required and leaving a link to this PR.

ndkoval commented 4 months ago

Maybe it would be better to rewrite the code in a way similar to

// <comment describing the issue>
if (actorId < 0) return null

thus, covering this weird path separately