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:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 | 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…
