Courses:

Principles of Computer Systems >> Content Detail

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 #	LECTURER	HANDOUTS #		TOPICS	PROBLEM SET # OUT	PROBLEM SET # DUE


1	L			Overview. The Spec language, state machine semantics, examples of specifications and code	1


		1 2 3 4 5		Course information Background Introduction to Spec Spec reference manual Examples of specs and code


2	L			Spec and code for sequential programs. Correctness notions and proofs. Proof methods: abstraction functions and invariants


		6		Abstraction functions


3	L			File systems 1: Disks, simple sequential file system, caching, logs for crash recovery	2	1


		7		Disks and file systems


4	L			File systems 2: Copying file system


5	R			Proof methods: History and prophecy variables; abstraction relations	3	2


		8		History variables


6	R			Semantics and proofs: Formal sequential semantics of Spec


		9		Atomic semantics of Spec


7	L			Performance: How to get it, how to analyze it	4	3


		10		Performance


		11		Paper: Michael Schroeder and Michael Burrows. "Performance of Firefly RPC," ACM Transactions on Computer Systems 8, 1, February 1990, pp 1-17.


8	L			Naming: Specs, variations, and examples of hierarchical naming	Form groups


		12		Naming


		13		Paper: David Gifford, et al. "Semantic file systems," Proc.13th ACM Symposium on Operating System Principles, October 1991, pp 16-25.


9	R			Concurrency 1: Practical concurrency, easy and hard. Easy concurrency using locks and condition variables. Problems with it: scheduling, deadlock	5	4


		14		Practical concurrency


		15		Concurrent disks


		16		Paper: Andrew Birrell, "An Introduction to Programming with Threads," Digital Systems Research Center Report 35, January 1989.


10	R			Concurrency 2: Concurrency in Spec: threads and non-atomic semantics. Big atomic actions. Safety and liveness. Examples of concurrency


		17		Formal concurrency


11	R			Concurrency 3: Proving correctness of concurrent programs: assertional proofs, model checking		5


12	R			Distributed consensus 1. Paxos algorithm for asynchronous consensus in the presence of faults


13	L			Distributed consensus 2	Early proposals


		18		Consensus


14	R			Sequential transactions with caching


		19		Sequential transactions


15	R			Concurrent transactions: Specs for serializability. Ways to code the specs	Late proposals
			Course Home About\| FAQs\| Contact\| Advertising\| Terms of Service\| Privacy Policy © 2017 Coursepedia.com, by Higher Ed Media LLC. All Rights Reserved.

Courses:

Principles of Computer Systems >> Content Detail

Table of Contents

Calendar / Schedule