More importantly, the rules in the execution model
determine how and when speculative effects happen.
For example, in a sequential semantics,
a conditional branch will evaluate its condition
then step to the appropriate branch.
A semantics that models branch prediction will instead predict
the condition result and step to the predicted branch.
We adapt notation from Guarnieri et al.  [1]}:
The \(\llbracket \,\cdot \, \rrbracket ^{\text{seq}}_{\text{}}\)  model represents standard sequential execution,
while \(\llbracket \,\cdot \, \rrbracket ^{\text{pht}}_{\text{}}\)  models prediction on conditional branches.
Other execution models are listed in tab:props.
