This is an axiomatic description of how buddy caps appear to the user.
While it is precise and concise, it is, alas, hard to understand.
Below j, k and n are all non-negative integers.
“c” and “d” always denote a cap.
Some arithmetic:
For any j > 0, there is a unique pair (n, k) such that j = (2k+1)2n.
Every access to memory is via a memory cap and an integer offset.
We write A(c, j) to denote the byte or cap sized memory location accessed by cap c and offset j.
For every memory cap c there is a positive integer n such that for all integers j and k:
If 0 ≤ j < k < 2n then A(c, j) and A(c, k) are both valid and denote different memory locations.
There is just one such n and we write n = S(c).
If j ≥ 2S(c) then A(c, j) is invalid, yields nothing and results in some sort of safe fault.
There are the following machine ops:
- S takes a cap c and returns S(c).
- Sub takes a cap and integer, and yields a cap.
If n < S(c) then S(Sub(c, (2k+1)2n)) = n+1
If j < 2n+1 then A(Sub(c, (2k+1)2n), j) = A(c, 2n+1k+j).
- Loc takes two caps and yields an int:
If j < S(c) then Loc(c, Sub(c, j)) = j.
Loc yields 0 if the respective blocks are disjoint.
- Load takes a cap c, an int j and if j < S(c) returns the current contents of A(c, j).
- Store takes a cap c, an int j and a byte b, and if j < S(c) changes A(c, j) to hold b.
In plain words:
- S returns the log of the size of the memory block referred to by the cap.
- Sub derives a sub-cap to a specified sub-block from a cap to the super-block.
- Loc determines whether one cap is to a sub-block of the other, and if so says which sub-block.
- Load fetches the content of the byte of the sub-block of the cap, indexed by an int.
- Store changes the content of the byte of the sub-block of the cap, indexed by an int.
Of course the Load and Store ops must be designed to preserve the distinction between byte and cap.
Slight adjustments are required above for unsegregated cap designs.
To be integrated:
There exists a null cap d such that S(d) = −1 and for all c Sub(c, 0) = d.
There is a cap c such that S(c) = 56, or thereabouts.