make proofs generic in cacheLineBits #814

lsf37 · 2024-09-02T11:14:37Z

import cacheLineBits from config (only used on Arm, defined but unused on RISCV, fixed on x64)
check basic properties in Arch_Kernel_Config_Lemmas
remove all other unfoldings apart from cacheLineBits_val which is used in ARM and ARM_HYP to fold C values (safe, because the range of values for cacheLineBits is small)
the proof updates are similar between ARM and ARM_HYP, and a bit different in AARCH64, where most of it was already generic. They are now all based on the same principles.

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.

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>

Xaphiosis · 2024-09-06T03:31:50Z

proof/crefine/ARM_HYP/Wellformed_C.thy

+  apply (simp flip: mask_eqs(7))
+  done
+
+(* ------------ *)


Not a fan of this. It's not clear what it's for. Is it the end of the cache line bits, the end of the informal abstraction interface, or what.

You're right, what we usually do is error "..." -- I'll use that here as well.

Er, what? Why not remove it like it was previously and have two new lines to the next "section"? I don't think I know what error means in this context.

Sorry, my comment somehow went into the wrong box, it was supposed to be an answer to the next one down (the "Overwritten in Isabelle" bit).

For this one, the problem was that the entire configuration section has no end, it just keeps going into abbreviations for notifications etc, which is weird. You're right that the divider is not great either. I guess the proper way to do this would be to find a good name for whatever comes next.

At that point, it makes sense to give it a section/subsection for the configuration part, and/or end it with (* end of Kernel_Config interface section *) or something, then the general chaos can continue afterwards without a good name.

Xaphiosis · 2024-09-06T03:34:12Z

spec/haskell/src/SEL4/Machine/Hardware/ARM/Exynos4210.hs

@@ -164,7 +164,7 @@ cacheInvalidateL2RangeCallback _ _ _ = return ()
 cacheCleanL2RangeCallback :: Ptr CallbackData -> PAddr -> PAddr -> IO ()
 cacheCleanL2RangeCallback _ _ _ = return ()

-- For the ARM1136
+-- Overwritten in Isabelle


I don't like this phrase. Don't we have an existing one that makes sense already? I'm not sure it's "overwritten in Isabelle", but rather it's clobbered by the abstract spec, or (non-exclusive) it's not imported by the translator.

Or maybe unused by the design/exec spec ...

Ah, this is what the error comment was about. Yes, might be good to error them out.

Xaphiosis · 2024-09-06T03:38:10Z

spec/machine/AARCH64/Arch_Kernel_Config_Lemmas.thy

+
+(* 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. *)


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?

Xaphiosis · 2024-09-06T03:39:20Z

spec/machine/ARM/Arch_Kernel_Config_Lemmas.thy

+   not too large to conflict with other values used inside cache ops.
+   10 is ptBits, which is only available after ExecSpec. Anything smaller than ptBits works. *)
+lemma cacheLineBits_sanity:
+  "cacheLineBits \<in> {2..10}"


would it make sense to say ptBits for these instead of the ..10 or whatever and have a [simplified ptBits_def] or whatever on the lemma statement?

oh right, "which is only available after ExecSpec". Hmm. Nitpick: "anything smaller than" and "not 1" don't gel together well

Xaphiosis · 2024-09-06T03:53:10Z

proof/crefine/AARCH64/Wellformed_C.thy

+  by (simp add: pageBits_def)
+
+lemma pageBits_leq_pptrBaseOffset_alignment:
+  "pageBits \<le> pptrBaseOffset_alignment"


I'm a bit lost, is pptrBaseOffset_alignment related to cache line size?

yes, it's larger :-)

The relationship is that addrFromPPtr alignment is preserved by anything smaller or equal to pptrBaseOffset_alignment, which is what we need for the .. && mask cacheLineBits = ... lemma

Xaphiosis · 2024-09-06T03:56:05Z

proof/crefine/ARM_HYP/Wellformed_C.thy

+
+lemma ptBits_leq_pdBits:
+  "ptBits \<le> pdBits"
+  by (simp add: pt_bits_def pd_bits_def pde_bits_def pte_bits_def)


it's odd to me that the above two lemmas are in the cacheLineBits interface section

Xaphiosis · 2024-09-06T03:56:23Z

proof/crefine/ARM_HYP/Wellformed_C.thy

+  by (simp add: pd_bits_def APIType_capBits_def pde_bits_def)
+
+lemma cacheLineBits_le_PageDirectoryObject_sz:
+  "cacheLineBits \<le> APIType_capBits PageDirectoryObject us"


what's the intuition behind this constraint?

Xaphiosis · 2024-09-06T03:58:45Z

proof/crefine/ARM_HYP/VSpace_C.thy

@@ -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"


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

Xaphiosis · 2024-09-06T04:00:06Z

proof/crefine/ARM_HYP/VSpace_C.thy

+  "ccorres dc xfdc
+           (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs)
+                \<and> vs && mask cacheLineBits = ps && mask cacheLineBits
+                \<comment> \<open>ahyp version translates ps into kernel virtual before flushing\<close>


while we're here, could you change ahyp to arm-hyp?

Xaphiosis · 2024-09-06T04:06:28Z

proof/crefine/ARM/Retype_C.thy

-                            field_simps is_aligned_mask[symmetric] mask_AND_less_0)+
+                            field_simps is_aligned_mask[symmetric] mask_AND_less_0
+                            cacheLineBits_le_PageDirectoryObject_sz[unfolded APIType_capBits_def,
+                                                                    simplified])+


By the way, are you aware of @ from Rule_By_Method? We might be able to abbreviate these kinds of things with [@<simp add: APIType_capBits_def>]

(not needed in this one, but more general observation)

Xaphiosis · 2024-09-06T04:12:11Z

proof/crefine/ARM_HYP/Machine_C.thy

                   (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
           (doMachineOp (cleanCacheRange_PoU w1 w2 w3))
           (Call cleanCacheRange_PoU_'proc)"
  apply (rule ccorres_gen_asm)
  apply (cinit' lift: start_' end_' pstart_')
+   apply (fold cacheLineBits_val)


I think some kind of comment on this line (and in other lemmas) would be good, it's the linchpin of this whole exercise.

Xaphiosis

Minor comments and questions, else good. Nice to have these abstractions, updating this was a pain all the times we went 5->6->5

lsf37 added 6 commits September 1, 2024 11:42

word_lib: shiftr is always less than max word

32d3eba

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

haskell: mark cacheLineBits as overwritten in Isabelle

c376ee9

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

x64 machine: remove unused cacheLineBits

b19ef7b

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

arm+arm-hyp ainvs: remove unfoldings of cacheLineBits

2b3fa2e

None of the unfoldings of cacheLineBits turn out to be necessary. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 requested review from Xaphiosis and corlewis September 2, 2024 11:15

lsf37 added the platforms making proofs generic in platform and config settings label Sep 2, 2024

lsf37 force-pushed the cacheLineBits branch from f2da890 to 0526d2c Compare September 2, 2024 11:16

lsf37 added 2 commits September 2, 2024 12:30

arm+arm-hyp crefine: make proof generic in cacheLineBits

203aaa7

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 force-pushed the cacheLineBits branch from 0526d2c to e335f1f Compare September 2, 2024 11:31

Xaphiosis reviewed Sep 6, 2024

View reviewed changes

Xaphiosis approved these changes Sep 6, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

make proofs generic in cacheLineBits #814

make proofs generic in cacheLineBits #814

lsf37 commented Sep 2, 2024 •

edited

Loading

Xaphiosis Sep 6, 2024

lsf37 Sep 6, 2024

Xaphiosis Sep 6, 2024

lsf37 Sep 6, 2024

Xaphiosis Sep 9, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 9, 2024 •

edited

Loading

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

lsf37 Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis Sep 6, 2024

Xaphiosis left a comment

make proofs generic in cacheLineBits #814

Are you sure you want to change the base?

make proofs generic in cacheLineBits #814

Conversation

lsf37 commented Sep 2, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis Sep 9, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis left a comment

Choose a reason for hiding this comment

lsf37 commented Sep 2, 2024 •

edited

Loading

Xaphiosis Sep 9, 2024 •

edited

Loading