CSE 548T
- Concurrent Systems: Design & Verification
(Fall 2004)
(Formerly
CS 563T)
Catalin Roman
Class
Information
| Instructor | : Catalin Roman (935-6132) roman@wustl.edu |
| Meeting Time | : M-W 4:00 P.M. - 5:30 P.M. |
| Location | : Cupples I Room 218 |
| Prerequisites | : CSE 240 & CSE 241 (formerly CS 201 & CS 241) |
| Credit | : 3 units |
| Textbook | : Parallel
Program Design—A Foundation by K. M. Chandy and J. Misra |
| Grading | : They are assigned based on the homework alone. In order to obtain a passing grade, all homework must be completed. No late homework is accepted without instructor’s permission as solutions are discussed in class. All homework must be typeset. |
| Newsgroup | : wu.cse.class.548 |
Overview
Concurrency presents programmers with unprecedented complexity
further exacerbated by our limited ability to reason about concurrent computations.
Yet, concurrent algorithms are central to the development of software executing
on modern multiprocessors or across computer networks. This course reviews
several important classes of concurrent algorithms and presents a formal method
for specifying, reasoning about, verifying, and deriving concurrent algorithms.
The selected algorithms are judged to have made significant contributions to
our understanding of concurrency. Rigorous treatment of the design and programming
process is emphasized. Students entering this course must be familiar with
predicate calculus and sequential algorithms. Upon completion of this course
students will be able to reason completely formally about small concurrent
programs and to apply systematically and correctly their formal skills to larger
problems.
Homeworks
Homeworks will be assigned
in class. They will be due in class, and the due date will be determined when
the homework is handed out. All homeworks must be completed in order to pass
the class. All homeworks must be typeset.
[List of assigned
homeworks]
Syllabus
A. INTRODUCTION
1. Overview and motivation (Ch. 1)
B. UNITY MODEL
2. A programming notation (Ch. 2 & 6)
3. A programming logic (Ch. 3)
4. Sample proofs (Ch. 3)
5. More on programming logic (Ch. 3)
C. ARCHITECTURES AND MAPPINGS
6. Program schemas (Ch. 4)
7. Shortest path case study (Ch. 5)
8. Program structuring and composition (Ch. 7)
D. ALGORITHMS
9. Termination detection (Ch.9)
10. Mutual exclusion (Ch. 15)
11. Dining and drinking philosophers (Ch. 12,13)
12. Garbage collection (Ch. 16)
13. Global snapshots (Ch. 10)
E. OTHER MODELS
14. Swarm
15. Mobile UNITY
Links