canarysnort01
commented
2 years ago While today there may only be a couple examples of complex conditional expressions, if the IDL were to be expanded in the future to define constants, enums, structs, and bitfields/typed unions, there would be many more examples of complex expressions, referencing not only configuration values but also constant and enum values.
So, I agree there should be a good way to encode expressions in the IDL.
As to how to encode them, I think there is a tension here between the cost of maintaining the XML file and the cost of generating a language binding from it.
Some additional questions I have along these lines:
-
Would maintaining the IDL become too cumbersome if expressions were encoded as proposed?
-
Is there an existing expression language that would be sufficient for current and future purposes that is both maintainable by a human as a simple expression string in the XML file and easily parsed and evaluated in many programming languages with widely available libraries?
As an aside, I think the root cause of this complexity is that the interface between the seL4 kernel and userland is so highly configuration dependent. This snowballs and deeply affects everything in libsel4, including which constants or enums are defined and what their values are, the layout and fields in structs/bitfields/unions, and which interfaces exist and what their methods are.
Because of all this complexity, the seL4 IDL XML file is really more of an IDL blueprint that must be evaluated against an seL4 configuration to generate the actual IDL.
I question whether this complexity is necessary and am curious how feasible or expensive simplifying it would be, but I'll leave that for a different discussion.
lsf37
ratmice
kent-mcleod
Before I jump too far down the rabbit hole on this, I wanted to sync with the community, It was mentioned during one of the developer meetings that the xml currently contains some c-isms in the form of c-preprocessor declarations,
Most of these are fairly simple, an example of the most complex being:
in sel4_arch_include/aarch64/interfaces/sel4arch.xml
If it weren't for these couple of complex conditions we could use something simple like:
condition_var="CONFIG_..." condition_defined=true|falseI tried to come up with a schema to cope with these definitions in a language neutral fashion:
Examples
Schema
The schema for the above xml uses an xsd (below), while the current encoding is using a dtd
As far as I can tell trying to do this with just a dtd leads to a much more verbose xml encoding.
Questions
CONFIG_contents of thevarattribute?checklist
condition=attributes toconditionelements in the sel4 xml.#ifconditions.