The Barrelfish project is no longer active. See https://systems.ethz.ch/ for information about our current research activities.
Posted on June 08, 2017
Prior use, hardware components need to be initialized and configured, a task typically carried out by firmware, the operating system or device drivers. Devices are inhrently complex and requre a specific initialization sequence to function properly. A small mistake can lead an undefined state or even the destruction of the hardware device. In this post we show at the example of the MIPS R4600 TLB that it is impossible to always fulfill the required invariants stated in the device specification – even for such simple devices as the MIPS R4600 TLB.
We plan to release a couple of blog posts regarding our view of tasteful hardware. In this post we focus on the MIPS R4600 TLB, a hardware device which looks simple at the first glance however as always the devel lies in the details.
The MIPS R4600 contains a software loaded TLB and can be configured to use a 32-bit or 64-bit addressing scheme. We will focus on the 64-bit mode in this post.
The TLB is fully associative and consists of a total of 48 entry pairs each of which represents an odd and even page. Hence, the TLB is able to map a grand total of 96 pages of 4K-16M in size. Each entry pair can either be assigned to a particular address space or can be set as global. Each page has a few status bits including the valid or dirty bit indicating that the page is writable. Cache coherency settings can be configured on a per entry basis. The entries cam be divided into a set of wired entries and a set of entries that can be replaced randomly.
The mappable region in the MIPS R4600 address space is 40 bits (1TB) and the TLB translates the virtual address (i.e. virtual page number extended by the address space identifier) into a 36-bit physical address spanning a 64 GB physical address space. The TLB will perform the lookup in parallel finding a matching entry-pair for the input address. An entry matches (TLB Hit) if the virtual page number of the address and the entry match and either the entry is global or the ASID of the entry matches with the virtual address. Note that an entry-pair can match, despite both of its pages are marked as invalid.
There are four different management operations that can be used to query or update the TLB. All operations will move data from/to some special purpose registers into a TLB entry pair. There will always be a full entry pair read or written.
TLBRI: Read Indexed - this reads the TLB entry at a specific index, and
writes the contents into the registers.
TLBP: Probe - this reads the VPN and ASID from the register, probes the TLB for a match, and writes the matching index into a register or sets the no-match bit.
TLBWI: Write Indexed - this writes the contents of the registers into the TLB entry-pair at the specified index.
TLBWR: Write Random - this writes the contents of the registers into a random location of the TLB.
The documentation of the MIPS R4600 TLB clearly states that software must ensure that there is never the possibility that two entries match to the same input virtual address — in fact this condition would shutdown/destroy previous generations of this TLB. We can express this as
For any pair of entries e, e’ they must either not match or e==e’.
The MIPS R4600 TLB is not as simple as it seems at first. We now elaborate on the fact that the invariant stated above does not always holde – even with software taking great care not to write double-matching entries. It all starts with the reset sate.
There are two exceptions that transfer the processor into a well-know state — for some definition of well-known state. Both resets will put the processor to run in unmapped and uncached CPU address space hence the TLB and caches are bypassed and do not need to be initialized. At reset, the number of wired TLB entries is set to zero and the TLB will be fully operational i.e. there is no need to turn it on explicitely. Node, that the definition of the reset state does not specify the contents of the TLB entries which can be anything and therefore violate the invariant (even a fully zeroed out TLB would violate this).
This problem is somewhat circumvented by starting execution outside of the address range translated by the TLB effectively turning the invariant into a weaker form in the sense of “there must not be any address issued such that two entries match at the same time”. Proofing things with this type of invariants is hard even impossible.
We have defined a formal model of the TLB in Isabelle/HOL and we have proven that there exists a state which satisfies the reset condition and represents an invalid TLB state at the same time.
We have shown that satisfying the invariant is not possible. Ideally, we want a way to turn the TLB into a valid state without two entries that match on the same virtual address. Then we can formally specify and prove the semantics of operations such that transitioning from a valid state the TLB will always end up in another valid state. To improve the MIPS R4600 TLB to actually satisfy the invariant, there are two options:
Disable: at rest the TLB is disabled, software can bring the TLB into a known state and then enable the TLB.
Fully specified reset: At reset, the contents of the TLB will be initialized with known values. An example would be that entry-pair i has VPN 2i.
We have seen how a – at first glance – simple device such as the MIPS R4600 TLB can be taken as a counter example on how tasteful hardware not should look like. We also provide two possible ways to make it possible to always satisfy the invariant of the TLB.
If you would like to post a comment, please subscribe to our mailing list. There is also a public wiki server for Barrelfish information - please apply for an account if you want to contribute.