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 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; }