From e21d4f2c36945e26f9ac841ecdfbab628cfa03e4 Mon Sep 17 00:00:00 2001
From: mww-aws <55661280+mww-aws@users.noreply.github.com>
Date: Mon, 29 Aug 2022 08:08:34 -0500
Subject: [PATCH] Added synchronization to fix NPE bug in MessageHandler (#72)

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.
---
 build.gradle                                     |  2 +-
 .../jkind/engines/messages/MessageHandler.java   | 16 ++++++++++++++--
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/build.gradle b/build.gradle
index 57f980af9..4c9ea1a2c 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,6 +1,6 @@
 import java.text.SimpleDateFormat;
 
-def jkind_version_base = '4.5.1'
+def jkind_version_base = '4.5.2'
 
 def buildTime() {
     def df = new SimpleDateFormat("yyyyMMddHHmm");
diff --git a/jkind/src/jkind/engines/messages/MessageHandler.java b/jkind/src/jkind/engines/messages/MessageHandler.java
index f03e21f9f..6a7800a6e 100644
--- a/jkind/src/jkind/engines/messages/MessageHandler.java
+++ b/jkind/src/jkind/engines/messages/MessageHandler.java
@@ -10,13 +10,25 @@
 public abstract class MessageHandler {
 	private BlockingQueue<Message> incoming = new LinkedBlockingQueue<>();
 
-	public void receiveMessage(Message message) {
+	// MWW, 8/27/2022
+	// receiveMessage and stopReceivingMessages 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. 
+	public synchronized void receiveMessage(Message message) {
 		if (incoming != null) {
 			incoming.add(message);
 		}
 	}
 
-	protected void stopReceivingMessages() {
+	protected synchronized void stopReceivingMessages() {
 		incoming = null;
 	}