Message Channels

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…

Share

About Mathias

Software development engineer. Principal developer of DrJava. Recent Ph.D. graduate from the Department of Computer Science at Rice University.
This entry was posted in Concurrent Unit Testing. Bookmark the permalink.

Leave a Reply