AARCH64 MCS Specs by michaelmcinerney · Pull Request #1016 · seL4/l4v

michaelmcinerney · 2026-06-10T08:19:44Z

Introduce the theory file Time and collect many definitions, lemmas,
and axiomatizations related to time in the MCS kernel that were
previously in separate architecture-dependent files.

Update for AARCH64 MCS.

Test with seL4/seL4@michaelm/ipc_queues_mcs_testing

Introduce the theory file Time and collect many definitions, lemmas, and axiomatizations related to time in the MCS kernel that were previously in separate architecture-dependent files. Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

michaelmcinerney · 2026-06-10T08:22:29Z

Force pushed to rebase and fix typo in commit message.

michaelmcinerney · 2026-06-10T08:23:02Z

And I suppose we'll want to turn on testing for AARCH64 ASpec and Haskell, but I'm not sure how to do that.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

michaelmcinerney · 2026-06-10T11:05:31Z

I did try testing the ASpec for AARCH64 with a couple of the commits I pushed, but it didn't work. I'm really not sure how to test HaskellKernel. It doesn't seem to be covered in run_tests.

lsf37 · 2026-06-10T23:10:44Z

I did try testing the ASpec for AARCH64 with a couple of the commits I pushed, but it didn't work. I'm really not sure how to test HaskellKernel. It doesn't seem to be covered in run_tests.

