Terrier: an embedded operating system using advanced types for safety
OA Version
Citation
Abstract
Operating systems software is fundamental to modern computer
systems: all other applications are dependent upon the correct and
timely provision of basic system services. At the same time,
advances in programming languages and type theory have lead to the
creation of functional programming languages with type systems that
are designed to combine theorem proving with practical systems
programming. The Terrier operating system project focuses on
low-level systems programming in the context of a multi-core,
real-time, embedded system, while taking advantage of a dependently
typed programming language named ATS to improve
reliability. Terrier is a new point in the design space for an
operating system, one that leans heavily on an associated
programming language, ATS, to provide safety that has traditionally
been in the scope of hardware protection and kernel
privilege. Terrier tries to have far fewer abstractions between
program and hardware. The purpose of Terrier is to put programs as
much in contact with the real hardware, real memory, and real timing
constraints as possible, while still retaining the ability to
multiplex programs and provide for a reasonable level of safety
through static analysis.
Description
License
Attribution-ShareAlike 4.0 International