l4-hackers

l4-hackers@os.inf.tu-dresden.de

2827 discussions

Can't access memory region
by Jason Philip 03 Feb '11

03 Feb '11

I need to have access to the VGA port and register. The register I need access in the range of 0x300 to 0x400 so I try getting a 1KB page from 300 onward, but it do not work. I suspect it do not work because it is I/O FPage and they have to align to (in this case 1kB) address. Could anyone help me access these port?

2 5

Questions on implementation details of capabilities
by Christoph Szeppek 03 Feb '11

03 Feb '11

Hello! I try to understand how capabilities are enforced by the Fiasco.OC kernel. From what I think I understood, capabilities are created in the kernel space area of an address space (which is the same in every address space) at Config::Caps_start. Each cap is identified by an index in this area and holds a reference to an object of type kobject_iface in its _obj attribute. This is the object this cap is controlling access to. Now I've got a few questions about further details. Where does the translation from address space local to kernel global cap id happen? How does the kernel know threads of which space are allowed to access which cap (mapdb?)? When a thread sends IPC, in which place of the kernel code do these caps get enforced / checked? BR, Christoph

2 1

Fiasco.OC internals
by Amadeo Cuadrado 03 Feb '11

03 Feb '11

Hello, My apologies if this question has been asked before in this list. What would be the most accurate doc that explains in detail the design and implementation of Fiasco.OC internals? Thanks in advance. Amadeo

2 1

Public release of seL4
by Gernot Heiser 02 Feb '11

02 Feb '11

NICTA and Open Kernel Labs have jointly released seL4. For those not aware of seL4, it is an L4 microkernel which is formally verified (meaning that the implementation is mathematically proven to conform to the specification). It is the world's first (and only) OS kernel that is formally verified in this strict sense. The public release includes the formal specification of the kernel (ARM version), kernel binaries for x86 and ARM, and a para-virtualized Linux running on top of seL4/x86. More about seL4: http://ertos.nicta.com.au/research/sel4/ NICTA download site: http://ertos.nicta.com.au/software/seL4/home.pyl Gernot

1 0

Fiasco Kernel extended V2 API vs. Pistachio X2 API
by Daniel Waddington - SISA 27 Jan '11

27 Jan '11

Hi, Can someone briefly explain the basic differences between the current Fiasco kernel API and the Pistachio X2 API? Thanks Daniel Waddington

3 2

I cannot for the life of me compile l4linux
by Daniel F. Haaland 27 Jan '11

27 Jan '11

l4re and fiasco seem to be working just fine (tested by running the hello world in qemu), but trying to add l4linux on top of l4re has caused me a lot of grief and the following error message: Getting required compilation flags failed. L4OBJ: /home/drxl/l4stuff/builddirs/L4Re-R27MP L4_REQUIRED_MODS: stdlibs log l4re_c-util libio shmc /home/drxl/l4stuff/src/l4linux/arch/l4/Makefile:301: *** Aborting.. Stop. make: *** [sub-make] Error 2 zsh: exit 2 make O=$MY_L4LINUX_OBJDIR I've detailed how I got to that point in painstaking detail here: http://blog.fairchild.dk/notes/2011/01/25/getting-l4linux-up-and-running/ In short I've begged, bargained and even resorted to shell-foo like: find . -type f -name 'Makefile' -exec grep -Hn REQUIRE {} \; |\ sed -e 's,$.*$\\$,\1,g' -e 's,^.*=$.*$$,\1,g' | sed -n 'H;${g;s/\n//gp}'| \ sed -e 's,[ ]*$[^ ]*$,\1\n,g' | sort -u | uniq | xargs -I ® svn update ® in the l4/pkg dir, to try and fix any unmet dependencies, but to no avail. So I guess I wouldn't mind a little help at this point. best regards Daniel

2 3

Processor compatibility
by Jason Philip 26 Jan '11

26 Jan '11

Is Pistachio compatible with Intel Celeron processor?

3 3

PCI Bus access
by Jason Philip 25 Jan '11

25 Jan '11

I am planning to interfacing the PCI bus using L4, however, I do not quite know how PCI interface works. I know that there is three memory region: configuration space, I/O space and Memory space, and that configuration space is use to detect and configure the device, but I do not know where any of this space are located and the protocol for interfacing them. Please help.

2 1

Privilege threads
by Jason Philip 24 Jan '11

24 Jan '11

how do you create privileged threads?

2 1

PingPong not working
by Jason Philip 23 Jan '11

23 Jan '11

I tried to build kernel and user level applications, but them don't work. When I boot the kernel using QEMU it tell me "loading kernel" but never go further. I try use user level application from earlier version and they work but I can't get my own build to work, why this happening?

3 5

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

l4-hackers