Will have a look later today on Haskell (it's definitely covered, the question is how to switch on only ASpec/ExecSpec/Haskell for now). The test matrix unfortunately needs to be changed on the master branch, because GitHub is great.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

lsf37 · 2026-06-12T04:41:13Z

 theory ArchCSpace_A
-imports
-  ArchVSpace_A
+imports ArchVSpace_A


The correct style according to the style guide theory is

theory ArchCSpace_Atheory ArchCSpace_A imports ArchVSpace_A begin

(or on the same line if it's just one, but still indented)

Given that there are no other changes in this file, I would remove the change entirely, though.

lsf37 · 2026-06-12T04:42:14Z

-          od
-        | _ \<Rightarrow> return ()
+     ct \<leftarrow> gets cur_thread;
+     ct_schdble \<leftarrow> gets (schedulable ct);


Suggested change

ct_schdble \<leftarrow> gets (schedulable ct);

ct_schedulable \<leftarrow> gets (schedulable ct);

lsf37 · 2026-06-12T04:46:31Z

+definition idle_sc_ptr :: vspace_ref where
+  "idle_sc_ptr = pptr_base + 0x3000"


We should probably repeat the comment from idle_thread_ptr above here, even if we didn't do that on the other architectures.

lsf37 · 2026-06-12T05:07:44Z

+definition usToTicks :: "word64 \<Rightarrow> word64" where
+  "usToTicks \<equiv> us_to_ticks"


Should we make this one an (input) abbreviation? (bit like maxIRQ)

Yeah that sounds good

lsf37 · 2026-06-12T05:10:01Z

+definition ticksToUs :: "word64 \<Rightarrow> word64" where
+  "ticksToUs \<equiv> ticks_to_us"
+
+definition maxUsToTicks :: "word64" where
+  "maxUsToTicks \<equiv> max_us_to_ticks"
+
+definition maxTicksToUs :: "word64" where
+  "maxTicksToUs \<equiv> max_ticks_to_us"
+
+definition kernelWCETTicks :: "word64" where
+  "kernelWCETTicks \<equiv> kernelWCET_ticks"
+
+definition kernelWCETUs :: "word64" where
+  "kernelWCETUs \<equiv> kernelWCET_us"
+
+definition maxPeriodUs :: "word64" where
+  "maxPeriodUs \<equiv> MAX_PERIOD_US"


same here, if we make these input abbreviations, we don't have to carry around simplification rules that they are equal, and we still don't need to make any unidiomatic changes to the Haskell code.

This would need an update for RISCV64 and ARM to do the same, but it's easier to do this now than later when we have more architectures.

lsf37 · 2026-06-12T05:11:43Z

-                vgicUpdateLR vcpuPtr irq_idx virqen
-                )
+    curThread <- getCurThread
+    isschedulable <- getSchedulable curThread


either

Suggested change

isschedulable <- getSchedulable curThread

isSchedulable <- getSchedulable curThread

or if that name is taken, then

is_schedulable <- getSchedulable curThread

lsf37 · 2026-06-12T05:12:13Z

-            when runnable $ handleFault curThread $ ArchFault $ VPPIEvent irq
-        _ -> return ()
+    curThread <- getCurThread
+    isschedulable <- getSchedulable curThread


(same name change as above)

lsf37 · 2026-06-12T05:14:25Z

+  Word_Lib.WordSetup
+  Kernel_Config \<comment> \<open>currently unnecessary, but added in anticipation of future use\<close>


Suggested change

Word_Lib.WordSetup

Kernel_Config \<comment> \<open>currently unnecessary, but added in anticipation of future use\<close>

Kernel_Config \<comment> \<open>currently unnecessary, but added in anticipation of future use\<close>

(Kernel_Config already imports Word_Lib.WordSetup)

lsf37 · 2026-06-12T05:18:23Z

-  "handleHypervisorEvent_C = (CALL schedule();; CALL activateThread())"
+  "handleHypervisorEvent_C =
+     (CALL updateTimestamp();;
+      \<acute>ret__unsigned_long :== CALL checkBudgetRestart();;
+      CALL schedule();;
+      CALL activateThread())"


This should really be a separate PR for just RISCV64 -- it's a fix for us forgetting to properly update the ADT on the C side to model hypervisor event entries. On RISCV64, we might be able to show that this is never called, but I think it's nicer to keep the proof of this function working for whenever RISCV64 gets hyp extensions.

That would include the generic change to hypervisor fault function in ASpec and Haskell. Maybe not necessarily a separate PR, but definitely a separate commit. It's not really anything to do with AARCH64, apart from the fact that we noticed it while doing the AARCH64 specs.

This was the part I mentioned before, where I said I wasn’t sure about the changes. This does work, but my thoughts were that we would prefer to say that we just don’t receive this type of event. This is saying that we do, and that the specific code for this specific event is a noop, and then we just wrap it in the surrounding code. When RISCV does get hyp extensions then I think we’d get rid of this custom definition and use the definition from the CParser instead. But I could be wrong.

Right, this is only correct, because handle_hypervisor_fault does nothing on RISCV, and we can't add the C version of that there, because that doesn't exist in RISCV64.

Arguing that the event doesn't occur is not so easy, it'd either be an assumption on do_user_op, or some kind of operation in the automaton that disallows it and that makes the automaton more awkward and arch specific (which we'd want to avoid for multikernel for instance). Given that the kernel entry/exit protocol is generic for this event in the specs, I would still go with what you have now, even if it is a somewhat large no-op. You're right that on AARCH64 (or when RISCV gets hyp extensions), this will be mostly handleVCPUFault_proc instead.

Alright great. Thanks for clarifying that.

lsf37 · 2026-06-12T05:19:19Z

                      elim: st_tcb_ex_cap'' pred_tcb'_weakenE)
+    apply (rule updateTimeStamp_checkBudgetRestart_helper)


This one I'm not sure which PR it belongs to. If it's related to the hypervisor event change, then in that separate PR.

lsf37 · 2026-06-12T05:24:27Z

-   apply (clarsimp simp: ct_in_state_def schact_is_rct_def valid_sched_def ct_not_in_q_def
-                         pred_tcb_at_def obj_at_def)
-
  (* Interrupt *)


This removal looks strange, why was the case there before and is now gone in a generic file? Indentation of the previous cases is likely wrong now if these lines can be just removed.

I think this case is now handled by the method handle_event_valid_sched_fault just before it, because it's shape is now the same as the other events.

ah, that makes a lot of sense. I did not think it would be able to. In that case the indentation is likely still correct.

lsf37 · 2026-06-12T05:25:18Z

-    apply (erule invs_sym_refs)
-   apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def)
-  apply fastforce
+  apply (wpsimp wp: check_budget_restart_if_lift


Is this still the handle_hypervisor_fault case? If yes, we should not remove the comment.

lsf37

Cool, other than teasing apart the generic code change that affects RISCV64 from the AARCH64 update, I think this is pretty good. I double-checked against a search on CONFIG_KERNEL_MCS and I can't find anything else that even looks arch specific. Which is a good sign.

Main query that might cost some work now, but reduce work later is whether we should make some definitions in ExecSpec input abbreviations instead. That'll save a few trivial equality lemmas and remove annoyances about having stated some property with the constant from the wrong spec level.

michaelmcinerney requested review from Xaphiosis, corlewis and lsf37 June 10, 2026 08:19

michaelmcinerney self-assigned this Jun 10, 2026

michaelmcinerney added the MCS related to `rt` branch and mixed-criticality systems label Jun 10, 2026

michaelmcinerney force-pushed the michaelm-aarch64_mcs_specs branch from b74e2e2 to 82bef93 Compare June 10, 2026 08:21

michaelmcinerney added 2 commits June 10, 2026 17:51

rt aspec+design+haskell+haskell-translator: update for AARCH64 MCS

cb65bd7

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

michaelmcinerney force-pushed the michaelm-aarch64_mcs_specs branch from 82bef93 to cb65bd7 Compare June 10, 2026 08:22

Fix AInvs squash

7fe943e

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

michaelmcinerney added 2 commits June 11, 2026 14:49

rt run_tests: turn on testing for ASpec for AARCH64

8708603

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

fix errors, squash

7ef2ce6

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

lsf37 force-pushed the michaelm-aarch64_mcs_specs branch from 67a140b to 7ef2ce6 Compare June 11, 2026 04:49

lsf37 reviewed Jun 12, 2026

View reviewed changes

lsf37 approved these changes Jun 12, 2026

View reviewed changes

	ct_schdble \<leftarrow> gets (schedulable ct);
	ct_schedulable \<leftarrow> gets (schedulable ct);

		definition idle_sc_ptr :: vspace_ref where
		"idle_sc_ptr = pptr_base + 0x3000"

		definition usToTicks :: "word64 \<Rightarrow> word64" where
		"usToTicks \<equiv> us_to_ticks"

	isschedulable <- getSchedulable curThread
	isSchedulable <- getSchedulable curThread

		Word_Lib.WordSetup
		Kernel_Config \<comment> \<open>currently unnecessary, but added in anticipation of future use\<close>

		elim: st_tcb_ex_cap'' pred_tcb'_weakenE)
		apply (rule updateTimeStamp_checkBudgetRestart_helper)

Conversation

michaelmcinerney commented Jun 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michaelmcinerney commented Jun 10, 2026

Uh oh!

michaelmcinerney commented Jun 10, 2026

Uh oh!

michaelmcinerney commented Jun 10, 2026

Uh oh!

lsf37 commented Jun 10, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lsf37 Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lsf37 Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lsf37 left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

michaelmcinerney commented Jun 10, 2026 •

edited

Loading

lsf37 Jun 12, 2026 •

edited

Loading

lsf37 Jun 12, 2026 •

edited

Loading