a
     
  Prof. Miquel Bertran Salvans  
  Docency  
     
 
Course on Advanced Architectures
  - Informatics Engineering programme
  - Prerequisites
  - Assumed knowledge
  - Overview
  - Objectives
  - Main topics
  - Methodology
  - Grading
  - Bibliography

Informatics Engineering programme
  - 3 hours per week. September through May.
  - 9 credits (ECTS).
  - Course taught in Catalan.

Prerrequisites
  - Programació 1 i 2.
  - Estructura de Computadors.
  - Computadors 2.
  - Llenguatges formals i teoria d'autòmats.
  - Lògica Matemàtica.

Assumed knowledge
  - Sequential programming.
  - Basic Architecture.
  - Logic.
  - Automata theory.

Overview

Modern architectures, together with their programming, which is necessary in applications, demand from the engineer informative knowledge plus the understanding of their operation principles. A deeper study of operational aspects requires knowledge of a new area for him: parallelism, with its concurrency and distribution ingredients.

A part of the subject is devoted to inform about many modern architectures: those involving one or more processors, interconnection networks among processors and memories, systems with parallel memories and with caches. Their operation and some design problems are also treated in this part.

Another part of the subject works on architecture modeling and programming. Entering into their more difficult aspects of concurrency and distribution. The simplifying assumptions, required in modeling and in reasoning with models, allow to work on the distinction between models and the real world. This adds a new general educational value, since the model-reality duality is present in all scientific thought.

The last part of the subject deals with property formulation and verification, frequently used nowadays in architecture design and in the design of applications, mainly when their correctness is critical for the safty of people or when large sums of money are at stake. Specification and verification of properties are always carried out on models. Thus the previous part prepares the student for the present one. Knowledge of this part will allow the engineer, in its professional live, to understand the computer aided verification tools and model checkers, which are everyday more present nowadays in the development of modern architectures and their applications.

Objectives
  1. To acquire a deeper knowledge of modern architecture structures and operation principles, both mono and multiprocessor.
  2. To educate on architecture modeling with the language constructs of parallelism and communications.
  3. To understand the new area, both basic and common to architecture modeling and programming, of concurrency and distribution.
  4. To learn how to express basic properties of the programs and models. To learn how to verify them following simple but mathematical methods.

Main topics
  1. Introduction. Parallelization and associated restrictions. Riscs or dependencies: structural,  data and control.
  2. Instruction level parallelism: RISC, Superescalars, dealing with riscs. Multithread and VLIW. Instruction scheduling.
  3. Introduction to interconnection networks. Crossbar, torus and hypercube. Static and dynamic  interconnection networks. Multistage dynamic networks. Temporal and spatial complexities.Multiprocessors and multicomputers.
  4. Caches in shared memory multiprocessors. Incoherency problem. Coherency and  consistency. Sufficient conditions for coherency and consistency. Various consistency protocols. Informal verification of these protocols.
  5. Introduction to architecture modeling with programs involving explicit parallelism constructs and communication statements. Communication selection statement. Modeling of time. Examples with the above architectures.
  6. Introduction to the basic assumptions of concurrency. Critical zones, mutual exclusion, deadlock, absence of individual starvation, etc... Mutual  exclusion granting techniques on multiprocessors: Dekker, Lamport, T&S, etc...
  7. Multiprocessor modeling and programming with semaphores and monitors. Specification and verification of properties. Model of a superscalar processor scheduler.
  8. Semantic modeling of parallel programs with finite transition machines. Specification of properties as invariants. Basic formal verification. Modeling with Kripke structures and finite automata over infinite words. Different formulations of equitativity.
  9. Specification of properties with linear temporal logic and with automta. Time modeling and formulation of temporal properties with timed automata.

Methodology
The subject is offered in two forms: with lectures (physical) and on-line. The work of the student, either alone or in group, is essential for the educational methodology. Homework is assigned, thus giding the student effort.
 
Lecture modality: The students attend the lectures, where concepts, techniques and descriptions are presented. Many examples and problems are also solved in class, in interleaved form with the latter items. Short problems, to be solved at home are proposed. Larger problems with deeper contents, to be solved at home and delivered to the teacher, are also assigned. A docency guide is displayied for the student at the virtual campus. He/she will find there references to specific parts of books where various explanations of the topics dealt with in the subject can be found.
 

On-line form: Instead of attending lectures, the student follows the subject development studying teaching material which is gradually displayied at the virtual campus, as the course progresses. He/she can also use the docency guide where he/she will be able to check his/her level by answering questionnaires. Apart from that, the other activities of the lecture modality are carried out as well.

Grading

The student level of knowledge, and the attainment of the above objectives, is evaluated by running exams, special work to be done at home, and student involvement in class.

Bibliography
- 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.
- Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems. Safety. Springer, New York, 1995
 - M. Bertran,  Apunts: Vol I Introducció a les arquitectures. Vol II Modelat. Vol III Especificació i modelat formals.  Arquitectura i enginyeria La Salle. Updated every year.
 - M.Bertran, Guia docent. Campus Virtual. Arquitectura i enginyeria La Salle. 2003.