Why do people specify a protocol without publishing the state machines?
For better or worse I’ve started to become familiar with the OSCI TLM 2.0 standard, and have to ask the question “why has OSCI specified a protocol with out formally defining the state machine that implement the protocol?” I suspect the answer is because no one has formally defined the state machines or state transitions.
I’m motivated to ask this question because back in 1999ish at the University of Wisconsin we came to and published the conclusion that you can’t formally reason about the correctness of a cache coherence protocol with out formally defining the state machine that implement the protocol. To further this work a language for specifying state machine in the context of coherence protocols was developed that could generate documentation, PDF, HTML, and executable simulation code. I believe the first publication of this methodology was in:
Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol, Daniel J. Sorin, Manoj Plakal, Anne E. Condon, Mark D. Hill, Milo M. K. Martin and David A. Wood,
IEEE Transactions on Parallel and Distributed Systems, June 2002 (vol 13, number 6).
(Previously available as Dept. of Computer Sciences Technical Report CS-TR-2000-1412, March 2000.)
So given a methodology for clearly specifying complex protocols published in 2000 why isn’t OSCI using it (or something better) in 2008?