Take a look at Andy’s Binary Editor
nyangau.org/be/be.htm and implement an open source equivalent as an integrated debugger for seL4.
You will need to be able to get keyboard input, write characters to the screen and get access to files containing the structure definitions. You can provide the structure definitions at boot time.
You won’t need an OS or POSIX or even much of a standard library; the implementation just requires the language runtime, a parser, a few data structures, and a bit of printf-like code. You could write it all and make it completely self-contained which would allow you to keep the footprint really small.
Steps to proceed are as follows:
1) Pick a language. I’d probably pick C++ for this but you might also consider D or Rust or maybe COGENT.
2) Work out how to write a small test program in your chosen language and get seL4 to run it. This will require an implementation of the runtime for the language. If this hasn’t been done already for the language you pick, you can implement bits of the runtime as you go along when they are needed. If you fail at this step, go back to step 1, pick a different language.
3) Work out how to get your test program to write characters to the screen (or serial console perhaps).
4) Work out how to get keyboard input.
5) Define the grammar for the structure definitions. If you happen to pick COGENT you might look at DARGENT.
6) Understand the Model View Controller design pattern.
7) Write a parser to parse the structure definitions to create a model. You’ll want the model to use lazy evaluation so the whole system defined by the structure definitions can be represented but there is only overhead for the bits that are being actively browsed.
8) Implement a view for the model which displays a selected part on the console.
9) Implement a controller for the view and model which is an event loop that handles keyboard input and manipulates the model and view accordingly.
After getting your new debugger to work for browsing the entire system including the kernel data structures, find a way to integrate it which allows it to be configured to run with only the capability it needs for the debugging you want to do. After that you could make sure it can be used for debugging real time applications with a guarantee not to interfere with their real time operation.
For bonus points, if you have picked COGENT, you might finish off with a formal proof that your debugger displays the correct characters on the console according to the structure definitions, contents of memory and history of keyboard input. This (in fact the whole task) would be complicated by the fact that the memory contents change all the time underneath you as you browse a live system so you’d have to work out how to incorporate that and still prove something useful.
Enjoy
hey guys
I'm abdurahman and i have same question for you
i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel