This course will be based on readings of original papers.
Students are expected to
read the material in advance of the associated class meeting,
and to participate actively in discussion of the subject matter.
| Week of |
Topic(s) and Papers |
| 7 Sep 2004 |
Concepts, Terms, and Issues
| Note |
No class on Monday of this week (Labor Day)
|
| Lecture |
Issues in constructing robust, concurrent
systems. The notion of a ``unit of
operation.'' Limitations of testing as a tool
for program checking. Challenges in producing
and/or verifying correctness in complex
software systems.
|
|
| 13 Sep 2004 |
Transactions
| Readings |
Jim Gray and Jeri Edwards, ``Scale
Up with TP Monitors.'' Byte, April 1995.
[For those interested, the entire special
report can be found here.]
|
| Lecture |
Transaction processing as a tool for
concurrent update management. Locking and
concurrent update as a tool for preserving
correct sequential semantics in the face of
concurrency.
|
|
| 20 Sep 2004 |
Register Renaming
| Readings |
R. M. Tomasulo, ``An
Efficient Algorithm for Exploiting Multiple
Arithmetic Units.'' IBM Journal of
Research and Development, 11(1),
pp. 25-33, 1967.
T. Arons and A. Pnueli Verifying
Tomasulo's Algorithm by
Refinement. Technical Report MCS98-15,
Mathematics & Computer Science, Weizmann
Institute Of Science. 1998
James E. Smith and Andrew R. Pleszkin, ``Implementing
Precise Interrupts in Pipelined
Processors.'' IEEE Transactions on
Computing 17(5), pp. 562-573, May,
1968.
|
| Lecture |
Using internal concurrency while preserving
sequential computation semantics. How the
internals of modern microprocessors work.
|
|
| 27 Sep 2004 |
Confinement
|
| 4 Oct 2004 |
Limitations of Testing
| Readings |
Fill me in.
|
| Lecture |
Fill me in.
|
|
| 11 Oct 2004 |
Note: No class on Monday of this week (Fall Break)
|
Tuesday, October 17 |
|
Wednesday, October 18 |
|
| 18 Oct 2004 |
Static Checking
| Readings |
Hao Chen and Jonathan S. Shapiro ``Using
Build-Integrated Static Checking to Preserve
Correctness Invariants.'' Proc. 2004
Conference on Computer and Communications
Security (October, 2004).
|
| Lecture |
How execution in the EROS and KeyKOS kernels
is organized and restricted to support
reliability.
|
|
| 25 Oct 2004 |
Verification I
| Readings |
TBD
|
| Lecture |
Fill me in.
|
|
| 1 Nov 2004 |
Verification II
| Readings |
TBD
|
| Lecture |
Fill me in.
|
|
| 8 Nov 2004 |
BITC
| Readings |
TBD
|
| Lecture |
Fill me in.
|
|
| 15 Nov 2004 |
TBD
| Readings |
TBD
|
| Lecture |
Fill me in.
|
|
| 22 Nov 2004 |
TBD
| Readings |
TBD
|
| Lecture |
Fill me in.
|
|
| 29 Nov 2004 |
TBD
| Readings |
TBD
|
| Lecture |
Fill me in.
|
|
| 6 Dec 2004 |
Review and Summary
|
