98-023 Concurrent and Distributed Programming with Inferno and Limbo
Course OutlineInferno is an operating system for resource-constrained devices, developed at Bell-Labs, by the creators of Unix and C (among other things). It runs natively over a variety of microprocessor and platform architectures (ARM/SPARC/PowerPC/x86 and more), and is additionally available as an emulator, on many popular OS platforms (*BSD/Linux/Windows/Solaris/IRIX/Mac OS X and more). Limbo is a programming language that was created for developing applications for Inferno. A primary tenet in Inferno is the representation of resources as entries in a hierarchical name space, and the accessing of this namespace with a simple, unified protocol, whether resources are local or across a far-flung network. This idea of virtualisation of resources, which is borrowed from the Plan 9 operating system, is taken one step further with the virtualisation of the entire hardware architecture, through the use of a virtual machine. This course will provide an in-depth study of developing applications in Limbo, constructing distributed applications that take advantage of Inferno's architecture, and modeling and analysis of concurrent applications using tools such as model checkers. Recommended Textbooks Inferno programming with Limbo The SPIN Model Checker Syllabus: Week 1: Introduction to Inferno; Abstractions and Names Week 2: Overview of the Limbo programming language Week 3: Data Types in Limbo and the Dis VM Week 4: Inferno Kernel Overview Week 5: Inferno Kernel Device Drivers Week 6: NO CLASS Week 7: C applications as resource servers: Built-in modules and device drivers Week 8: Case study I building a distributed multi-processor simulator Week 9: Platform independent Interfaces: Limbo GUIs; Project Update Week 10: Programing with threads, CSP Week 11: Debugging concurrent programs; Promela and SPIN Week 12: Factotum, Secstore and Infernos security architecture Week 13: Case study II Edisong, a distributed audio synthesis and sequencing engine Meeting Time and Location: Time: MW 7:00pm to 7:50pm Location: PH A19C Credits: 3 This is a StuCo course. You should register through the normal CMU On Line Registration. Course Materials Slides from course Lecture 1: Course overview; Inferno overview; Relevant history [PDF] Lecture 2: Lecture 1 review; Abstraction and names; Resources as files [PDF] Lecture 3: Introduction to Limbo; Limbo language genealogy [PDF] Lecture 4: Limbo data types[PDF] Lecture 5: More Limbo data types; Project discussion [PDF] Lecture 6: A bit more about data types: ADTs and ref ADTs; Dis VM architecture and internal data types [PDF] Lecture 7: Inferno kernel and and emulator overview; Source tree and compilation tools; Compiling the emulator[PDF] Lecture 8: Emulator overview; Terminology; Emulator data structures[PDF] Lecture 9: Native kernel overview; Kernel compilation[PDF] Lecture 10: Native kernel initialization[PDF] Lecture 11: C applications as Inferno resource servers; Styx servers versus builtin modules[PDF] Lecture 12: Project ideas[PDF] Lecture 13: Building a distributed multiprocessor simulator using Inferno (part 1) Lecture 14: Building a distributed multiprocessor simulator using Inferno (part 2) Lecture 15: Circular mounts Lecture 16: Open discussion Lecture 17: Communicating Sequential Processes (CSP) [PDF] Lecture 18: More CSP examples[PDF] Lecture 19: A brief review of CSP; Introduction to SPIN and Promela [PDF] Miscellaneous files from course Native inferno disk images: inferno1440.img, infernogfx.img, infernogfx1440.img Promela example for discussing Limbo channels: limbochannels.pr Contact: PGP Public Key |