Hey Michal,
(1) The IBM-PC compatible build of the kernel currently uses the serial via the IO port interface. To use the VGA buffer, you'd have to
do the work of getting the VGA alphanumeric-mode buffer mapped in at boot, and then write the code to print to the buffer.
(1a) I'd recommend doing this in userspace as part of your root task though, since there's no real advantage (that I can glean) to adding
a VGA framebuffer driver to the kernel, unless you have no machines with serial ports, which is probably why you're trying to do this, I'd guess.
(2) Serializing access to hardware between the kernel and other entities is a difficult problem if you also need to preserve trustworthiness
proprerties of the kernel. If you use a shared lock between the kernel and userspace for example, you open up a very obvious DoS attack against the kernel.
(3) It is possible, but you'd have to do a the plumbing yourself, yes. Consider doing this in your root task or as part of your userspace
environment on top of seL4.
(4) It looks like you'd have to implement both putConsoleChar and putDebugChar, although they do exactly the same thing
(5) Yes, the VGA function is exposed at the same address on all IBM-PC compatibles, no worries
--Hope I helped,
--
Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO