Caches and TLBs.
Some speculative semantics and tools
([1]}, [2]}, [3]}, [4]}) include abstract models of
caches, where the cache state captures which addresses may be in the cache at
a given time.
One could imagine also including detailed models of TLBs.
As discussed in subsec:leakage, modeling caches or TLBs is probably
not helpful, at least for mitigation or verification tools—not only does it
make the semantics more complicated, but it potentially leads to non-portable
guarantees.
In particular, including a model of the cache usually leads to the
\(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{cache}}\)  leakage model, rather than the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  or
\(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage models which provide stronger defensive guarantees.
Following in the tradition of constant-time programming in the
non-speculative world, it seems wiser for our analyses and mitigations to be
based on microarchitecture-agnostic principles as much as possible, and not
depend on details of the cache or TLB structure.
