Hi seL4 Dev Team,
I'm currently working on (mostly learning at this point) how we could add TX1 platform support for a PCIE network card (Intel 82580), using TK1 and others as a reference. I'm fairly new to working with PCI, but after looking around I think I have a general idea on what I need to do. I would appreciate it very much if someone with more experience could tell me if I'm on the wrong path here:
* Using the TX1 TRM, I would populate the missing physical device region definitions in 'tx1/plat/machine/devices.h', and update the 'dev_p_regs[]' struct in 'tx1/plat/machine/hardware.h' * Figure out if I need to build up SMMU support (also a newbie here), I'm having doubts on whether I can bang on physical addresses or not without it * Construct a suitable implementation of 'ps_io_port_ops_t' for handling the I/O routines for libpci * Put together a hello world main program to exercise some of libpci's functionality * Once things are looking good there, move up to libethdrivers and port the needed bits for our Ethernet adapter using existing references (and eventually hooking up to lwip hopefully)
At this point, I've been avoiding camkes for the sake of learning how everything works and if anyone can recommend a good starting C project for doing I/O on an ARM platform, that would be very helpful.
Thanks in advance.
Hi Jon,
Sorry for the late response -- this email came in when the University was closing in on its end of year shutdown. Your steps look fairly good, but you will most likely also have to write mux, clock and other drivers for the TX1 -- or if the drivers are similar enough between the TK1 and TX1, you can probably reuse large portions of the existing TK1 drivers. I don't think you'll need SMMU support unless you plan to virtualize some hardware on your target system using passthrough. I'd need a better description of your target system to answer more authoritatively.
For `ps_io_ops_t` -- thankfully this is just a virtual memory mapping operation, so you shouldn't need to do anything since libsel4platsupport already provides the common backend implementation for it (see `__map_device_page`). You should be able to just call `sel4platsupport_new_io_ops()`.
Setting up a test environment for your drivers will be a bit of a challenge, but you can use seL4test to get you started (https://wiki.sel4.systems/Testing). What you would do is set up your own new, "fake" test app and call your driver routines from within that test app.
I'm not sure I can give you a good answer on a C project to look at because looking at C projects targeted at conventional monolithic and hybrid kernels may not be very helpful in understanding how to do the same thing on a microkernel.
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
Hi Kofi Doku,
Thank you for the thorough response, it was very helpful.
Happy New Year, Jon
On Mon, Jan 1, 2018 at 4:38 PM, Kofidoku.Atuah@data61.csiro.au wrote:
Hi Jon,
Sorry for the late response -- this email came in when the University was closing in on its end of year shutdown. Your steps look fairly good, but you will most likely also have to write mux, clock and other drivers for the TX1 -- or if the drivers are similar enough between the TK1 and TX1, you can probably reuse large portions of the existing TK1 drivers. I don't think you'll need SMMU support unless you plan to virtualize some hardware on your target system using passthrough. I'd need a better description of your target system to answer more authoritatively.
For `ps_io_ops_t` -- thankfully this is just a virtual memory mapping operation, so you shouldn't need to do anything since libsel4platsupport already provides the common backend implementation for it (see `__map_device_page`). You should be able to just call `sel4platsupport_new_io_ops()`.
Setting up a test environment for your drivers will be a bit of a challenge, but you can use seL4test to get you started ( https://wiki.sel4.systems/Testing). What you would do is set up your own new, "fake" test app and call your driver routines from within that test app.
I'm not sure I can give you a good answer on a C project to look at because looking at C projects targeted at conventional monolithic and hybrid kernels may not be very helpful in understanding how to do the same thing on a microkernel.
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
-
Jon Lamb -
Kofidoku.Atuah＠data61.csiro.au