On Fri, 11 Jun 2010 19:31:58 +0200 Philippe Anel <x...@bouyapop.org> wrote: > > I only did my tests on 9vx. I have a version that I instrumented with > a circular log buffer, and I have some gdb macros which dumps the > buffer. > > I can put the whole source somewhere and even a log with my comments > of the bug if you want to see it. But please note that I made several
Yes, please. Thanks! > changes (because I had to understand how it works) and I would rather > copy my changes to the latest 9vx source tree so that everyone can > read it. What do you think ? Agreed. Best to check this in on a separate branch though. Branching/merging is cheap in hg. > Please, I would like to insist on the fact I'm not saying the promela > model is wrong. And I realize that the fix I propose might not be the > good one. Maybe the problem is even elsewhere. All these is just > feelings, logs and headache. I haven't used promela so can't say anything about it. sleep() is pretty complicated so figuring it out will take some time and effort but I first have to understand the cause and from past experience I know that code to check a cause hypothesis can be quite valuable (hence my earlier question). An unambiguous proof of what went wrong somehow frees my mind to better focus on the solution! Thanks for your thought experiements & code!
