Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

make proofs generic in cacheLineBits #814

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

make proofs generic in cacheLineBits #814

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
32d3eba
word_lib: shiftr is always less than max word
lsf37 Sep 1, 2024
c376ee9
haskell: mark cacheLineBits as overwritten in Isabelle
lsf37 Aug 30, 2024
185995b
arm+arm-hyp+aarch64 machine: cacheLineBits from kernel config
lsf37 Aug 30, 2024
b19ef7b
x64 machine: remove unused cacheLineBits
lsf37 Aug 30, 2024
2b3fa2e
arm+arm-hyp ainvs: remove unfoldings of cacheLineBits
lsf37 Aug 30, 2024
29f8314
arm-hyp ainvs+crefine: move masking lemmas for cacheLineBits
lsf37 Sep 1, 2024
203aaa7
arm+arm-hyp crefine: make proof generic in cacheLineBits
lsf37 Sep 1, 2024
e335f1f
aarch64 crefine: make proof generic in cacheLineBits
lsf37 Sep 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions spec/machine/AARCH64/Arch_Kernel_Config_Lemmas.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,5 +117,15 @@ lemma maxIRQ_1_plus_eq_Suc_machine[simp]:
"unat (1 + Kernel_Config.maxIRQ :: machine_word) = Suc Kernel_Config.maxIRQ"
by (simp add: Kernel_Config.maxIRQ_def)


(* cacheLineBits conditions *)

(* 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. *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

lemma cacheLineBits_sanity:
"cacheLineBits \<in> {2..12}"
by (simp add: cacheLineBits_def Kernel_Config.CONFIG_L1_CACHE_LINE_SIZE_BITS_def)

end
end
3 changes: 3 additions & 0 deletions spec/machine/AARCH64/Platform.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,9 @@ abbreviation (input) "fromPAddr \<equiv> id"
definition canonical_bit :: nat where
"canonical_bit = 47"

definition cacheLineBits :: nat where
"cacheLineBits = CONFIG_L1_CACHE_LINE_SIZE_BITS"

definition kdevBase :: machine_word where
"kdevBase = 0x000000FFFFE00000"

Expand Down
10 changes: 10 additions & 0 deletions spec/machine/ARM/Arch_Kernel_Config_Lemmas.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,5 +119,15 @@ lemma maxIRQ_1_plus_eq_Suc_machine[simp]:
"unat (1 + maxIRQ :: machine_word) = Suc Kernel_Config.maxIRQ"
by (simp add: Kernel_Config.maxIRQ_def)


(* cacheLineBits conditions *)

(* 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.
10 is ptBits, which is only available after ExecSpec. Anything smaller than ptBits works. *)
lemma cacheLineBits_sanity:
"cacheLineBits \<in> {2..10}"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

by (simp add: cacheLineBits_def Kernel_Config.CONFIG_L1_CACHE_LINE_SIZE_BITS_def)

end
end
2 changes: 1 addition & 1 deletion spec/machine/ARM/Platform.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ definition pageColourBits :: nat where
"pageColourBits \<equiv> 2"

definition cacheLineBits :: nat where
"cacheLineBits = 5"
"cacheLineBits = CONFIG_L1_CACHE_LINE_SIZE_BITS"

definition cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
Expand Down
10 changes: 10 additions & 0 deletions spec/machine/ARM_HYP/Arch_Kernel_Config_Lemmas.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,5 +131,15 @@ lemma maxIRQ_le_mask_irq_len:
using le_maxIRQ_machine_less_irqBits_val
by (fastforce simp add: word_le_nat_alt word_less_nat_alt irq_len_val mask_def)


(* cacheLineBits conditions *)

(* 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. *)
lemma cacheLineBits_sanity:
"cacheLineBits \<in> {2..12}"
by (simp add: cacheLineBits_def Kernel_Config.CONFIG_L1_CACHE_LINE_SIZE_BITS_def)

end
end
2 changes: 1 addition & 1 deletion spec/machine/ARM_HYP/Platform.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ definition pageColourBits :: nat where
"pageColourBits \<equiv> 2"

definition cacheLineBits :: nat where
"cacheLineBits = 6"
"cacheLineBits = CONFIG_L1_CACHE_LINE_SIZE_BITS"

definition cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
Expand Down