Tony wrote:
I find it easier to think of constraints when I am
actually working with
them, and not when I am designing a tool that might come across them.
When I was working on this stuff, it was an iterative process. I'd discover
a potential race condition or the like, and edit a check for it into the
compiler. While debugging the compiler, I'd have it log a message every time
it found a situation where something had to be done in order to meet the
constraint. This sometimes resulting in the discovery that the same problem
potentially existed in other parts of the microcode.