Definition: A test measuring students knowledge of a set of concepts and also their conceptions and misconceptions.
Concept Inventories exist for some subfields of computer science but are missing for CS2 with its four basic ADTs, Algorithm Analysis, Programming Language Concepts and Compilers.
 |
The Hoist Project
Static Verification of Device Drivers
Image Copyright 2013 Thaddeus B. Kubis,
thad@tbkphotos.com
|
This project is exploring the use of type safe languages in writing or
verifying device drivers. The languages use an advanced type systems to
prevent data or IO misuse. Specifically, they only allow a thread to access
its own memory, they provide safe concurrency support, and support for pre-
and post-conditions to prove other properties about device drivers.
The language checks safety at compile time (statically) whenever possible.
project has focused on the needs of device drivers since studies have shown
that these contain most OS bugs. Our long term goal is to automate static
verification of the existing drivers in Linux to prove that they meet all
the saftey criteria or pinpoint where they fail.
Formal languages developed in this project include
Lambda-low which provides linear access to memory,
Lambda-concurrent which adds concurrency support (locks) to Lambda-low,
and Laddie (Language for Automated Device Drivers), a specification
language for the IO interface used between a driver and a device.
A formal language is expressed as a syntax and a type system that run on
an abstract machine using a set of evaluation rules. (It has proven properties
of soundness: preservation and progress). Formal languages are implemented
as concrete languages in order to actually use them.
The formal languages are implemented in concrete languages and
actual device driver code has been written in them and run in Linux on a
network card.
Lambda-low and Lambda-concurrent are implemented in Clay, a C-like
imperative language with linear access to memory, arithmetic constraints
on function pre- and post-conditions, and concurrency support. After
typechecking, Clay compiles to C++/C (user choice).
Laddie is implemented as a declarative
language which compiles to Clay.
The current phase of this project is a semi-automated translator
for existing C drivers to Clay.
Clay Files
- Please note: This is NOT the same language as the Clay created in 2011.
- Clay compiler
copyright
- Lea Wittie
Clay User's Guide, Bucknell TR #08-1
Tech Report 2008
- Chris Hawblitzel, Heng Huang, Lea Wittie, and Juan Chen.
A Garbage-Collecting Typed Assembly Language.
In TLDI, January 2007. (local copy)
- Chris Hawblitzel, Heng Huang, Lea Wittie, and Juan Chen.
A Garbage-Collecting Typed Assembly Language.
In Microsoft Technical Report TR-2006-169. (Gctal) Tech Report 2006
(local copy)
- Lea Wittie.
Type-Safe Operating System Abstractions, Ph.D. Thesis. In
Dartmouth Technical Report TR2004-526. (Lambda-concurrent)
Tech Report 2004 (local copy)
- Chris Hawblitzel, Heng Huang, and Lea Wittie.
Composing a well-typed region.
In Dartmouth Technical Report TR2004-521. (type safe memory access)
Tech Report 2004 (local copy)
- Heng Huang, Lea Wittie, and Chris Hawblitzel.
Formal Properties of Linear Memory Types.
In Dartmouth Technical Report TR2003-468. (Lambda-low)
Tech Report 2003 (local copy)
- Chris Hawblitzel, Edward Wei, Heng Huang, Erik Krupski, and Lea
Wittie.
Low-Level Linear Memory Management. In SPACE, January 2004.
(local copy)
Laddie Files
Translator from C to Clay (Language name needed) files
- Lianne Lairmore's Honors Thesis Report 2013 (coming soon)