Arquitectura básica de computadores, programación sequencial, lógica matemática básica, automatas.
Los alumnos adquieren los conocimientos y desarrollan las habilidades siguients:
1.- Comprensión del funcionamiento de arquitecturas concretas.
2.- Modelado de arquitecturas con paralelismo explícito y primitivas de comunicación síncrona.
3.- Formulación, sobre modelos, de propiedades básicas de arquitecturas, con lógicas formales.
4.- Verificación de propiedades básicas de modelos relativamente simples, con métodos inductivos.
1.- Arquitecturas concretas. Alguna de las siguientes: procesadores con paralelismo a
nivel de instrucción, redes de interconexión, sistemas multiprocesador con cachés, etc...
2.- Modelado con paralelismo explícito y primitivas de comunicación síncrona, semáforos y
monitors. Ejemplos sobre las arquitecturas anteriores; p.e. modelado de un planificador
de procesador superescalar.
3.- Modelado semántico con máquinas de transiciones finitas, FTSs. Atomicidad y validez de
los modelos. Ejemplos sobre multicomputadores y multiprocesadores.
4.- Formulación de propiedades de modelos de arquitecturas. Con lógica de primer orden,
lógica temporal LTL y con autómatas de palabras infinitas.
5.- Verificación con trazas, inducción básica, método incremental, refuerzo de invariantes, etc ...
Clases magistrales y clases de resolución de problemas, dialogando con los alumnos. Propuesta
de dos prácticas para entregar individualmente, pero pudiendo dialogar con otros alumnos y el
profersor. Las prácticas representan afrontar una problemática nueva y difícil, pero son una excusa
excelente para llevar al día la asignatura y para aprender de los numerosos errores i planteamientos
inadecuados de la mayor parte de los alumnos, al presentar y dialogar en clase las soluciones por el
profesor. Existen apuntes de la mayoría de los temas.
Se cita y recomienda la bibliografía fundamental para la ampliación de conocimientos.
La asignatura se imparte durante el primer cuatrimestre. La evaluación se basa en un examen
final escrito (A), ya acabado el primer cuatrimestre. La entrega de las prácticas dentro de las
fechas límite anunciadas es condición necesaria para presentarse al examen final. Hay una
convocatoria adicional en septiembre.
En modo semipresencial, se puede optar por la evaluación continuada, basada ésta en dar a
las prácticas un peso de 0,4. No obstante, debido a su forma y finalidad, es muy difícil aprobarlas,
por lo que se desaconseja esta opción.
1.- Comprensión del funcionamiento de arquitecturas concretas. (A) Examen escrito.
2.- Modelado de arquitecturas. (A) Examen escrito.
3.- Formulación, sobre modelos, de propiedades básicas de arquitecturas, con lógicas formales.
(A) Examen escrito.
4.- Saber verificar propiedades básicas de modelos simples. (A) Exámen escrito.
Apuntes:
Volum 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.