Re: BoF session in Prague "Formal State Machines"
Fred Baker <fred@cisco.com> Fri, 09 February 2007 03:55 UTC
Received: from [127.0.0.1] (helo=stiedprmman1.va.neustar.com) by megatron.ietf.org with esmtp (Exim 4.43) id 1HFMqz-0004e2-RE; Thu, 08 Feb 2007 22:55:17 -0500
Received: from [10.91.34.44] (helo=ietf-mx.ietf.org) by megatron.ietf.org with esmtp (Exim 4.43) id 1HFMqy-0004dr-7A for cosmogol@ietf.org; Thu, 08 Feb 2007 22:55:16 -0500
Received: from sj-iport-5.cisco.com ([171.68.10.87]) by ietf-mx.ietf.org with esmtp (Exim 4.43) id 1HFMqr-0001il-Oi for cosmogol@ietf.org; Thu, 08 Feb 2007 22:55:16 -0500
Received: from sj-dkim-7.cisco.com ([171.68.10.88]) by sj-iport-5.cisco.com with ESMTP; 08 Feb 2007 19:55:09 -0800
X-IronPort-AV: i="4.13,303,1167638400"; d="scan'208"; a="387330577:sNHT51782492"
Received: from sj-core-4.cisco.com (sj-core-4.cisco.com [171.68.223.138]) by sj-dkim-7.cisco.com (8.12.11/8.12.11) with ESMTP id l193t9gg001345; Thu, 8 Feb 2007 19:55:09 -0800
Received: from xbh-sjc-221.amer.cisco.com (xbh-sjc-221.cisco.com [128.107.191.63]) by sj-core-4.cisco.com (8.12.10/8.12.6) with ESMTP id l193ssnN020398; Thu, 8 Feb 2007 19:55:08 -0800 (PST)
Received: from xfe-sjc-212.amer.cisco.com ([171.70.151.187]) by xbh-sjc-221.amer.cisco.com with Microsoft SMTPSVC(6.0.3790.1830); Thu, 8 Feb 2007 19:54:58 -0800
Received: from [10.0.0.96] ([10.21.99.69]) by xfe-sjc-212.amer.cisco.com with Microsoft SMTPSVC(6.0.3790.1830); Thu, 8 Feb 2007 19:54:57 -0800
In-Reply-To: <20070208204527.GA13732@sources.org>
References: <20070205202703.GB1731@sources.org> <45C845B5.7050201@gmx.net> <20070206212438.GA23042@sources.org> <71C245A9-A53C-4E44-B944-55381FBFA8E7@cisco.com> <20070208204527.GA13732@sources.org>
Mime-Version: 1.0 (Apple Message framework v752.3)
Content-Type: text/plain; charset="US-ASCII"; delsp="yes"; format="flowed"
Message-Id: <DF0756AA-496C-4057-89AA-079308CFCC1C@cisco.com>
Content-Transfer-Encoding: 7bit
From: Fred Baker <fred@cisco.com>
Date: Fri, 09 Feb 2007 09:24:53 +0530
To: Stephane Bortzmeyer <bortzmeyer@nic.fr>
X-Mailer: Apple Mail (2.752.3)
X-OriginalArrivalTime: 09 Feb 2007 03:54:57.0990 (UTC) FILETIME=[10DACE60:01C74BFE]
DKIM-Signature: v=0.5; a=rsa-sha256; q=dns/txt; l=4114; t=1170993309; x=1171857309; c=relaxed/simple; s=sjdkim7002; h=Content-Type:From:Subject:Content-Transfer-Encoding:MIME-Version; d=cisco.com; i=fred@cisco.com; z=From:=20Fred=20Baker=20<fred@cisco.com> |Subject:=20Re=3A=20BoF=20session=20in=20Prague=20=22Formal=20State=20Mac hines=22 |Sender:=20; bh=5ysS074cWYWxDmU9V8ehx1HrUV24Mjh8ZEvynzRRX80=; b=W1Fit9dGpiBmWMmdRkwaYi1Y+hBxg8OYabZkbdKdjI5uUeTAgr7w4NYQMgLHivn03HApyqVW di45RwYEz0iW3RNPp/w75bK/DBgpiWJQgYd5RxMRJMEG1XB+slOHLb1k;
Authentication-Results: sj-dkim-7; header.From=fred@cisco.com; dkim=pass (si g from cisco.com/sjdkim7002 verified; );
X-Spam-Score: 0.0 (/)
X-Scan-Signature: f66b12316365a3fe519e75911daf28a8
Cc: cosmogol@ietf.org
Subject: Re: BoF session in Prague "Formal State Machines"
X-BeenThere: cosmogol@ietf.org
X-Mailman-Version: 2.1.5
Precedence: list
List-Id: DIscussion on state machine specification in IETF protocols <cosmogol.ietf.org>
List-Unsubscribe: <https://www1.ietf.org/mailman/listinfo/cosmogol>, <mailto:cosmogol-request@ietf.org?subject=unsubscribe>
List-Archive: <http://www1.ietf.org/pipermail/cosmogol>
List-Post: <mailto:cosmogol@ietf.org>
List-Help: <mailto:cosmogol-request@ietf.org?subject=help>
List-Subscribe: <https://www1.ietf.org/mailman/listinfo/cosmogol>, <mailto:cosmogol-request@ietf.org?subject=subscribe>
Errors-To: cosmogol-bounces@ietf.org
Personally, I have used a fairly convoluted series of steps in designing state machines for various things; I have done it because I found the results useful. It uses a combination of a compiler- compiler language and a table-driven state machine. Let's take an intentionally complex example: TCP. A TCP session can be described as starting from and ending in the initial state of "no connection". From the initiator's perspective, there is a sequence (be gentle on me, I'm doing this from memory while waiting for a meeting to start) initiate: user-open {send SYN, start dead timer, start retransmit timer} [retransmit-timer {send SYN, restart retransmit timer}]* ( dead-timer {FAIL} | network-SYN-ACK {send empty data segment, restart dead-timer, restart retransmit timer ) the receiver has the opposite sequence starting with the receipt of a SYN segment from the network and ending with either the dead-timer or receipt of a subsequent segment. Constructing these rules and running them through YACC with the correct set of options gets me a state machine that is quite a bit more complex than the one in RFC 793 but in fact handles all the issues that a TCP implementation faces. The one change one makes to that state machine is changing reduction rules to jumps to the state that the reduction rule would place you in. The problem with it is statements like "{FAIL}". The constructed state machine tells one all the necessary states and all of the correct state transitions; it doesn't tell much about the error cases. For this, I wind up transcribing the YACC-produced state machine into a state table and filling in all of the error cases. I'm about to make a statement that, while it is true, will sound preposterous. I assure you that it is true. In 1983, working at Control Data, I designed an XNS SPP implementation that used what today we call VJ congestion avoidance procedures. I spent a lot of time getting the state machine correct. I then constructed a set of 'sed' processes (we were running unix v6 on a PDP 11/34) that did text edits to convert my state machine into the high level code for the protocol, and wrote a "language" of supporting routines; the counterpart to "send SYN" was, for example, a call to a routine that constructed a control packet to be sent to the peer with a certain set of calling parameters. Work that followed on that code related to optimization and setting parameters appropriately, but folks who later maintained it told me that they never found a protocol bug in it. Identifying and ensuring the correct handling of all the error cases is as important, perhaps more so, as handling the normal-and-correct transitions. I can't say I have ever found a language that does that well, including and perhaps especially SDL. On Feb 9, 2007, at 2:15 AM, Stephane Bortzmeyer wrote: > On Thu, Feb 08, 2007 at 12:24:19AM +0100, > Fred Baker <fred@cisco.com> wrote > a message of 50 lines which said: > >> Table-described state machines can in fact be machine- readable if >> they are designed to be. > > Nobody ever said the opposite. Cosmogol is very close from a > table-described state machine, by the way, although the syntax is very > different from a typical table but a table, or a Comogol description > are both just a list of tuples (current-state, transition, > next-state). > >> Now, you might not *like* to write programs that recognize ascii-art >> cells and find in them things like input names, new state names, >> conditionals, actions, and side-effects. > > Indeed. I challenge you to write a parser for the state machines of > RFC > 4006 :-) specially with the RFC headers and footers. > > We certainly could imagine a more table-like formal syntax with > delimiters like: > > OPEN | Close it | CLOSED > CLOSED | Open it | OPEN > OPEN | Blow it out"| GONE > > (or TeX's & sign) > > or with fixed-size cells like RFC 4006 attempts to do. > > Do you find it better? _______________________________________________ Cosmogol mailing list Cosmogol@ietf.org https://www1.ietf.org/mailman/listinfo/cosmogol
- BoF session in Prague "Formal State Machines" Stephane Bortzmeyer
- Re: BoF session in Prague "Formal State Machines" Hannes Tschofenig
- Re: BoF session in Prague "Formal State Machines" Stephane Bortzmeyer
- Re: BoF session in Prague "Formal State Machines" Hannes Tschofenig
- Re: BoF session in Prague "Formal State Machines" Fred Baker
- Re: BoF session in Prague "Formal State Machines" Frank Ellermann
- Re: BoF session in Prague "Formal State Machines" Stephane Bortzmeyer
- Re: BoF session in Prague "Formal State Machines" Fred Baker