1: \newcommand{\etalchar}[1]{$^{#1}$}
2: \begin{thebibliography}{NGMG98}
3:
4: \bibitem[ABM93]{ABM89}
5: Y.~Afek, G.~Brown, and M.~Merritt.
6: \newblock Lazy caching.
7: \newblock {\em ACM Transactions on Programming Languages and Systems},
8: 15(1):182--205, 1993.
9:
10: \bibitem[AMP96]{AMP96b}
11: R.~Alur, K.L. McMillan, and D.~Peled.
12: \newblock Model-checking of correctness conditions for concurrent objects.
13: \newblock In {\em Proceedings of the 11th Annual IEEE Symposium on Logic in
14: Computer Science}, pages 219--228, 1996.
15:
16: \bibitem[Aro01]{Arons01}
17: T.~Arons.
18: \newblock Using timestamping and history variables to verify sequential
19: consistency.
20: \newblock In G.~Berry, H.~Comon, and A.~Finkel, editors, {\em CAV 01:
21: Computer-aided Verification}, Lecture Notes in Computer Science 2102, pages
22: 423--435. Springer-Verlag, 2001.
23:
24: \bibitem[BDH{\etalchar{+}}99]{BDH99}
25: E.~Bilir, R.~Dickson, Y.~Hu, M.~Plakal, D.~Sorin, M.~Hill, and D.~Wood.
26: \newblock Multicast snooping: {A} new coherence method using a multicast
27: address network.
28: \newblock In {\em Proceedings of the 26th Annual International Symposium on
29: Computer Architecture ({ISCA}'99)}, 1999.
30:
31: \bibitem[BGM{\etalchar{+}}00]{BGM00}
32: L.A. Barroso, K.~Gharachorloo, R.~McNamara, A.~Nowatzyk, S.~Qadeer, B.~Sano,
33: S.~Smith, R.~Stets, and B.~Verghese.
34: \newblock Piranha: a scalable architecture based on sigle-chip multiprocessing.
35: \newblock In {\em Proceedings of the 27st Annual International Symposium on
36: Computer Architecture}, pages 282--293. IEEE Computer Society Press, 2000.
37:
38: \bibitem[CE81]{ClarkeEmerson81}
39: E.M. Clarke and E.A. Emerson.
40: \newblock Design and synthesis of synchronization skeletons using
41: branching-time temporal logic.
42: \newblock In {\em Workshop on Logic of Programs}, Lecture Notes in Computer
43: Science 131, pages 52--71. Springer-Verlag, 1981.
44:
45: \bibitem[CGH{\etalchar{+}}93]{CGH93}
46: E.M. Clarke, O.~Grumberg, H.~Hiraishi, S.~Jha, D.E. Long, K.L. McMillan, and
47: L.A. Ness.
48: \newblock Verification of the {Futurebus+} cache coherence protocol.
49: \newblock In {\em Proceedings of the 11th IFIP WG10.2 International Conference
50: on Computer Hardware Description Languages and their Applications}, pages
51: 15--30, 1993.
52:
53: \bibitem[CH01]{CondonHu01}
54: A.E. Condon and A.J. Hu.
55: \newblock Automatable verification of sequential consistency.
56: \newblock In {\em 13th Symposium on Parallel Algorithms and Architectures}.
57: ACM, 2001.
58:
59: \bibitem[Com98]{alpha-manual}
60: Alpha~Architecture Committee.
61: \newblock {\em Alpha Architecture Reference Manual}.
62: \newblock Digital Press, 1998.
63:
64: \bibitem[Del00]{Delzanno00}
65: G.~Delzanno.
66: \newblock Automatic verification of parameterized cache coherence protocols.
67: \newblock In E.A. Emerson and A.P. Sistla, editors, {\em CAV 2000: Computer
68: Aided Verification}, Lecture Notes in Computer Science 1855, pages 53--68.
69: Springer-Verlag, 2000.
70:
71: \bibitem[EM95]{EirikssonMcMillan95}
72: {\'{A}}.Th. E{\'{\i}}riksson and K.L. McMillan.
73: \newblock Using formal verification/ $\!$analysis methods on the critical path in
74: system design: a case study.
75: \newblock In P.~Wolper, editor, {\em CAV 95: Computer Aided Verification},
76: Lecture Notes in Computer Science 939, pages 367--380. Springer-Verlag, 1995.
77:
78: \bibitem[GK97]{GibbonsKorach97}
79: P.B. Gibbons and E.~Korach.
80: \newblock Testing shared memories.
81: \newblock {\em SIAM Journal on Computing}, 26(4):1208--1244, 1997.
82:
83: \bibitem[GK01]{GlusmanKatz01}
84: M.~Glusman and S.~Katz.
85: \newblock Extending memory consistency of finite prefixes to infinite
86: computations.
87: \newblock In K.G. Larsen and M.~Nielsen, editors, {\em CONCUR 01: Theories of
88: Concurrency}, Lecture Notes in Computer Science,
89: Springer-Verlag, 2001.
90:
91: \bibitem[HQR99]{HQR99b}
92: T.A. Henzinger, S.~Qadeer, and S.K. Rajamani.
93: \newblock Verifying sequential consistency on shared-memory multiprocessor
94: systems.
95: \newblock In N.~Halbwachs and D.~Peled, editors, {\em CAV 99: Computer Aided
96: Verification}, Lecture Notes in Computer Science 1633, pages 301--315.
97: Springer-Verlag, 1999.
98:
99: \bibitem[ID96]{IpDill96}
100: C.N. Ip and D.L. Dill.
101: \newblock Better verification through symmetry.
102: \newblock {\em Formal Methods in System Design}, 9(1--2):41--75, 1996.
103:
104: \bibitem[KOH{\etalchar{+}}94]{KOH94}
105: J.~Kuskin, D.~Ofelt, M.~Heinrich, J.~Heinlein, R.~Simoni, K.~Gharachorloo,
106: J.~Chapin, D.~Nakahira, J.~Baxter, M.~Horowitz, A.~Gupta, M.~Rosenblum, and
107: J.~Hennessy.
108: \newblock The {S}tanford {FLASH} multiprocessor.
109: \newblock In {\em Proceedings of the 21st Annual International Symposium on
110: Computer Architecture}, pages 302--313. IEEE Computer Society Press, 1994.
111:
112: \bibitem[KP92]{KatzPeled92}
113: S.~Katz and D.~Peled.
114: \newblock Verification of distributed programs using representative
115: interleaving sequences.
116: \newblock {\em Distributed Computing}, 6(2):107--120, 1992.
117:
118: \bibitem[Lam78]{Lamport78}
119: L.~Lamport.
120: \newblock Time, clocks, and the ordering of events in a distributed program.
121: \newblock {\em Communications of the ACM}, 21(7):558--565, 1978.
122:
123: \bibitem[Lam79]{Lamport79}
124: L.~Lamport.
125: \newblock How to make a multiprocessor computer that correctly executes
126: multiprocess programs.
127: \newblock {\em IEEE Transactions on Computers}, C-28(9):690--691, 1979.
128:
129: \bibitem[Lam94]{Lamport94}
130: L.~Lamport.
131: \newblock The {T}emporal {L}ogic of {A}ctions.
132: \newblock {\em ACM Transactions on Programming Languages and Systems},
133: 16(3):872--923, 1994.
134:
135: \bibitem[LD92]{LoewensteinDill92}
136: P.~Loewenstein and D.L. Dill.
137: \newblock Verification of a multiprocessor cache protocol using simulation
138: relations and higher-order logic.
139: \newblock {\em Formal Methods in System Design}, 1(4):355--383, 1992.
140:
141: \bibitem[LLG{\etalchar{+}}90]{LLG90}
142: D.~Lenoski, J.~Laudon, K.~Gharachorloo, A.~Gupta, and J.~Hennessy.
143: \newblock The directory-based cache coherence protocol for the {DASH}
144: multiprocessor.
145: \newblock In {\em Proceedings of the 17th Annual International Symposium on
146: Computer Architecture}, pages 148--159, 1990.
147:
148: \bibitem[LLOR99]{LLOR99}
149: P.~Ladkin, L.~Lamport, B.~Olivier, and D.~Roegel.
150: \newblock Lazy caching in {TLA}.
151: \newblock {\em Distributed Computing}, 12(2/3):151--174, 1999
152:
153: \bibitem[McM01]{McMillan01}
154: K.L. McMillan.
155: \newblock Parameterized verification of the flash cache coherence protocol by
156: compositional model checking.
157: \newblock In {\em CHARME 01: IFIP Working Conference on Correct Hardware Design
158: and Verification Methods}, Lecture Notes in Computer Science,
159: Springer-Verlag, 2001.
160:
161: \bibitem[MS91]{McMillanSchwalbe91}
162: K.L. McMillan and J.~Schwalbe.
163: \newblock Formal verification of the {Encore Gigamax} cache consistency
164: protocol.
165: \newblock In {\em Proceedings of the International Symposium on Shared Memory
166: Multiprocessors}, pages 242--251, 1991.
167:
168: \bibitem[Nal99]{Nalumasu99}
169: R.P. Nalumasu.
170: \newblock {\em Formal Design and Verification Methods for Shared Memory
171: Systems}.
172: \newblock PhD thesis, University of Utah, 1999.
173:
174: \bibitem[NGMG98]{NGMG98}
175: R.P. Nalumasu, R.~Ghughal, A.~Mokkedem, and G.~Gopalakrishnan.
176: \newblock The `test model-checking' approach to the verification of formal
177: memory models of multiprocessors.
178: \newblock In A.J. Hu and M.Y. Vardi, editors, {\em CAV 98: Computer Aided
179: Verification}, Lecture Notes in Computer Science 1427, pages 464--476.
180: Springer-Verlag, 1998.
181:
182: \bibitem[PD95]{PongDubois95}
183: F.~Pong and M.~Dubois.
184: \newblock A new approach for the verification of cache coherence protocols.
185: \newblock {\em IEEE Transactions on Parallel and Distributed Systems},
186: 6(8):773--787, 1995.
187:
188: \bibitem[PD96]{ParkDill96}
189: S.~Park and D.L. Dill.
190: \newblock Protocol verification by aggregation of distributed transactions.
191: \newblock In R.~Alur and T.A. Henzinger, editors, {\em CAV 96: Computer Aided
192: Verification}, Lecture Notes in Computer Science 1102, pages 300--310.
193: Springer-Verlag, 1996.
194:
195: \bibitem[PSCH98]{PSCH98}
196: M.~Plakal, D.J. Sorin, A.E. Condon, and M.D. Hill.
197: \newblock Lamport clocks: verifying a directory cache-coherence protocol.
198: \newblock In {\em Proceedings of the 10th Annual ACM Symposium on Parallel
199: Algorithms and Architectures}, pages 67--76, 1998.
200:
201: \bibitem[QS81]{QueilleSifakis81}
202: J.~Queille and J.~Sifakis.
203: \newblock Specification and verification of concurrent systems in {CESAR}.
204: \newblock In M.~{Dezani-Ciancaglini} and U.~Montanari, editors, {\em Fifth
205: International Symposium on Programming}, Lecture Notes in Computer Science
206: 137, pages 337--351. Springer-Verlag, 1981.
207:
208: \bibitem[WG99]{sparc-manual}
209: D.L. Weaver and T.~Germond, editors.
210: \newblock {\em The {SPARC} Architecture Manual}.
211: \newblock Prentice Hall Inc., 1999.
212:
213: \bibitem[YML99]{YML99}
214: Y.~Yu, P.~Manolios, and L.~Lamport.
215: \newblock Model checking {TLA+} specifications.
216: \newblock In {\em CHARME 99: IFIP Working Conference on Correct Hardware Design
217: and Verification Methods}, Lecture Notes in Computer Science 1703, pages
218: 54--66. Springer-Verlag, 1999.
219:
220: \end{thebibliography}
221: