The pillars of the bridge on the cover of this book date from the Roman
Empire and they are in daily use today, an example of conventional
engineering at its best. Modern commodity operating systems are examples
of current system programming at its best, with bugs discovered and
fixed on a weekly or monthly basis. This book addresses the question of
whether it is possible to construct computer systems that are as stable
as Roman designs.
The authors successively introduce and explain specifications,
constructions and correctness proofs of a simple MIPS processor; a
simple compiler for a C dialect; an extension of the compiler handling C
with inline assembly, interrupts and devices; and the virtualization
layer of a small operating system kernel. A theme of the book is
presenting system architecture design as a formal discipline, and in
keeping with this the authors rely on mathematics for conciseness and
precision of arguments to an extent common in other engineering fields.
This textbook is based on the authors' teaching and practical
experience, and it is appropriate for undergraduate students of
electronics engineering and computer science. All chapters are supported
with exercises and examples.