In Flight
Mark Miller expressed surprise that one of the recent security bugs to afflict Intel, fetched data that was not “in flight”. I do not have the paper in front of me now but I recall that malign code fetched that data under speculation. It fetched the data counter to MMU policy relying, I suppose, on the fact that the rules would be enforced before the speculative branch was reified.

If this much is right then it would presumably faster to cut off speculation upon MMU fetch prohibition. Perhaps this makes Mark’s “in flight” a rule to reason about.

Here is my sketch of speculation and branch prediction hardware that overcomes most but not all of the Intel problems. IBM introduced and some designs followed the concept of ASID. (“Address Space ID”) The hardware associated a small integer (6 or 8 bits) with the origins of a mapping tables for the MMU. This association was incrementally made upon execution of the privileged command which loaded the segment table origin. The integer accompanied each virtual address in the TLB and thus addresses from many different maps could inhabit the TLB at once. When the small integers were exhausted the whole TLB was reset and a new association began. The ASID was exposed to the programmer only to explain performance and the necessity not to assume that loading the control register was as good as a Purge TLB.

The first trick is to associate each branch prediction with a unique ASID. The second trick is to obey TLB rules even during speculation. I don’t know whether it is profitable to speculate in two ASID’s at once but if so the ASID would be part of the “speculation machinery”.

This would simplify arguments for finding and avoiding the Spectre and Meltdown problems. It would outright solve some of them.

I have not considered whether these two schemes are compatible with X86 architecture, They are with simpler machines on which Keykos and Unis have run.