Basic computer architecture, sequential programming, basic mathematical logic, automata.
The student acquires the following knowledge and habilities:
1.- Comprehension of the behavior of concrete architectures.
2.- Architecture modeling with parallelism and synchronous communication operations.
3.- Formulation of basic properties of architecture models, with formal logic notations.
4.- Verification of basic properties of simple models, with inductive methods.
1.- Specific architechtures. Taken among the following: processors with instruction level parallelism,
interconnection networks, multiprocessors with cachés, etc ...
2.- Architecture modelling with explicit parallelism and synchronous communication operations,
semaphores and monitors. Examples taken from the above architectures; such as the modeling
of a superscalar processor scheduler.
3.- Semantic modeling with finite transition systems, FTSs. Atomicity and model validity.
Examples from both multicomputer and multiprocessor applications.
4.- Formulation of architecture model properties. In first order logic, linear temporal logic, and infinite
word automata.
5.- Verification with traces, basic induction, incremental induction, invariant strengthenning, etc ...
Regular and problem resolution lectures, with student interaction. Two work assignments to be
solved at home ultimately on an individual basis, but after optional interaction with the professor
or other students. These assignments put the student in frot of problems new and difficult for him;
but they are an excellent excuse for both keeping the study of the subject to date and for learning
from the errors and misconceptions made by most students. Learning from these errors takes
place when the solutions are discussed in class.
Notes of the majority of the subject materials are available.
Fundamental literature references are given for those wishing further learning on their own.
The subject is offered in the first quarter, and the student evaluation is based on a
written final exam (A), at the end of the first quarter.
Assignment submissio within deadlines is a necessary condition to take the exam.
An additional exam is offered in September.
In the on-line version of the subject, the student may choose a distributed evaluation
where the home assignments are given a weight of 0,4.
Nevertheless, this is not recommended due to the aims and difficulty of these
assignments.
1.- Comprehension of the behavior of concrete architectures. (A) written exam.
2.- Architecture modeling. (A) written exam.
3.- Formulation of basic properties of architecture models. (A) written exam.
4.- Verification of basic properties of simple models, with inductive methods. (A) written exam.
1.- Comprensió del funcionament d'arquitectures concretes. (A) Exàmen escrit.
2.- Modelat d'arquitectures. (A) Exàmen escrit.
3.- Formulació, sobre models, de propietats bàsiques d'arquitectures, amb lògiques formals.
(A) Exàmen escrit.
4.- Saber verificar propietats bàsiques de models senzills, amb mètodes inductius. (A) Exàmen escrit.
Notes:
Volun I : Introducció i descripció d'arquitectures
Volum II : Modelat d'arquitectures
Volum III : Especificació de propietats i modelat semàntic
John L. Hennessy & David A. Patterson. Parallel Computer Architecture.
A Hardware/Software Approach. Morgan Kaufman, San Francisco, 2003
David E. Culler, Jaswinder Pal Singh, with Anoop Gupta. Parallel Computer Architecture.
A Hardware/Software Approach, Morgan Kaufman, San Francisco, 1999
Kai Hwang, Advanced Computer Architectures, 6th Edition. McGraw-Hill, N.Y.,1993.
Zohar Manna, Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems.
Specification. Springer, New York, 1992.