By: David Kanter (dkanter.delete@this.realworldtech.com), September 2, 2007 7:55 pm
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.
So, I can't really answer this question. However, Brannon wrote a paper with Leslie Lamport that discusses this:
http://citeseer.ist.psu.edu/cache/papers/cs/27523/http:zSzzSzresearch.microsoft.comzSzuserszSzlamportzSzpubszSzhigh-level.pdf/batson03highlevel.pdf
Perhaps you can get Brannon to share some thoughts on this paper...
DK
---------------------------
>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.
So, I can't really answer this question. However, Brannon wrote a paper with Leslie Lamport that discusses this:
http://citeseer.ist.psu.edu/cache/papers/cs/27523/http:zSzzSzresearch.microsoft.comzSzuserszSzlamportzSzpubszSzhigh-level.pdf/batson03highlevel.pdf
Perhaps you can get Brannon to share some thoughts on this paper...
DK