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?

Xaphiosis · 2024-09-24T06:19:01Z

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

+
+postSetFlags :: PPtr TCB -> TcbFlags -> Kernel ()
+postSetFlags t flags =
+    when (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) (fpuRelease t)


interesting, with one flag I guess this is the shortest way to do it, but with more flags it'll be a bunch of tcbFlagToWords .|.'ed together?

Hmm, good question, I hadn't thought about what this will look like if/when there are more flags. Maybe it's worth adding some sort of flagSet helper function that does the tcbFlagToWord and .&.. That would make this something like

when (flagSet (ArchFlag FpuDisabled) flags) (fpuRelease t)

Something like that sounds good, but I'd prefer isFlagSet or something, otherwise it sounds like a flag-setter.

Maybe inFlagSet?

I like isFlagSet, to me it's more of an abstraction where we don't care how it's implemented while inFlagSet implies that it's a set.

hasFlag? I keep reading isFlagSet as "is this a flag set", not "is this flag set/unset".

Uhh, I really think that isFlagSet is pretty standard for "is the flag set", I'm not sure many people would think of isFlagASet when reading it, and I'm not even sure that's possible in Isabelle's type system, and isSetOfFlags is an even more creative interpretation... but then Englishes

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.

Xaphiosis · 2024-09-24T06:23:50Z

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

+data ArchTcbFlag = FpuDisabled
+
+archTcbFlagToWord :: ArchTcbFlag -> Word
+archTcbFlagToWord (FpuDisabled) = 0x1


No desire for bit-equivalent here?

Good point, I missed that. Thinking about it now though, the equivalent in C produces values with the final mask, so at some point we'll need to do the conversion between that and the bit form. Do we think that that's simple enough that it can be done wherever, or would it be better do it in Refine instead of CRefine?

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

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

Xaphiosis · 2024-09-24T06:49:28Z

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

@@ -70,6 +70,11 @@ atcbContextSet uc atcb = atcb { atcbContext = uc }
 atcbContextGet :: ArchTCB -> UserContext
 atcbContextGet = atcbContext

+data ArchTcbFlag = FpuDisabled


in some cases when we have datatypes that are boringly similar to what we have in ASpec, we don't translate them and instead introduce an alias in the skeleton files; not sure if that's useful here

I think that would make sense, also for any future flags. Not sure of there we have a good location to put these in for arch specific data types, but it's worth looking.

lsf37 · 2024-09-24T07:33:13Z

spec/abstract/AARCH64/FPU_A.thy

+\<comment> \<open>FIXME: maybe use a case instead of the if (depends on if wpc or if_split is easier)\<close>
+definition switch_local_fpu_owner :: "obj_ref option \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "switch_local_fpu_owner new_owner \<equiv> do
+     do_machine_op enableFpu;
+     cur_fpu_owner \<leftarrow> gets (arm_current_fpu_owner \<circ> arch_state);
+     when (cur_fpu_owner \<noteq> None) $ save_fpu_state (the cur_fpu_owner);


I would generally prefer case for option if you have both branches, because it allows you to avoid using the.

I'm just seeing that we don't really have both branches here. Don't we have a maybeM or similar combinator in the nondetmonad for running something only when the argument is Some? Don't quite remember.

That comment was actually for the if statement just after this when, which does have both branches. I'll have a dig around for a helpful combinator. Assuming one does exist, would we want something similar in the Haskell?

