  Reasoning about correctness and security of software is increasingly
difficult due to the complexity of modern microarchitectural features such as
out-of-order execution. A class of security vulnerabilities termed Spectre that
exploits side effects of speculative, out-of-order execution was announced in
2018 and has since drawn much attention. In this paper we formalise speculative
execution and its side effects with the intention of allowing speculation to be
reasoned about abstractly at the program level, limiting the exposure to
processor-specific or low-level semantics. To this end we encode and expose
speculative execution explicitly in the programming language, rather than
solely in the operational semantics; as a result the effects of speculative
execution are captured by redefining the meaning of a conditional statement,
and introducing novel language constructs that model transient execution of an
alternative branch. We add an abstract cache to the global state of the system,
and derive some general refinement rules that expose cache side effects due to
speculative loads. Underlying this extension is a semantic model that is based
on instruction-level parallelism. The rules are encoded in a simulation tool,
which we use to analyse an abstract specification of a Spectre attack and
vulnerable code fragments.
