Asynchronous state machines

[Rich Bodo]

Hi,

        This is rambling, possibly OT stuff so please ignore and
        forgive my intrusion if so.

        I used to know stuff.  Like how to diagram two cooperating
        asynchronous state machines and make sure they communicated
        consistently.  There was this cool class I took where we would
        make diagrams into tables into equations into silicon.  That
        was long ago.  Then, more recently, I found Spin, a protocol
        verification program.  I didn't have time to read the book.

        Recently, I decided that my time was being wasted by of the
        fact that most protocols I use are not verified, and most
        programs I use with complex state machines have never even had
        their state machines documented.  So I thought, "Hey, the hurd
        guys (and gals) must have been / are going through some pretty
        hairy examples of these same problems; I should ask them."

        Well, here I am.  I probably need to RTFM, but...

        Have anyone diagrammed the HURD state machines?  Verified the
        consistency of the same?  Am I nuts and possibly shooting
        e-mail to the wrong list (that I'm not even subscribed to)?

        Thank you.

-Rich

Rich Bodo | rsb@ostel.com | 650-964-4678