Yes, having them structurally the same would be nice. (It's not that super important, it's correct as it is, just a style question, so if we don't already have a combinator, we can also leave it as is.)

Context: the FIXME was originally because we weren't sure whether dealing with if or case would be easier in the corres proof, so the plan was to check and then remove the FIXME afterwards

I've made this change now but it's a little bit more complicated in Haskell, as to the best of my knowledge there isn't an easily accessible equivalent to maybeM. The most likely option that I found is https://hackage.haskell.org/package/extra-1.7.16/docs/Control-Monad-Extra.html#v:whenJust, but using that would introduce a new dependency on the extra package. I've currently used the underlying for from Data.Traversable, but that feels a bit unreadable and will require some care when translating to the design spec. Thoughts?

l4v/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs

Lines 33 to 41 in 285ecfc

switchLocalFpuOwner :: Maybe (PPtr TCB) -> Kernel ()

switchLocalFpuOwner newOwner = do

doMachineOp enableFpu

curFpuOwner <- gets (armKSCurFPUOwner . ksArchState)

for curFpuOwner saveFpuState

case newOwner of

Nothing -> doMachineOp disableFpu

Just tcbPtr -> loadFpuState tcbPtr

modifyArchState (\s -> s { armKSCurFPUOwner = newOwner })

I don't have a good solution here. There's a function maybe in Data.Maybe that we could use with maybe (return ()) saveFpuState curFpuOwner that we could make an alias for to remove the return () part, but then the return values have to match so it would only work for unit returns. Otherwise you could return undefined with the correct type (whatever 'b the function returns). How does for get through the Haskell translator? I don't think we have something like that in Isabelle.

Yeah, for won't get through the translator without doing something manual, so on second thought probably shouldn't use it.

I think I'm ok with your maybe idea, particularly since now that I look at it, that's basically how whenJust is implemented. It lines up pretty well with maybeM as well, which requires a unit return.

Context: the FIXME was originally because we weren't sure whether dealing with if or case would be easier in the corres proof, so the plan was to check and then remove the FIXME afterwards

Good point, and also works as a reminder that there's two things going on here. There's switching the when to a maybeM which I think we all agree is nice to avoid the, and there's whether it should if or case, where case is again nice in that it avoids the but it is unknown which will be easier in the proofs. How about for now I switch it to case but leave the FIXME until we get to the proofs?

yes, I'd be happy with that

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.

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 <corey.lewis@proofcraft.systems>

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

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.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

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

Xaphiosis reviewed Sep 24, 2024

View reviewed changes

spec/haskell/src/SEL4/Object/TCB/AARCH64.hs Show resolved Hide resolved

Xaphiosis reviewed Sep 24, 2024

View reviewed changes

spec/haskell/src/SEL4/Model/StateData/AARCH64.hs Show resolved Hide resolved

corlewis force-pushed the fpu_context_switching branch from 1dbb4fc to bfd342f Compare September 24, 2024 06:31

Xaphiosis reviewed Sep 24, 2024

View reviewed changes

spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs Show resolved Hide resolved

Xaphiosis reviewed Sep 24, 2024

View reviewed changes

lsf37 added the seL4-PR requires merging a corresponding seL4 pull request label Sep 24, 2024

lsf37 reviewed Sep 24, 2024

View reviewed changes

spec/abstract/AARCH64/FPU_A.thy Outdated Show resolved Hide resolved

lsf37 reviewed Sep 24, 2024

View reviewed changes

spec/abstract/AARCH64/FPU_A.thy Outdated Show resolved Hide resolved

lsf37 reviewed Sep 24, 2024

View reviewed changes

spec/abstract/Schedule_A.thy Outdated Show resolved Hide resolved

lsf37 reviewed Sep 24, 2024

View reviewed changes

lsf37 approved these changes Sep 24, 2024

View reviewed changes

corlewis force-pushed the fpu_context_switching branch 2 times, most recently from 3aaac5d to 285ecfc Compare September 26, 2024 03:27

corlewis changed the base branch from master to explicit_fpu September 26, 2024 04:32

corlewis force-pushed the fpu_context_switching branch 3 times, most recently from 7a5943d to f1fb45c Compare September 27, 2024 01:02

corlewis added 2 commits September 27, 2024 20:40

aarch64 haskell+design: update exec spec to use semi-lazy FPU switching

b7f740d

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

corlewis force-pushed the fpu_context_switching branch from f1fb45c to 31b2feb Compare September 27, 2024 10:41

corlewis changed the title ~~aarch64: update specs to use semi-lazy FPU switching~~ Update specs to use semi-lazy FPU switching Sep 27, 2024

corlewis added 3 commits September 27, 2024 21:39

x64 spec: update specifications for semi-lazy FPU changes

04816a1

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

haskell-translator: convert unit types in type aliases

eee9aa4

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

arm+arm-hyp+riscv64 spec: update other arches for semi-lazy FPU changes

c45b235

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

corlewis force-pushed the fpu_context_switching branch from 31b2feb to c45b235 Compare September 27, 2024 11:39

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update specs to use semi-lazy FPU switching #819

Update specs to use semi-lazy FPU switching #819

corlewis commented Sep 24, 2024 •

edited

Loading

Xaphiosis Sep 24, 2024

Xaphiosis Sep 24, 2024

corlewis Sep 24, 2024 •

edited

Loading

Xaphiosis Sep 24, 2024

lsf37 Sep 24, 2024

corlewis Sep 24, 2024

lsf37 Sep 24, 2024

Xaphiosis Sep 26, 2024 •

edited

Loading

Xaphiosis Sep 24, 2024

corlewis Sep 24, 2024

Xaphiosis Sep 24, 2024

corlewis Sep 24, 2024

Xaphiosis Sep 24, 2024

lsf37 Sep 24, 2024

lsf37 Sep 24, 2024

lsf37 Sep 24, 2024

corlewis Sep 24, 2024

lsf37 Sep 24, 2024

Xaphiosis Sep 26, 2024

corlewis Sep 26, 2024

Xaphiosis Sep 26, 2024

corlewis Sep 26, 2024

corlewis Sep 26, 2024

lsf37 Sep 27, 2024

lsf37 Sep 24, 2024

Xaphiosis Sep 24, 2024

corlewis Sep 24, 2024

Xaphiosis Sep 26, 2024

lsf37 left a comment

corlewis commented Sep 27, 2024

lsf37 commented Sep 27, 2024

	switchLocalFpuOwner :: Maybe (PPtr TCB) -> Kernel ()
	switchLocalFpuOwner newOwner = do
	doMachineOp enableFpu
	curFpuOwner <- gets (armKSCurFPUOwner . ksArchState)
	for curFpuOwner saveFpuState
	case newOwner of
	Nothing -> doMachineOp disableFpu
	Just tcbPtr -> loadFpuState tcbPtr
	modifyArchState (\s -> s { armKSCurFPUOwner = newOwner })

Update specs to use semi-lazy FPU switching #819

Are you sure you want to change the base?

Update specs to use semi-lazy FPU switching #819

Conversation

corlewis commented Sep 24, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

corlewis Sep 24, 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

Xaphiosis Sep 26, 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

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

lsf37 left a comment

Choose a reason for hiding this comment

corlewis commented Sep 27, 2024

lsf37 commented Sep 27, 2024

corlewis commented Sep 24, 2024 •

edited

Loading

corlewis Sep 24, 2024 •

edited

Loading

Xaphiosis Sep 26, 2024 •

edited

Loading