After fighting with this for a couple of weeks I realise there's a race that hits on faster machines. I'm trying to work backwards now - using the sched/queue mechanism on spllower on the current implementation to understand the timing issues better.
It's been an intense week+ with little to show, but I've learned a lot. Ideally I would have wanted to model this using a formal specification, but since time is of importance I'm going to use the more straightforward method. I'll report back once I have something working. many thanks, Cherry -- Sent from my Android device with K-9 Mail. Please excuse my brevity.