On top of code-level errors, system software using I/O can have temporal and concurrency errors. Clay is a C-like, systems language that aimed for memory-safety using type-based techniques such as linear and singleton types. In this dissertation, Lea Wittie formalized safe “concurrency, locks, and system state needed for a device driver” using an abstract, machine model she proves sound and the types in Clay. She ports OSKit’s Ethernet driver from C to Clay to test the approach. The result is a driver safe for multithreaded environments: “guaranteed to obtain locks before using shared data; cannot cause FIFO to overflow or underflow; will only call I/O operations when invariants are satisfied.”

Note: Clay is one of languages that attempted temporal safety without GC before Rust. I linked to Lea Wittie’s homepage in case readers want more information on it.