Descripció
Descriure arquitectures tals com sistmes multiprocessador amb cachés, sistemes multicomputador, xarxes d'interconnexió, etc... Aprendre a modelar arquitectures, amb notacions diverses, i a raonar sobre el seu funcionament correcte, a base de formulació de propietats amb notacions de la lògica matemàtica. Es tracta la problemàtica fonamental i omnipresent de la concurrència i la distribució.
Tipus assignatura
Optativa
Semestre
Primer
Crèdits
5.00
Coneixements previs

Arquitectura de computadors bàsica, programació sequèncial, lògica matemàtica bàsica, autòmats.

Objectius

Els alumnes adquireixen coneixements i desenvolupen les habilitats següents:

1.- Comprensió del funcionament d'arquitectures concretes.

2.- Saber modelar arquitectures amb paral.lelisme explícit i primitives de comunicació síncrona.

3.- Seber formular, sobre models, propietats bàsiques d'arquitectures, amb lògiques formals.

4.- Saber verificar propietats bàsiques de models senzills, amb mètodes inductius.

Continguts

1.- Arquitectures concretes. Alguna de les següents: processadors amb paral.lelisme a nivell
d'instrucció, xarxes d'interconnexió, sistemes multiprocessador amb cachés, etc ...

2.- Modelat amb paral.lelisme explícit i primitives de comunicació síncrona, semàfors i
monitors. Exemples sobre les arquitectures anteriors; p.e. modelat d'un planificador
de processador superescalar.

3.- Modelat semàntic amb màquines de transicions finites, FTSs. Atomicidad y validez de los
modelos. Exemples sobre multicomputadors i multiprocessadors.

4.- Formulació de propietats de models d'arquitectures. Amb lògica de primer ordre,
lògica temporal LTL i amb autòmats de paraules infinites.

5.- Verificació amb traces, inducció bàsica, mètode incremental, reforç de l'invariant,
altres ...

Metodologia

Clases magistrals i clases on es resolen problemes dialogant amb l'alumne. Proposta de dues
pràctiques a lliurar individualment, però havent dialogat amb altres alumnes i el professor. Les
pràctiques representen l'enfrontament amb una problemàtica nova i difícil, però són una excusa
excel.lent per portar al día l'asignatura i per aprendre dels numerosos errors i malplantejaments
fets per la major part dels alumnes. S'aprèn d'aquests errors quan les solucions són presentades
i dialogades a classe.
Existeixen apunts de la majoria dels temes.
Es cita i recomana la bibliografía fonamental per ampliar coneixements.

Avaluació

L'assignatura s'imparteix durant el primer quadrimestre i l'avaluació es fa a partir
d'un exàmen final escrit (A), un cop acabat el primer quatrimestre. El lliurament
de les pràctiques dins les dates anunciades és condició necessària per a poder
presentar-se a l'exàmen final. Hi ha una convocatòria adicional a setembre.
En la modalitat semipresencial es pot optar per l'avaluació contínua. Està basada
en donar un pés de 0,4 a les pràctiques. No obstant, degut a la forma d'aquestes,
és molt difícil aprovar-les, pel qual es desaconsella aquesta opció.

Criteris avaluació

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.

Bibliografia bàsica

Apunts:
Volun I : Introducció i descripció d'arquitectures
Volum II : Modelat d'arquitectures
Volum III : Especificació de propietats i modelat semàntic

Material complementari

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.