Portland State University. Department of Computer Science
Functional programming (Computer science), Systems programming (Computer science), Linux, Operating systems (Computers), Algorithms
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) algorithm is the protypical example of relativisitc programming; it is used in more than 2000 places in the Linux kernel and has thus far resisted analysis. In this paper a simple language for a sequentially consistent multiprocessor is defined and we implement RCU in that language. Both the RCU implementation and the language semantics are instrumented to prove that RCU does not collect live ob- jects and that it is memory safe; restrictions on the definition and use of local RCU pointers that eliminate the instrumentation are introduced. Thus, RCU implementations that conform to these restrictions do not collect live objects and are memory safe.
These restrictions are readily accommodated by program analysis tools to certify RCU implementations.
Bauer, Robert T., "Operational Verification of a Relativistic Program" (2009). Computer Science Faculty Publications and Presentations. 214.