Added synchronization to fix NPE bug in MessageHandler #72
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Tested by running several of the tests in the jkind testing directory looking for possible deadlocks and performance changes. There is a slight performance hit using synchronized for message passing (a few seconds, depending on the problem), and no deadlocks occurred.
|
It may be more performant to just add a try/catch block around the incoming.add call to trap NPEs, then check whether incoming is null, but this is also a little bit messier, maintenance-wise, and I'd rather not generate the NPE at all. |
|
Nice find. Thanks for tracking this down and making the fix. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
MWW, 8/27/2022
This PR fixes an occasional NPE bug that we have seen in jkind in the MessageHandler class. Within the class, the
receiveMessage and stopReceivingMessages methods run on different threads, leading to occasional NPE exceptions due to race conditions when solver is completing analyses.
NPEs happen when incoming is checked for null, but then receiveMessage thread is interrupted and incoming is set to null by stopReceivingMessages prior to incoming.add(message).
Note that other protected functions do not need to be synchronized because they are called on the same thread as stopReceivingMessages.
The fix was tested by running several of the tests in the jkind testing directory looking for possible deadlocks and performance changes. We also ran models that occasionally lead to NPEs that are internal. There is a slight performance hit using synchronized for message passing (a few % of execution, depending on the problem), and no deadlocks occurred. Furthermore, no NPEs were observed.