Physical Sciences and Mathematics Commons^™

Operational Verification Of A Relativistic Program, Robert T. Bauer

Computer Science Faculty Publications and Presentations

Engineering eorts to achieve scalable multiprocessor perfor- mance for concurrent reader-writer programs have resulted in a family of algorithms that are non-blocking and that tolerate interprocessor in- terference. Because these algorithms accept a unique frame of reference for each processor's accesses to memory, they typify a concurrent pro- gramming technique for shared memory multicore architectures called relativistic programmming.

Rigorous verification of these algorithms is not possible with existing semantic based approaches because the semantics under approximates multiprocessor behavior and the algorithms rely on abstruse interactions with the operating system that aren't reconciled with language seman- tics.

The Read-Copy Update (RCU) …

The Design And Implementation Of A Safe, Lightweight Haskell Compiler, Timothy Jan Chevalier

Computer Science Faculty Publications and Presentations

Typed programming languages offer safety guarantees that help programmers write correct code, but typical language implementations offer no proof that source-level guarantees extend to executable code. Moreover, typical implementations link programs with unsafe runtime system (RTS) code. I present a compiler for the functional language Haskell that preserves some of the properties of Haskell’s type system. The soundness proof for the combination of the compiler and a verified RTS requires a proof that the compiler emits code that cooperates correctly with the RTS. In particular, the latter proof must address the boundary between the user program and the garbage collector. …