Safety of Program Transformations in Shared-memory Concurrency

Опубликовано 7 сентября 2016, 17:14

Most programmers assume an interleaved semantics when reasoning about shared-memory concurrent programs. Unfortunately, even simple and widely implemented optimisations, such as constant propagation, violate the interleaved semantics. In this talk, I will argue that in absence of data races, interleaved semantics can be recovered for common classes of optimisations. My argument focuses on two classes of program transformations - eliminations and reorderings - which seem to explain most of the optimisations performed by realistic compilers. The core of the proof technique is trace semantic: programs are viewed as sets of action traces and transformations as relations on tracesets. This makes the proof largely independent of concrete language details.