Fixed url below. On Sat, Jan 11, 2020 at 3:41 PM Harry Butterworth <heb1...@gmail.com> wrote:
> Take a look at Andy’s Binary Editor nyangau.org/be/be.htm > <http://nyangau.org/be/be.html> 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 > > On Fri, Jan 10, 2020 at 8:21 PM abdi mahmud haji < > abdimahmudhaji...@gmail.com> wrote: > >> 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 >> >
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
