Document Type

Technical Report

Publication Date

6-2009

Subjects

Functional programming (Computer science), Systems programming (Computer science), Linux, Operating systems (Computers), Algorithms

Abstract

Engineering e orts 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.

Description

Portland State University Computer Science Department Technical Report #09-04, 2009.

Persistent Identifier

https://archives.pdx.edu/ds/psu/30745

Download

Share

COinS