search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Added XSD and a validation script #77

Open podhrmic opened 8 months ago

podhrmic commented 8 months ago

Partially resolves https://github.com/seL4/microkit/issues/70

TL;DR; I added an XSD schema for validating the system XMLs. You are currently using numbers with underscores, such as period="100_000" which is not a valid XML number. I parse these as strings, which is fine as long as you trust your build tool to resolve these correctly.

The long story I asked ChatGPT to generate XSD schema from the few Microkit examples that are out there, and it did pretty well. I manually edited the XSD in a few places, and it certainly can be improved further, but IMHO it is good enough as it is. I recommend validating all .system files in a CI.

Ivan-Velickovic commented 7 months ago

Thanks for doing this @podhrmic. I'm not familiar with XSD, do you know if there's more sanitisation we can do, such as a minimum and maximum value for the period/budget for example?

For #70 I was hoping for some kind of specification that would be the input for the Microkit tool as well as any other tools that generate or consume the system description. One thing to consider is that with this XSD file, there is a possibility for the tool to be out-of-sync with the XSD or vice-versa. Something to look into would be whether we can consume the XSD file in Microkit to avoid that, or do you know of anything else in the XML space that would achieve this?

Ivan-Velickovic commented 7 months ago

And sorry for taking so long to review the PR.

podhrmic commented 7 months ago

No worries, I figured you were busy!

You can certainly set min/max for any integer attribute, similar to what I have done for the priority values here. It just requires the budget etc. to be treated as integers, not strings (see my initial comment).

You can certainly generate datatypes from XSD, (xmlschema, xsdata, xml-schema, xgen, ... ). Perhaps a good start is to explicitly write the requirements for the .system format, implement them in XSD and then use the XSD to generate code for Microkit tools.

If this is interesting to you, I can look into it further!