On speculative computation and thread safe programming

We propose a formal definition for (valid) speculative computa-tions, which is independent of any implementation technique. By speculative computations we mean optimization mechanisms that rely on relaxing the flow of execution in a given program, and on guessing the values read from pointers in the memory. Our frame-work for formalizing these computations is the standard operational one that is used to describe the semantics of programming lan-guages. In particular, we introduce speculation contexts, that gen-eralize classical evaluation contexts, and allow us to deal with out of order (or parallel) computations. We show that the standard DRF guarantee, asserting that data race free programs are correctly im-plemented in a relaxed semantics, fails with speculative computa-tions, but that a similar guarantee holds for programs that are free of data races in the speculative semantics. We then introduce a lan-guage featuring an explicit distinction between shared and private variables, and show that there is a translation, guided by a type and effect system, that transforms a program written in this language into speculatively data race free code, which is therefore robust against aggressive optimizations. 1