make proofs generic in cacheLineBits #814
Conversation
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
lsf37
force-pushed
the
cacheLineBits
branch
2 times, most recently
from
0526d2c
to
e335f1f
Compare
|
|
||
| (* Folding cacheLineBits_val in C functions only works reliably if cacheLineBits is not 1 and | ||
| not too large to conflict with other values used inside cache ops. | ||
| 12 is ptBits, which is only available after ExecSpec. Anything smaller than ptBits works. *) |
There was a problem hiding this comment.
This is a bit of a worry, since it's a purely syntactic restriction. What is the risk that the proofs will fail in the future due to the appearance of some other number that happens to be the same as cacheLineBits?
There was a problem hiding this comment.
The risk is very low. This code hasn't changed in a very long time, and it would be fairly strange to mention other numbers in these functions that happen to be in that cache line size range. The only other literal number that occurs in these functions before simplification is 1 (for loop counter increment and a few other expressions).
There was a problem hiding this comment.
(the upper range of the interval comes from the proof constraints)
| by (simp add: pd_bits_def APIType_capBits_def pde_bits_def) | ||
|
|
||
| lemma cacheLineBits_le_PageDirectoryObject_sz: | ||
| "cacheLineBits \<le> APIType_capBits PageDirectoryObject us" |
There was a problem hiding this comment.
what's the intuition behind this constraint?
There was a problem hiding this comment.
It's a side condition in Retype, specifically for the PoU flush invocation for page directories (hence page directory size). The actual number is just pdBits, but the symbolic input in Retype is the APIType_capBits form. I was trying not to unfold that there, because that makes other instances of APIType_capBits also numeric which makes it harder to distinguish where things are coming from.
| @@ -3129,18 +3130,13 @@ lemma ccorres_return_void_C': | |||
| done | |||
|
|
|||
| lemma is_aligned_cache_preconds: | |||
| "\<lbrakk>is_aligned rva n; n \<ge> 7\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x7F \<and> | |||
| addrFromPPtr rva \<le> addrFromPPtr rva + 0x7F \<and> rva && mask 6 = addrFromPPtr rva && mask 6" | |||
| "\<lbrakk>is_aligned rva n; n \<ge> 7\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x7F \<and> addrFromPPtr rva \<le> addrFromPPtr rva + 0x7F" | |||
There was a problem hiding this comment.
do you happen to know where the 7 and 0x7F come from here? I'm wondering if it's related to cache line size in any way, or from somewhere else
There was a problem hiding this comment.
It's from somewhere else, I don't remember which one it was exactly, but one of the page table related sizes. They were grouped together here because they are left over as word proof obligations in one of the big C guard implication goals at the end.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use generated CONFIG_L1_CACHE_LINE_SIZE_BITS as source of truth for the value of cacheLineBits The requirements for cacheLineBits are numeric: we need more than 1 and less than or equal to ptBits, which is only available as a constant after ExecSpec. 1 is excluded, because we want to be able to fold the value of cacheLineBits inside C cache operations, and 1 is mentioned as index increment. No other numerals conflict in these functions. The only observed values for cacheLineBits are 5 and 6 on Arm, but there is no need to be more restrictive than cacheLineBits_sanity. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
None of the unfoldings of cacheLineBits turn out to be necessary. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
addrFromPPtr_mask and ptrFromPAddr_mask are only needed for masking with cacheLineBits in CRefine. Move to CRefine where the rest of the cacheLineBits infrastructure is. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
On AArch64 we have so far only seen cacheLineBits = 6 in the kernel. To be future-proof, bring AArch64 proofs into line with AArch32 anyway, rename cacheLineSize to cacheLineBits to stay consistent, and make proof generic in cacheLineBits. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
lsf37
force-pushed
the
cacheLineBits
branch
from
e335f1f
to
9abc160
Compare
cacheLineBitsfrom config (only used on Arm, defined but unused on RISCV, fixed on x64)cacheLineBits_valwhich is used in ARM and ARM_HYP to fold C values (safe, because the range of values forcacheLineBitsis small)There is a bunch of commits. I think they make reasonable sense as logical units, but happy to be persuaded otherwise if people want more squashing.
This changes bring Cortex-A72 into the ARM/ARM_HYP range.