**Abstract:**

We propose a formal definition for (valid) speculative computations,
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 framework for formalizing these
computations is the standard operational one that is used to describe
the semantics of programming languages. In particular, we introduce
speculation contexts, that generalize classical evaluation contexts,
and allow us to deal with out of order computations. Regarding
concurrent programs, we show that the standard DRF guarantee,
asserting that data race free programs are correctly implemented in a
relaxed semantics, fails with speculative computations, but that a
similar guarantee holds for programs that are free of data races in
the speculative semantics.

[pdf]