aarch64,smc: Add tests for SMC cap behaviors

[kent-mcleod]

SMC caps are a new cap type for performing SMC calls on aarch64. These tests check that CNode operations behave as expected when manipulating capabilities of this type.

[Indanz]

How does this relate to #85?

[kent-mcleod]

How does this relate to https://github.com/seL4/sel4test/pull/85?

They could be merged. These test cases are for confirming cap operations for the smc cap do the right thing while #85 is checking actual functionality of the invocation.

[Indanz]

Could the same support be added to the IRQControl cap? That one can't be copied currently. It didn't seem that much effort to add proper CNode operation support to SMC. Or is there a fundamental difference between the two?

[kent-mcleod]

Could the same support be added to the IRQControl cap? That one can't be copied currently. It didn't seem that much effort to add proper CNode operation support to SMC. Or is there a fundamental difference between the two?

IRQControl caps don't have a defined meaning for are badge/guard value - it's used to create divisions in the derivation tree so that revoke knows what children belong to the parent cap. I think it would be hard to express that a copied IRQControl cap was allowed to revoke it's children, but not allowed to revoke sibling irqcontrol caps currently.

[kent-mcleod]

I've updated this for merging now.

[Indanz]

Did you test it with KernelAllowSMCCalls enabled? I don't think we have a HW test that enables it yet.

[kent-mcleod]

Yes, I tested it on an imx8mm-evk platform and the new tests run as expected. Although the existing SMC test that actually tries to perform an SMCCall fails on that platform. (I might check again running the tests with an EL2 kernel instead of EL1.)

[lsf37]

Could the same support be added to the IRQControl cap? That one can't be copied currently. It didn't seem that much effort to add proper CNode operation support to SMC. Or is there a fundamental difference between the two?

IRQControl caps don't have a defined meaning for are badge/guard value - it's used to create divisions in the derivation tree so that revoke knows what children belong to the parent cap. I think it would be hard to express that a copied IRQControl cap was allowed to revoke it's children, but not allowed to revoke sibling irqcontrol caps currently.

That would definitely be a major proof change, because the fact that there is only one IRQControl cap in the system is used by quite a few invariant proofs. Mostly for what Kent describes above, but also for a whole bunch of other small properties.

[lsf37]

Yes, I tested it on an imx8mm-evk platform and the new tests run as expected. Although the existing SMC test that actually tries to perform an SMCCall fails on that platform. (I might check again running the tests with an EL2 kernel instead of EL1.)

If you can give me a config where everything works as expected, I'll look into how to add that to the hw test run.

[Indanz]

Could the same support be added to the IRQControl cap? That one can't be copied currently. It didn't seem that much effort to add proper CNode operation support to SMC. Or is there a fundamental difference between the two?

IRQControl caps don't have a defined meaning for are badge/guard value - it's used to create divisions in the derivation tree so that revoke knows what children belong to the parent cap. I think it would be hard to express that a copied IRQControl cap was allowed to revoke it's children, but not allowed to revoke sibling irqcontrol caps currently.

How is the situation different than notifications? There that's solved by usingmdbFirstBadged.

Alternatively, revoke on IRQControl could only revoke IRQ handles and not IRQControl copies, which would still be much better than the current situation. Same for delete.

That would definitely be a major proof change, because the fact that there is only one IRQControl cap in the system is used by quite a few invariant proofs. Mostly for what Kent describes above, but also for a whole bunch of other small properties.

I don't see why the proofs would care whether there are multiple copies of IRQControl, the object is stateless. Currently there is zero or one IRQControl cap in the system.

Not being able to copy IRQControl very annoying because it means you need to create all possible IRQ handles and pass them on at startup. The root task can't safely delegate IRQControl, as it may be deleted by accident and then recovery is impossible. With SMP this is even worse, as you need to know which core the IRQ will arrive on at creation time, but the code that wants to choose where to handle IRQs may be loaded dynamically later.

[kent-mcleod]

Yes, I tested it on an imx8mm-evk platform and the new tests run as expected. Although the existing SMC test that actually tries to perform an SMCCall fails on that platform. (I might check again running the tests with an EL2 kernel instead of EL1.)

If you can give me a config where everything works as expected, I'll look into how to add that to the hw test run.

I wasn't able to find one where the original SMC0001 test passes. Including on zynqmp where the board in the machine_queue has ATF installed and running.

[Indanz]

I wasn't able to find one where the original SMC0001 test passes. Including on zynqmp where the board in the machine_queue has ATF installed and running.

Does it fail on line:

https://github.com/seL4/sel4test/blob/6fe5193ee8dfdb4aed6b9efc59ee9b81122f2460/apps/sel4test-tests/src/tests/smc.c#L60

Because looking back at #85, initialising x2 and x3 to 2 and 3 and testing it's still that was my suggestion, but it turned out not to be useful. However, the initialisation is still there. I think those x2 and x3 checks should be removed altogether.

[kent-mcleod]

Does it fail on line:

yes. As x2 and x3 are not clobbered but the earlier asserts pass.

[Indanz]

Does the rest of the test pass if you remove those two lines?

[kent-mcleod]

Yes

[kent-mcleod]

https://github.com/seL4/sel4test/pull/116