98-023 Concurrent and Distributed Programming with Inferno and Limbo (Spring 2004)



Course Outline

Inferno 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

1.     Inferno programming with Limbo, by P. Stanley-Marbell. John Wiley and Sons, 2003. ISBN: 978-0-470-84352-9

2.     The SPIN Model Checker, by G. J. Holzmann, Addison-Wesley, 2003. ISBN: 978-0321228628.


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

We will be using the CMU blackboard system to provide all course materials, updates, grades etc.
If you are registered for the course and log into blackboard, you should be able to access all the 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:    More about data types: ADTs and ref ADTs; Dis VM architecture and VM data types  [PDF]
Lecture 7:    Inferno kernel and emulator; Source tree; 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