9 Commits

Author	SHA1	Message	Date
Gerwin Klein	bfb390f918	CAVEATS: verification update; remove clang problem ... - add new platforms supported by verification - remove 32-bit imx8mm with FPU (proof out of date) - add AArch64 integrity - add FPU where covered - remove caveat on lazy FPU and VCPU switching (fixed) - remove caveat on SMP lock with clang (fixed) Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2025-11-24 10:28:33 +11:00
Gerwin Klein	4b7c2a315f	configs: add zynqmp and rpi4 to verified platforms ... The AARCH64 config now also works for functional correctness on zcu102/zcu106 and rpi4. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-08 14:17:49 +10:00
Gerwin Klein	f52e102d5d	caveats: language tweaks for more clarity ... Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00
Gerwin Klein	0b4f14f8ae	caveats: more Intel caveats ... - missing MSI remapping feature - clarifications on timing/micro-architectural attacks - clarifications on Rowhammer Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00
Gerwin Klein	1aa42bec1d	caveats: improve vspace reuse; tweak multikernel ... - tweak SMP/multikernel text to make clear that SMP is not deprecated - rephrase old VSpace reuse section hopefully be clearer Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00
Gerwin Klein	5c1d58c17e	caveats: add MCS WCET and cache ops ... - MCS WCET settings are just defaults without much basis - stale page cap data also allows cache ops to proceed Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00
Gerwin Klein	f64c7b659d	caveats: add tested platforms for SMP combinations ... Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00
Gerwin Klein	54040e84b3	caveats: rework correctness, add SMP, more MCS ... - rework implementation correctness section, give more information, add roadmap items - expand MCS section, add roadmap - add SMP section + combinations Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00
Gerwin Klein	16003dfb6b	caveats: consolidate into a single md file ... Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>	2024-07-01 15:30:49 +10:00