In current implementation of MonitorTracker in model checking strategy, the monitor re-entrance information is lost when thread performs wait operation on some object. Thus upon wake-up the model checker just re-acquires a monitor once, but does not restore previous monitor re-entrance counter. This leads to a bug (see the new test added in this PR).
This PR fixes this problem by saving the information about lock re-entrance and then correctly restoring it.
In current implementation of
MonitorTracker
in model checking strategy, the monitor re-entrance information is lost when thread performswait
operation on some object. Thus upon wake-up the model checker just re-acquires a monitor once, but does not restore previous monitor re-entrance counter. This leads to a bug (see the new test added in this PR).This PR fixes this problem by saving the information about lock re-entrance and then correctly restoring it.