• for

Courses:

Principles of Computer Systems >> Content Detail


Table of Contents



Calendar / Schedule



Calendar

This calendar provides the lecture topics, along with assignment due dates. Lectures given by Professors Lampson and Rinard are shown as "L" and "R," respectively, in the Lecturer column. The Handouts column indicates materials distributed in class.





LEC #LECTURERHANDOUTS #TOPICSPROBLEM SET # OUTPROBLEM SET # DUE
1LOverview. The Spec language, state machine semantics, examples of specifications and code1
1
2
3
4
5		Course information
Background
Introduction to Spec
Spec reference manual
Examples of specs and code
2LSpec and code for sequential programs. Correctness notions and proofs. Proof methods: abstraction functions and invariants
6Abstraction functions
3LFile systems 1: Disks, simple sequential file system, caching, logs for crash recovery21
7Disks and file systems
4LFile systems 2: Copying file system
5RProof methods: History and prophecy variables; abstraction relations32
8History variables
6RSemantics and proofs: Formal sequential semantics of Spec
9Atomic semantics of Spec
7LPerformance: How to get it, how to analyze it43
10Performance
11Paper: Michael Schroeder and Michael Burrows. "Performance of Firefly RPC," ACM Transactions on Computer Systems 8, 1, February 1990, pp 1-17.
8LNaming: Specs, variations, and examples of hierarchical namingForm groups
12Naming
13Paper: David Gifford, et al. "Semantic file systems," Proc.13th ACM Symposium on Operating System Principles, October 1991, pp 16-25.
9RConcurrency 1: Practical concurrency, easy and hard. Easy concurrency using locks and condition variables. Problems with it: scheduling, deadlock54
14Practical concurrency
15Concurrent disks
16Paper: Andrew Birrell, "An Introduction to Programming with Threads," Digital Systems Research Center Report 35, January 1989.
10RConcurrency 2: Concurrency in Spec: threads and non-atomic semantics. Big atomic actions. Safety and liveness. Examples of concurrency
17Formal concurrency
11RConcurrency 3: Proving correctness of concurrent programs: assertional proofs, model checking5
12RDistributed consensus 1. Paxos algorithm for asynchronous consensus in the presence of faults
13LDistributed consensus 2Early proposals
18Consensus
14RSequential transactions with caching
19Sequential transactions
15RConcurrent transactions: Specs for serializability. Ways to code the specsLate proposals
 







© 2009-2020 HigherEdSpace.com, All Rights Reserved.
Higher Ed Space ® is a registered trademark of AmeriCareers LLC.