By: Brannon (Brannon_Batson.delete@this.yahoo.com), September 3, 2007 7:12 am
Room: Moderated Discussions
Konrad Schwarz (no.spam@no.spam) on 9/2/07 wrote:
---------------------------
>Hi,
>
>you make frequent reference to EV7 and I see Brannon Batson's name in the patent
>list. Would you have any (more) indication that Lamport's Temporal Logic of Actions
>was used to validate the cache coherency protocol (or other parts)? I would like to know how well it fares in practice.
>
>Regards
>
>Konrad
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.
Brannon
---------------------------
>Hi,
>
>you make frequent reference to EV7 and I see Brannon Batson's name in the patent
>list. Would you have any (more) indication that Lamport's Temporal Logic of Actions
>was used to validate the cache coherency protocol (or other parts)? I would like to know how well it fares in practice.
>
>Regards
>
>Konrad
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.
Brannon