Exercises in Style (Alpha Specifications)

• Autorzy: Abraham U. , Pinhas T.
• Języki publikacji: EN

Abstrakty

EN

We compare two documents: the Alpha Architecture Reference Manual (from Compaq Computer Corporation) and the TLA+ specification of the Alpha memory model (by Lamport, Sharma, Tuttle, and Yu). We compare the styles, the languages employed, and the fundamental assumptions (that is the basic frameworks of the two texts). We conclude that the TLA+ specification is not so much a formalization of the Alpha Reference Manual text as it is a translation into a different framework. We believe that a formalization of the Alpha Reference Manual can be useful, and we propose one.

Słowa kluczowe

EN

Alpha Reference Manual

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 54, nr 2,3
• Strony: 107--135
• Opis fizyczny: bibliogr. 9 poz.

Twórcy

autor

Abraham U.

autor

Pinhas T.

• Department of Mathematics and Computer Science, Ben-Gurion University, Be'er Sheva, Israel

Bibliografia

• [1] U. Abraham, Models for Concurrency, Gordon and Breach, 1999.
• [2] Concurrency without global states: a case study. In preparation.
• [3] Alpha Architecture Committee. Alpha Architecture Reference Manual. Digital Press, Boston, third edition, 1998.
• [4] J. Barwise, Admissible Sets and Structures. Springer 1975.
• [5] Compaq. Alpha Architecture Reference Manual. Compaq Computer Corporation, fourth edition, 2002. (Available at ftp.compaq.com/pub/products/alphaCPUdocs/alpha arch ref.pdf.)
• [6] L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, Vol. 7, No. 7, pp. 1-52, 1993.
• [7] L. Lamport. Specifying concurrent systems with TLA +. In Manfred Broy and Ralf Steinbrüggen, editors, Calculational system Design, pages 183-247, Amsterdam, 1999. IOS Press.
• [8] L. Lamport, M. Sharma, M. Tuttle, and Y. Yu. The Wildfire Challenge Problem. 2001.
• [9] Y. N. Moschovakis, Notes on Set Theory. Springer 1994.