I picked up my search for a way to correctly implement notifyAll in Promela again, and just before I had to teach Comp 212 lab, I found out about message chanels.
Channels provide two operations, channel!value and channel?variable, that send a value into a and receive a value from a channel, respectively. This is exactly what I needed! And I don’t even care about the contents, I just care about blocking. Both block until the value is received or sent, though, so I have to send exactly the right number of times, i.e. not at all if no thread is waiting.
Now I was able to implement primitives that very closely mimic the Java synchronization operations:
typedef WAITOBJ {
bool used = 0;
int lock = 0;
int count = 0;
chan signal = [0] of {bit}
}
#define monitorenter(obj) \
atomic { \
if \
:: (obj.lock==0) -> obj.lock = (_pid + 1); \
:: (obj.lock==_pid+1) -> skip; \
fi; \
}
#define monitorexit(obj) \
obj.lock = 0;
#define wait(obj) \
atomic { \
monitorexit(obj); \
obj.count = obj.count + 1; \
obj.signal?0; \
monitorenter(obj); \
}
#define notify(obj) \
atomic { \
if \
:: (obj.count > 0) -> { \
obj.signal!0; \
obj.count = obj.count - 1; \
} \
:: else -> skip; \
fi; \
}
#define notify\_all(obj) \
atomic { \
do \
:: (obj.count > 0) -> { \
obj.signal!0; \
obj.count = obj.count - 1; \
} \
:: else -> break; \
od; \
}
With these macros used in place of the synchronization code I had before, the code passes all four tests I have written, and it looks a whole lot cleaner. I have to admit, though, that the tests are very simple still…
