Lamport's TLA

Article: The Common System Interface: Intel's Future Interconnect
By: Brannon (Brannon_Batson.delete@this.yahoo.com), September 18, 2007 1:58 pm
Room: Moderated Discussions
Konrad Schwarz (no.spam@no.spam) on 9/18/07 wrote:
---------------------------
>Brannon (Brannon_Batson@yahoo.com) on 9/3/07 wrote:
>---------------------------
>>Yes, TLA was quite useful--as described in the paper David linked to. Please feel
>>free to post any additional questions here and I'll respond as best I can.
>
>So -- how well did it fare in practice/would you use it again?

It worked great--sure I'd use it again. CSI was my third project using it (we used it on Alpha Ev7 & Ev8, as well).

>
>TLA doesn't have an automated mapping from itself to logic circuits; did this manual
>step introduce many errors? [This question is coming from a safety perspective;
>you may know that other formal methods aim to make proveably correct software and try to eliminate these manual steps].

As you know, there's no simple answer to this question.

It's very important to focus on which class of bugs you are trying to find. There is a large and important class of bugs which can be found on an abstract representation of the design (protocol bugs). The industry experience has been that this class of bugs is notoriously difficult to find through traditional pre-silicon validation--and can be extremely disruptive to the design if found late. In some sense, these bugs exist before the design is started because they exist (however subtle) on the backs of napkins and whiteboards as architects are creating a complex protocol.

This motivates one to attempt to verify a protocol while the design is still in early stages. Another good reason for this is that formal verification gives you a quantification of the state space which is useful feedback during the design phase--it leads to simpler & easier to validate hardware.

So, the value of using an abstract specification is that one can verify a protocol very early in the design process, and one can use unbounded model checking on a reasonably-sized model which plausibly can fine all the bugs in a protocol. Unbounded model checking is probably the best way to attack a complex cache coherence protocol because one can write a small number of high-level invariants--and any bug in the spec will eventually manifest as a violation of one of these invariants. The invariants I use for coherence protocols are things like (a) there's no two lines in an 'exclusive' state at a time, (b) all requests eventually complete, and (c) a line in a clean state matches the value in memory.

We could attempt unbounded model checking on a more refined version of a protocol (like the actual RTL code or C code) but there are two important problems with this:
(1) first and foremost, there are going to be lots of implementation artifacts which pollute the state space. Queue's dramatically increase the width of the state graph and can therefore prevent you from exploring the entire state space.
(2) a particular implementation may restrict the behavior in an unintended way such that you miss a bug which will affect a later implementation. Using an abstract specification lends itself better to describing a superset implementation.

TLA+ happens to be a really good specification language because it is extremely high level with very elegant data structures, data manipulation, and ways of expressing nondeterminism. But there are others.

It would be nice to have a more graceful transition into a hardware descriptor language. I'm not aware of a language which is comparable to TLA+ for expressing abstract systems and is better than TLA+ for describing precise implementations--but it is not inconceivable that one could be created (or has been created). I honestly think it is more a question of the supported tools.

Anyway, to answer your question--yes there is a large class of bugs below the level of abstraction of a typical TLA+ spec, but those tend to be the type of bugs that traditional pre-silicon validation are pretty good at finding. I've seen some success in using an existing TLA+ spec to create high-value test vectors for stimulating an RTL implementation of that spec. There's various ways to do this.

A more formal strategy might involve bounded model checking against the low-level RTL itself. Or perhaps some sort of hierarchical term-rewriting to translate the high-level spec into the low-level RTL. Both are fraught with different kinds of peril.

A common mistake is in assuming that bugs are injected into the low-level implementation during a direct translation from some high-level spec (whether formal or English) due to the clumsiness of the hardware specification language. This is not the case. Overwhelmingly the bugs which exist below the abstraction of the high-level spec are due to features, algorithms, & data structures that are just not at all addressed by the high-level spec. The high-level spec often doesn't know anything about pipelining or reset behavior, asynchronous crossings, queues, arbiters, speculation, etc. For this reason, there is (in fact) limited utility to specifically addressing 'translation' bugs between different languages. The problem isn't the syntax, it's in the translation between layers of abstraction.

Put another way, there's nothing preventing me from writing a tool that can synthesize TLA+ into hardware. But, in order to produce good hardware--I need to write my TLA+ in a very low-level way that is aware of pipelining, queues, arbiters (etc.). At this point, I will very likely have injected the same bugs into my TLA+ that I would otherwise have injected into RTL.

What I gain, arguably, is the ability to more easily check the high-level version and the low-level version against one another only because there exists a tool which can aid me in that task (the TLA+ model checker, TLC). But I wouldn't call this an intrinsic value in using one language for everything.

>
>Regards,
>
>Konrad
>
>P.S.: This really is a pretty cool forum.

Brannon
< Previous Post in ThreadNext Post in Thread >
TopicPosted ByDate
New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/08/28 01:16 AM
  New article - The Common System Interface: Intel's Future InterconnectVincent Diepeveen2007/08/28 05:02 AM
  New article - The Common System Interface: Intel's Future InterconnectRichard Cownie2007/08/28 10:28 AM
    New article - The Common System Interface: Intel's Future InterconnectVincent Diepeveen2007/08/31 11:44 AM
      New article - The Common System Interface: Intel's Future InterconnectRichard Cownie2007/08/31 08:53 PM
        New article - The Common System Interface: Intel's Future InterconnectVincent Diepeveen2007/09/01 02:21 AM
          Adding layers can simplify designPaul A. Clayton2007/09/01 07:39 AM
          New article - The Common System Interface: Intel's Future InterconnectMichael S2007/09/02 02:25 AM
        New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/14 12:47 PM
    New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/09/14 08:47 PM
  New article - The Common System Interface: Intel's Future InterconnectPaul2007/08/28 11:04 AM
    New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/08/28 12:43 PM
      New article - The Common System Interface: Intel's Future InterconnectJoe Chang2007/08/28 06:17 PM
        New article - The Common System Interface: Intel's Future InterconnectJoe Chang2007/08/29 04:27 PM
  Thanks for the workWouter Tinus2007/08/28 12:33 PM
    Thanks for the workmac2007/08/29 12:44 PM
  New article - The Common System Interface: Intel's Future InterconnectHerbert Hum2007/08/28 01:22 PM
    ThanksDavid Kanter2007/08/28 04:13 PM
  Many thanks, very, very interesting! (NT)Cameron Jack2007/08/29 01:51 AM
  very nice article + memory ctrl integrationMarcin Niewiadomski2007/08/29 11:46 AM
    very nice article + memory ctrl integrationDavid Kanter2007/09/14 08:50 PM
      very nice article + memory ctrl integrationMarcin Niewiadomski2007/09/16 08:48 PM
  Coherency: Forwarding and OwnedPeter Gerdes2007/08/29 02:11 PM
    Coherency: Forwarding and OwnedDavid Kanter2007/08/29 06:29 PM
      Coherency: Forwarding and Ownednick2007/08/29 07:03 PM
        Coherency: Forwarding and OwnedDavid Kanter2007/08/29 11:08 PM
      Coherency: Forwarding and OwnedMichael S2007/08/30 01:17 AM
        Coherency: Forwarding and OwnedDavid Kanter2007/08/30 07:31 AM
      Coherency: Forwarding and OwnedPeter Gerdes2007/08/30 11:46 AM
        Coherency: Forwarding and OwnedDavid Kanter2007/08/30 01:46 PM
          Coherency: Forwarding and OwnedPeter Gerdes2007/08/30 07:03 PM
            Coherency: Forwarding and OwnedDavid Kanter2007/09/14 08:44 PM
              Node Interleaveunknown2007/09/15 03:14 AM
                Node InterleaveDavid Kanter2007/09/15 07:50 AM
                  Node InterleaveHoward Chu2007/09/16 12:14 PM
              Coherency: Forwarding and OwnedPeter Gerdes2007/09/16 12:50 PM
                Coherency: Forwarding and OwnedDavid Kanter2007/09/16 04:34 PM
                  Coherency: Forwarding and OwnedEduardoS2007/09/16 04:52 PM
                  Coherency: Forwarding and OwnedJonathan Kang2007/09/17 05:16 AM
                  Coherency: Forwarding and OwnedMatthias2007/09/17 06:59 AM
                    Coherency: Forwarding and Owned - additionMatthias2007/09/17 07:01 AM
                Coherency: Forwarding and Ownedanonymous2007/09/17 09:15 AM
                  Coherency: Forwarding and OwnedPeter Gerdes2007/09/17 12:44 PM
  New article - The Common System Interface: Intel's Future InterconnectMr. Camel2007/08/30 03:16 PM
    New article - The Common System Interface: Intel's Future InterconnectMichael S2007/08/31 01:11 AM
      New article - The Common System Interface: Intel's Future InterconnectMr. Camel2007/08/31 03:13 AM
        New article - The Common System Interface: Intel's Future InterconnectMichael S2007/08/31 03:24 AM
        New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/08/31 05:39 AM
          New article - The Common System Interface: Intel's Future InterconnectMichael S2007/08/31 06:53 AM
      New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/08/31 05:41 AM
        New article - The Common System Interface: Intel's Future InterconnectMichael S2007/08/31 06:36 AM
          New article - The Common System Interface: Intel's Future InterconnectMr. Camel2007/08/31 08:36 AM
  Thanks and excellent work!Jack A.2007/08/30 07:41 PM
  Lamport's TLAKonrad Schwarz2007/09/02 01:57 AM
    Lamport's TLADavid Kanter2007/09/02 07:55 PM
    Lamport's TLABrannon2007/09/03 07:12 AM
      Lamport's TLAKonrad Schwarz2007/09/18 10:21 AM
        Lamport's TLABrannon2007/09/18 01:58 PM
  New article - The Common System Interface: Intel's Future InterconnectJosé Javier Zarate2007/09/09 04:01 PM
  New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/16 05:42 PM
    Remote prefetchDavid Kanter2007/09/17 07:51 AM
  New article - The Common System Interface: Intel's Future InterconnectJigal2007/09/22 02:39 PM
    New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/09/22 04:35 PM
      New article - The Common System Interface: Intel's Future Interconnect8B/10B Latency2007/09/22 06:16 PM
        New article - The Common System Interface: Intel's Future Interconnectanon2007/09/22 08:05 PM
          New article - The Common System Interface: Intel's Future InterconnectDavid W. Hess2007/09/22 08:50 PM
            Clocking in CSIDavid Kanter2007/09/23 08:46 AM
              Hypertransport 3 AC CouplingDavid W. Hess2007/09/23 09:32 AM
                Hypertransport 3 AC Couplinganon2007/09/23 09:53 AM
                  Clocking lanesDavid Kanter2007/09/23 10:51 AM
        New article - The Common System Interface: Intel's Future InterconnectDavid Kanter2007/09/22 08:34 PM
          New article - The Common System Interface: Intel's Future InterconnectDavid W. Hess2007/09/22 09:10 PM
            New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/25 07:15 AM
          New article - The Common System Interface: Intel's Future InterconnectMichael S2007/09/23 01:06 AM
            New article - The Common System Interface: Intel's Future InterconnectDavid W. Hess2007/09/23 03:41 AM
            Serialization delayDavid Kanter2007/09/23 08:57 AM
              Serialization delayMichael S2007/09/23 11:20 AM
                Serialization delayDavid Kanter2007/09/23 12:43 PM
                  Serialization delayMichael S2007/09/24 12:40 AM
                    Serialization delayMichael S2007/09/24 04:28 AM
                    Serialization delayAaron Spink2007/09/24 12:19 PM
                      Serialization delayMichael S2007/09/25 03:38 AM
                        Serialization delayJonathan Kang2007/09/25 08:10 AM
                          Serialization delayDavid W. Hess2007/09/26 12:22 AM
                        Serialization delayAaron Spink2007/09/25 12:13 PM
                          Thank you (NT)Michael S2007/09/25 12:53 PM
                Serialization delayJonathan Kang2007/09/25 07:26 AM
                  Serialization delayMichael S2007/09/25 01:57 PM
                    Serialization delayJonathan Kang2007/09/26 05:24 AM
                      Serialization delayDavid W. Hess2007/09/26 06:39 AM
                        Serialization delayJonathan Kang2007/09/26 09:56 AM
                          Serialization delayDavid W. Hess2007/09/27 02:21 AM
                            Serialization delayJonathan Kang2007/09/27 04:36 AM
                              Serialization delayDavid W. Hess2007/09/27 05:31 PM
                      Serialization delayrwessel2007/09/26 01:26 PM
                        Serialization delayJonathan Kang2007/09/27 07:16 AM
                          Serialization delayrwessel2007/09/27 12:20 PM
                            Serialization delayJonathan Kang2007/09/28 04:38 AM
                              Serialization delayrwessel2007/09/28 01:00 PM
                                Serialization delayJonathan Kang2007/10/01 07:07 AM
                                  Cache coherent latencyDavid Kanter2007/10/01 07:20 AM
                                    Cache coherent latencyblaine2007/10/01 10:36 AM
                                      Critical word first on coherent interconnectsDavid Kanter2007/10/01 11:10 AM
                                        Does ccHT do critical word first?blaine2007/10/02 07:10 AM
                                    Cache coherent latencyJonathan Kang2007/10/01 12:34 PM
                                      Cache coherent latencyDavid Kanter2007/10/01 01:13 PM
                      Serialization delayMichael S2007/09/28 04:32 AM
                        Serialization delayanonymous2007/09/28 10:25 AM
                          Serialization delayMichael S2007/09/29 09:06 AM
        New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/25 07:05 AM
      New article - The Common System Interface: Intel's Future Interconnectjigal2007/09/23 12:37 PM
        CSI, PCI and HTDavid Kanter2007/09/23 12:46 PM
        New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/25 07:39 AM
          New article - The Common System Interface: Intel's Future Interconnectjigal2007/09/25 02:16 PM
            New article - The Common System Interface: Intel's Future InterconnectMichael S2007/09/26 03:14 AM
              New article - The Common System Interface: Intel's Future InterconnectAnonymous2007/09/26 09:41 AM
                New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/26 09:59 AM
            New article - The Common System Interface: Intel's Future InterconnectJonathan Kang2007/09/26 05:48 AM
Reply to this Topic
Name:
Email:
Topic:
Body: No Text
How do you spell avocado?