6.826—Principles of Computer Systems 1999 Handout 2. Overview and Background 1 2. Overview and Background This is a course for computer system designers and builders, and for people who want to really understand how systems work, especially concurrent, distributed, and fault-tolerant systems. The course teaches you how to write precise specifications for any kind of computer system, what it means for an implementation to satisfy a specification, and how to prove that it does. It also shows you how to use the same methods less formally, and gives you some suggestions for deciding how much formality is appropriate (less formality means less work, and often a more understandable spec, but also more chance to overlook an important detail). The course also teaches you a lot about the topics in computer systems that we think are the most important: persistent storage, concurrency, naming, networks, distributed systems, transactions, fault tolerance, and caching. The emphasis is on careful specifications of subtle and sometimes complicated things, the important ideas behind good implementations, and how to understand what makes them actually work. We spend most of our time on specific topics, but we use the general techniques throughout. We emphasize the ideas that different kinds of computer system have in common, even when they have different names. The course uses a formal language called Spec for writing specs and implementations; you can think of it as a very high level programming language. There is a good deal of written introductory material on Spec (explanations and finger exercises) as well as a reference manual and a formal semantics. We introduce Spec ideas in class as we use them, but we do not devote class time to teaching Spec per se; we expect you to learn it on your own from the handouts. Because we write specs and do proofs, you need to know something about logic. Since many people don’t, there is a concise treatment of the logic you will need at the end of this handout. This is not a course in computer architecture, networks, operating systems, or databases. We will not talk in detail about how to implement pipelines, memory interconnects, multiprocessors, routers, data link protocols, network management, virtual memory, scheduling, resource allocation, SQL, relational integrity, or TP monitors, although we will deal with many of the ideas that underlie these mechanisms. Topics General Specifications as state machines. The Spec language for describing state machines (writing specs and implementations). What it means to implement a spec. Using abstraction functions and invariants to prove that a program implements a spec. 6.826—Principles of Computer Systems 1999 Handout 2. Overview and Background 2 What it means to have a crash. What every system builder needs to know about performance. Specific Disks and file systems. Practical concurrency using mutexes (locks) and condition variables; deadlock. Hard concurrency (without locking): models, specs, proofs, and examples. Transactions: simple, cached, concurrent, distributed. Naming: principles, specs, and examples. Distributed systems: communication, fault-tolerance, and autonomy. Networking: links, switches, reliable messages and connections. Remote procedure call and network objects. Fault-tolerance, availability, consensus and replication. Caching and distributed shared memory. Previous editions of the course have also covered security (authentication, authorization, encryption, trust) and system management, but this year we are omitting these topics in order to spend more time on concurrency and semantics and to leave room for project presentations. Prerequisites There are no formal prerequisites for the course. However, we assume some knowledge both of computer systems and of mathematics. If you have taken 6.033 and 6.042, you should be in good shape. If you are missing some of this knowledge you can pick it up as we go, but if you are missing a lot of it you can expect to have serious trouble. It’s also important to have a certain amount of maturity: enough experience with systems and mathematics to feel comfortable with the basic notions and to have some reliable intuition. If you know the meaning of the following words, you have the necessary background. If a lot of them are unfamiliar, this course is probably not for you. Systems Cache, virtual memory, page table, pipeline Process, scheduler, address space, priority Thread, mutual exclusion (locking), semaphore, producer-consumer, deadlock Transaction, commit, availability, relational data base, query, join File system, directory, path name, striping, RAID LAN, switch, routing, connection, flow control, congestion Capability, access control list, principal (subject) If you have not already studied Lampson’s paper on hints for system design, you should do so as background for this course. It is Butler Lampson, Hints for computer system design, Proceedings of the Ninth ACM Symposium on Operating Systems Principles, October 1983, pp 33-48. There is a pointer to it on the course Web page.6.826—Principles of Computer Systems 1999 Handout 2. Overview and Background 3 Programming Invariant, precondition, weakest precondition, fixed point Procedure, recursion, stack Data type, sub-type, type-checking, abstraction, representation Object, method, inheritance Data structures: list, hash table, binary search, B-tree, graph Mathematics Function, relation, set, transitive closure Logic: proof, induction, de Morgan’s laws, implication, predicate, quantifier Probability: independent events, sampling, Poisson distribution State machine, context-free grammar Computational complexity, unsolvable problem If you haven’t been exposed to formal logic, you should study the summary at the end of this handout. References These are places to look when you want more information about some topic covered or alluded to in the course, or when you want to follow current research. You might also wish to consult Prof. Saltzer’s bibliography for 6.033, which you can find on the course web page. Books Some of these are fat books better suited for reference than for reading cover to cover, especially Cormen, Leiserson, and Rivest, Jain, Mullender, Hennessy and Patterson, and Gray and Reuter. But the last two are pretty easy to read in spite of their encyclopedic character. Systems programming: Greg Nelson, ed., Systems Programming with Modula-3,