Update specs to use semi-lazy FPU switching #819

corlewis · 2024-09-24T05:36:58Z

These are the preliminary spec changes to seL4 to implement RFC-18. They include extending the machine interface with new ops, adding the current owner of the FPU state to the kernel state, and adding the new seL4_TCB_Set_Flags syscall and related functions.

Xaphiosis · 2024-09-24T05:52:35Z

spec/machine/AARCH64/MachineOps.thy

+   od"
+
+definition enableFpu :: "unit machine_monad" where
+  "enableFpu \<equiv> modify (\<lambda>s. s\<lparr>fpu_enabled := True \<rparr>)"


Left over from internal review:

@Xaphiosis

the (lack of) link between enableFpu and enableFpuEL01 confuses me... there's no machine op for disabling the FPU? Are enableFpu and enableFpuEL01 called separately by the C, or is this only the abstract spec model?

@corlewis

I was confused also. In the C, enableFpu calls either disableTrapFpu or enableFpuEL01, depending on whether it is a configuration with hypervisor support (see https://github.com/seL4/seL4/blob/85aa104eb4d527bc9f0aac28f3e9c3a84eed1d7a/include/arch/arm/arch/64/mode/machine/fpu.h#L127). I was originally going to just have enableFpu in the spec before realising that enableFpuEL01 is called directly from vcpu_disable (https://github.com/seL4/seL4/blob/85aa104eb4d527bc9f0aac28f3e9c3a84eed1d7a/include/arch/arm/armv/armv8-a/64/armv/vcpu.h#L702)

@Xaphiosis

That seems odd, because it is unconditionally enabling FPU for native threads with no VCPU on hyp configurations. Doesn't that effectively ignore the native thread's configured flags?

To answer this earlier question, our confusion was due to the fact that on AArch64 with hypervisor support there are two registers that control whether the FPU is enabled. The first, CPACR_EL1, is generally controlled by the VM and is used to enable or disable the FPU for virtualised threads. This register is the one being enabled by enableFpuEL01, which seL4 only calls when disabling the VCPU. For native threads seL4 instead uses CPTR_EL2, which it modifies with enableFpu and disableFpu.

spec/haskell/src/SEL4/Object/TCB/AARCH64.hs

Xaphiosis · 2024-09-24T06:22:22Z

spec/haskell/src/SEL4/Object/Structures.lhs

+> type TcbFlags = Word
+
+> data TcbFlag
+>     = NoFlag


I'm still not sure I understand the purpose of NoFlag, could you enlighten me?

I can't speak about the original intentions in the C, but in my mind here it provides a way to abstract away the details of how the flags are implemented. For instance, we could say flags = NoFlag to say that no flags are set.

Having now said that, this is another argument for adding something like the flagSet helper function I mentioned in a different comment, since that would extend this abstraction and hide the details of the flags being implemented as a Word.

spec/haskell/src/SEL4/Object/Structures/AARCH64.hs

spec/haskell/src/SEL4/Model/StateData/AARCH64.hs

spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs

spec/haskell/src/SEL4/Object/Structures/AARCH64.hs

spec/abstract/AARCH64/FPU_A.thy

spec/abstract/Schedule_A.thy

lsf37 · 2024-09-24T07:45:06Z

spec/machine/AARCH64/MachineOps.thy

 definition isFpuEnable :: "bool machine_monad" where
-  "isFpuEnable \<equiv> return True"
+  "isFpuEnable \<equiv> gets fpu_enabled"


Does anyone remember why this is called isFpuEnable in C and not isFpuEnabled?

Probably Englishes

Yeah, no idea beyond that. Should we give it the better name here?

If you want to, but then it would be good to also rename it in C.

lsf37

Nice work! I only had cosmetic comments.

We should probably target this to a new branch to use until the proofs are done and the entire thing can be merged into master.

corlewis · 2024-09-27T10:47:51Z

This PR has now been updated with a commit making equivalent changes to the FPU handling code in the x64 specification, and a commit making the required changes to the architectures that are not configured to have FPUs enabled so that they can still be built.

lsf37 · 2024-09-27T12:34:12Z

This PR has now been updated with a commit making equivalent changes to the FPU handling code in the x64 specification, and a commit making the required changes to the architectures that are not configured to have FPUs enabled so that they can still be built.

Good to see all tests passing up to AInvs. Nice work!

corlewis · 2024-12-17T23:53:04Z

This has been rebased and had a few additional changes included following the earlier discussions.

Xaphiosis

I think we're mostly ok, one or two comment chains did not resolve.

On the commits, why is "x64 spec: update specifications for semi-lazy FPU changes" not merged in with the others? It's a bit confusing, there's AARCH64 work split up across spec levels, then x64 not split up, and then everything else.

Also, subjective suggestion: there's no need to start commit comments with "This ", i.e. can say "Includes" instead of "This includes". Maybe we can also teach this novel idea to others :)

corlewis · 2024-12-18T06:18:29Z

On the commits, why is "x64 spec: update specifications for semi-lazy FPU changes" not merged in with the others? It's a bit confusing, there's AARCH64 work split up across spec levels, then x64 not split up, and then everything else.

The X64 changes were kept separate because it has FPU enabled, the other architectures don't and their changes are mostly trivial to match the modified interface.

I think the commit structure was just due to the way in which this work was developed; first for AArch64, which included changes to generic files, then copying required arch-specific changes to X64, and then doing required arch-specific changes for other architectures that don't support FPU.

I have no strong preference here and see two obvious options, would you prefer something like the current structure but with the two AArch64 commits combined, or to make it all one big commit for all architectures?

Xaphiosis · 2024-12-18T06:29:53Z

On the commits, why is "x64 spec: update specifications for semi-lazy FPU changes" not merged in with the others? It's a bit confusing, there's AARCH64 work split up across spec levels, then x64 not split up, and then everything else.

The X64 changes were kept separate because it has FPU enabled, the other architectures don't and their changes are mostly trivial to match the modified interface.

I think the commit structure was just due to the way in which this work was developed; first for AArch64, which included changes to generic files, then copying required arch-specific changes to X64, and then doing required arch-specific changes for other architectures that don't support FPU.

I have no strong preference here and see two obvious options, would you prefer something like the current structure but with the two AArch64 commits combined, or to make it all one big commit for all architectures?

The question is whether you believe there is beneficial information in the extra commits. In my mind the aarch64+x64 are together because of FPU, and then the rest are not very interesting probably. Since it's all reviewed now, probably can squash them together, add a note in the commit message.

corlewis · 2024-12-18T07:47:58Z

The question is whether you believe there is beneficial information in the extra commits. In my mind the aarch64+x64 are together because of FPU, and then the rest are not very interesting probably. Since it's all reviewed now, probably can squash them together, add a note in the commit message.

I think there's a little bit of use in keeping aarch64 and x64 separate from the less interesting architectures, so I've now squashed things into two commits. Have a look and let me know what you think

spec/design/skel/Structs_B.thy

Xaphiosis · 2024-12-18T19:48:23Z

spec/design/skel/Structs_B.thy

+arch_requalify_consts (H)
+  archTcbFlagToWord
+
+#INCLUDE_SETTINGS keep_constructor = tcb_flag


Do you happen to know why we tell it to keep constructors for tcb_flag when we're importing TcbFlag? Does a tcb_flag actually exist anywhere? It doesn't seem the most easily graspable interface, I'm glad you managed to figure it out.

Another case of the translator being magic; TcbFlag is quietly translated to tcb_flag.

spec/haskell/src/SEL4/Object/Structures.lhs

Xaphiosis · 2024-12-18T19:57:28Z

The question is whether you believe there is beneficial information in the extra commits. In my mind the aarch64+x64 are together because of FPU, and then the rest are not very interesting probably. Since it's all reviewed now, probably can squash them together, add a note in the commit message.

I think there's a little bit of use in keeping aarch64 and x64 separate from the less interesting architectures, so I've now squashed things into two commits. Have a look and let me know what you think

Commits make sense now, modulo squashes. I had one last bikeshed about comments and noFlag, but otherwise this is good to go from my side.

Xaphiosis · 2024-12-19T00:14:25Z

All done now from my side.

This includes extending the machine interface with new ops, adding the current owner of the FPU state to the kernel state, and adding the new seL4_TCB_Set_Flags syscall and related functions. Signed-off-by: Corey Lewis <[email protected]>

Signed-off-by: Corey Lewis <[email protected]>

These architectures do not have FPU enabled and so just need minor updates to match the changed interface. Signed-off-by: Corey Lewis <[email protected]>

corlewis requested review from Xaphiosis and lsf37 September 24, 2024 05:36

corlewis force-pushed the fpu_context_switching branch from de54aec to 1dbb4fc Compare September 24, 2024 05:42