This list is intended for discussions about the L4 microkernel family and software running on top of L4. ()

headers eric johnson | 1 Aug 05:36

_______________________________________________
l4-hackers mailing list
l4-hackers <at> os.inf.tu-dresden.de
http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers

Hi,

I am still trying to run l4linux on top of fiasco. I am running it on
top of a console system and configured L4Linux2.6 without any input
drivers. Thanks to your suggestion I am loading vmlinuz with a start script.

I can't tell you much, but once booted both serial and console are
spammed with

...
l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94140
l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94150
l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94160
...

messages.

Did I forget to configure some kind of memory translation unit?

Here is my grub config:

kernel /bin/svn453/bootstrap -serial
modaddr 0x03000000
module /bin/svn453/fiasco -nokdb -nowait -serial -comspeed 115200
-pcsampling -debug -sp 1000000
module /bin/svn453/sigma0
module /bin/svn453/roottask task modname "bmodfs" attached 7 modules
module /bin/svn453/dm_phys
module /bin/svn453/names --verbose 0 --logsrv logcon
module /bin/svn453/events
module /bin/svn453/simple_ts --events -t 300
module /bin/svn453/l4io
module /bin/svn453/bmodfs
 module /bin/svn453/l4linux26.cfg
 module /bin/svn453/libloader.s.so
 module /bin/svn453/libld-l4.s.so
 module /bin/svn453/logcon
 module /bin/svn453/run
 module /bin/svn453/vmlinuz
 module /bin/svn453/drops-rd.rd
module /bin/svn453/loader --events --fprov=BMODFS run l4linux26.cfg  logcon
module /bin/svn453/con --nolog
vbeset 0x117

Thanks for your help.

Kind Regards,
Stefan

Hi,

On Tue Aug 04, 2009 at 11:11:15 +0200, Stefan Kögel wrote:
> I am still trying to run l4linux on top of fiasco. I am running it on
> top of a console system and configured L4Linux2.6 without any input
> drivers. Thanks to your suggestion I am loading vmlinuz with a start script.
> 
> I can't tell you much, but once booted both serial and console are
> spammed with
> 
> ...
> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94140
> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94150
> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94160
> ...
> 
> messages.
> 
> Did I forget to configure some kind of memory translation unit?

No but I'd guess that there's some driver in the Linux that causes this.
Maybe you could start from the x86-ux or x86-native defconfigs and see
if the same happens?

Adam
--

-- 
Adam                 adam <at> os.inf.tu-dresden.de
  Lackorzynski         http://os.inf.tu-dresden.de/~adam/

On Wed Jul 29, 2009 at 13:03:57 +0300, Roman Beslik wrote:
> Hello -- see the attachment.

Just for the diff of .yy files. The change is fine per se but
unfortunately breaks with older versions of bison which are still used.
One way could be to include the generated files in the distribution.

Adam
--

-- 
Adam                 adam <at> os.inf.tu-dresden.de
  Lackorzynski         http://os.inf.tu-dresden.de/~adam/

On Fri Jul 31, 2009 at 20:36:37 -0700, eric johnson wrote:
> i m using a pistachio L4 kernel. ( with no operating system on top. )
> I am running this on an emulator ( qemu) .  So i dont have a way of having
> real interrupts. There might be a way in qemu to do that , but i dont know
> how.
> 
> My question is : i figure there is an interrupt thread for every interrupt.
> ? Since i dont have any real hardware i would like to have a interrupt
> thread for a random interrupt no. How do i make sure that this interrupt
> thread is created ? I am trying to simulate the behaviour of an interrupt
> processing in L4.

Why do you think that Qemu's interrupts are not real from the point of
view of the software running on it?

Adam
--

-- 
Adam                 adam <at> os.inf.tu-dresden.de
  Lackorzynski         http://os.inf.tu-dresden.de/~adam/

_______________________________________________
l4-hackers mailing list
l4-hackers <at> os.inf.tu-dresden.de
http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers

Hi,

I started from a default l4linux26 kernel config. I did not touch
anything, except for the things I had to, like acpi, apic, MTRR, MCE ..
and the stuff that is missing (olpc, scx200 and these things).
Everything else is default.
The problem still exists but I was able to gather some info.

Executing the l4linux26.cfg prints out:

loader  | sleeping for 1000 ms
loader  | vmlinuz: Starting application using libld-l4.s.so
loader  | vmlinuz,#11: Loading binary
loader  | vmlinuz,#11: Loading ldso
loader  | vmlinuz,#11: Starting libld-l4.s.so at 00013940 via 0000cc3c
loader  | DEBUG file = vmlinuz
l4lx    | ======> L4Linux 2.6 starting... <========
l4lx    | Linux version 2.6.30-l4 (stefan <at> scarface) (gcc version 4.3.2
(Ubuntu
l4lx    : 4.3.2-1ubuntu12) ) #10 Wed Aug 5 16:45:57 CEST 2009
l4lx    | Binary name: vmlinuz
l4lx    | Linux kernel command line (5 args): mem=64M load_ramdisk=1
ramdisk_si
l4lx    : ze=16384 root=/dev/ram l4env_rd=drops-rd.rd
l4lx    | Image: 00400000 - 00874000 [4560 KiB].
l4lx    | Areas: Text:     00400000 - 006fd000 [3060kB] (a bit longer)
l4lx    |        Data:     006fd000 - 007280e8 [172kB]
l4lx    |        Initdata: 0072c000 - 00770000 [272kB]
l4lx    |        BSS:      00772000 - 00853a94 [902kB]
l4lx    | l4lx_thread_create: Created thread 11.03 (tamer0)
l4lx    | Tamer0 is 11.03
l4lx    | Using tamed mode.
ROOT: Task #0c is not allowed to execute cli/sti
loader  | vmlinuz,#11: WARNING: Can't map I/O space, ROOT denies page
(result=0
loader  : 0004000)
loader  | vmlinuz,#11: Not allowed to perform any I/O
l4lx    | Got 0 out of 65536 I/O ports
l4lx    | Connecting to l4io server.
l4lx    | l4env_linux_startup thread 4.
l4lx    | l4lx_thread_create: Created thread 11.04 (cpu0)
l4lx    | main thread will be 11.04
l4lx    | l4env_register_pointer_section: addr = 0072a000 size = 290816
l4lx    |      sec-w-init: virt: 0x0072a000 to 0x00770fff [284 KiB]
l4lx    | Noncontiguous region for sec-w-init
l4lx    |      sec-w-init: Number of physical regions: 2, 290816 Bytes
l4lx    |      sec-w-init: 1: Phys: 0x014f0000 to 0x01500000, Size:    65536
l4lx    |      sec-w-init: 2: Phys: 0x013b5000 to 0x013ec000, Size:   225280
l4lx    | main thread: received startup message.
l4lx    | Main thread running, waiting...
l4lx    | memory_setup: mem=64M load_ramdisk=1 ramdisk_size=16384
root=/dev/ram
l4lx    :  l4env_rd=drops-rd.rd
l4lx    | setup_l4env_memory: Forcing superpages for main memory
l4lx    | Main memory size: 64MB
l4lx    |     Main memory: virt: 0x00c00000 to 0x04bfffff [65536 KiB]
l4lx    |     Main memory: Number of physical regions: 1, 67108864 Bytes
l4lx    |     Main memory: 1: Phys: 0x07400000 to 0x0b400000, Size: 67108864
l4lx    | Filling lower ptabs...
l4lx    | mainmem = c00000
l4lx    | Done (1864 entries).
l4lx    | l4env_register_pointer_section: addr = 00772000 size = 1056768
l4lx    |             end: virt: 0x00772000 to 0x00873fff [1032 KiB]
l4lx    |             end: Number of physical regions: 1, 1056768 Bytes
l4lx    |             end: 1: Phys: 0x06499000 to 0x0659b000, Size:  1056768
l4lx    | memory_setup done
l4lx    | l4env_rd_path: drops-rd.rd
l4lx    | Loading: drops-rd.rd
l4lx    | INITRD: Size of RAMdisk is 16384KiB
l4lx    | RAMdisk from 04c00000 to 05c00000 [16384KiB]
l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x80000
l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x80010
l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x80020
...

and continues untiel physical address 0x9fff0 and ends with a lock up of
the computer.

I am wondering about these lines:

ROOT: Task #0c is not allowed to execute cli/sti
loader  | vmlinuz,#11: WARNING: Can't map I/O space, ROOT denies page
(result=0
loader  : 0004000)
loader  | vmlinuz,#11: Not allowed to perform any I/O

Could that be causing the error? How can I fix this?

Thank you for help.
Kind Regards,
Stefan
> Hi,
>
> On Tue Aug 04, 2009 at 11:11:15 +0200, Stefan K?gel wrote:
>   
>> I am still trying to run l4linux on top of fiasco. I am running it on
>> top of a console system and configured L4Linux2.6 without any input
>> drivers. Thanks to your suggestion I am loading vmlinuz with a start script.
>>
>> I can't tell you much, but once booted both serial and console are
>> spammed with
>>
>> ...
>> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94140
>> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94150
>> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x94160
>> ...
>>
>> messages.
>>
>> Did I forget to configure some kind of memory translation unit?
>>     
>
> No but I'd guess that there's some driver in the Linux that causes this.
> Maybe you could start from the x86-ux or x86-native defconfigs and see
> if the same happens?
>
>
>
> Adam
>   

Hi,

On Wed Aug 05, 2009 at 19:39:00 +0200, Stefan Kögel wrote:
> I started from a default l4linux26 kernel config. I did not touch
> anything, except for the things I had to, like acpi, apic, MTRR, MCE ..
> and the stuff that is missing (olpc, scx200 and these things).
> Everything else is default.
> The problem still exists but I was able to gather some info.
> 
> Executing the l4linux26.cfg prints out:
> 
> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x80000
> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x80010
> l4lx    | l4env_phys_to_virt: Could not translate phys. address 0x80020
> ...
> 
> and continues untiel physical address 0x9fff0 and ends with a lock up of
> the computer.

L4Linux will not work but the system would still run.

My guess is that ISCSI_IBFT_FIND is enabled. This option causes scans
through physical memory, and the conversion functions in L4Linux are
built in a conservative way because if something goes wrong this can
lead to very subtle issues.
If my guess is wrong you should get a backtrace when you enable
earlyprintk on the kernel command line (i.e. it's already there but not
printed (yet)).

> I am wondering about these lines:
> 
> ROOT: Task #0c is not allowed to execute cli/sti
> loader  | vmlinuz,#11: WARNING: Can't map I/O space, ROOT denies page
> (result=0
> loader  : 0004000)
> loader  | vmlinuz,#11: Not allowed to perform any I/O
> 
> Could that be causing the error? How can I fix this?

Adding allow_cli as an option flag to the loader script will give
L4Linux all I/O rights and make the message go away.

Adam
--

-- 
Adam                 adam <at> os.inf.tu-dresden.de
  Lackorzynski         http://os.inf.tu-dresden.de/~adam/

Hi Udo,

thanks so much for your reply and sorry for the delayed answer.
I will write a pure L4 based system trasher like you suggested.
However, as running a L4Lx next to the RT part of my system is a quite 
common use
case, I will also benchmark this part.
As I wrote in my last mail, I used hackbench [1]  (among others) to 
evaluate in legacy Linux system.
This is a quite evil tool that creates groups of tasks that communicate 
with each other via sockets.
Running this tool under L4Lx really block any other task (even with 
higher priority).
I am neither sure what exactly causes these interruption, nor how to 
eliminate them.
Any experience with these kind of tools or any other advice is highly 
appreciated?

Cheers,
Andre

[1] http://devresources.linux-foundation.org/craiger/hackbench/

Udo A. Steinberg wrote:
> On Tue, 21 Jul 2009 18:00:42 +0200 Andre Puschmann (AP) wrote:
>
> AP> I now want to put some load on the system as I did in native Linux with
> AP> tools like "hackbench" and "cache calibrator". Any suggestions how to
> AP> achieve this under L4? The same tools inside a L4Linux environment?
>
> Write some programs that continuously do IPC across task boundaries. If you
> want to trash the caches, memset contiguous regions of memory that are larger
> than the sum of all your cache sizes. The "pingpong" program should give you
> some ideas how to implement these kind of things.
>
> Cheers,
>
> 	- Udo
>   

Hi,

For those out there who missed the publicity (incl ./): NICTA
announced last week that the formal verification of our seL4 kernel
has been completed. This makes seL4 the first ever general-purpose OS
kernel with a formal proof that the implementation is consistent with
the specification.

A paper on the project will appear in this year's SOSP.

Details at http://ertos.nicta.com.au/news/home.pml#verified

Gernot

10	February 2012
24	January 2012
23	December 2011
42	November 2011
60	October 2011
46	September 2011
39	August 2011
44	July 2011
52	June 2011
45	May 2011
31	April 2011
47	March 2011
71	February 2011
61	January 2011
21	December 2010
66	November 2010
6	October 2010
16	September 2010
28	August 2010
1	July 2010
10	June 2010
15	May 2010
30	April 2010
14	March 2010
15	February 2010
26	January 2010
20	December 2009
16	November 2009
25	October 2009
18	September 2009
27	August 2009
29	July 2009
21	June 2009
15	May 2009
96	April 2009
84	March 2009
49	February 2009
24	January 2009
25	December 2008
29	November 2008
66	October 2008
19	September 2008
13	August 2008
20	July 2008
35	June 2008
49	May 2008
37	April 2008
74	March 2008
17	February 2008
99	January 2008
17	December 2007
34	November 2007
39	October 2007
110	September 2007
79	August 2007
123	July 2007
73	June 2007
79	May 2007
52	April 2007
60	March 2007
29	February 2007
47	January 2007
80	December 2006
63	November 2006
49	October 2006
38	September 2006
113	August 2006
35	July 2006
68	June 2006
75	May 2006
39	April 2006
44	March 2006
20	February 2006
52	January 2006
27	December 2005
54	November 2005
70	October 2005
77	September 2005
74	August 2005
114	July 2005
182	June 2005
76	May 2005
26	April 2005
83	March 2005
105	February 2005
24	January 2005
13	December 2004
18	November 2004
27	October 2004
38	September 2004
8	August 2004
6	July 2004
10	June 2004
11	May 2004
1	March 2004
10	February 2004
27	January 2004

interrupt registration

problems running l4linux No.2

Re: problems running l4linux No.2

Re: compiling Fiasco trunk, Bison trouble

Re: interrupt registration

Re: interrupt registration

Re: problems running l4linux No.2

Re: problems running l4linux No.2

Re: Howto implement a periodic real-time task?

seL4 kernel is formally verified

Mon	Tue	Wed	Thu	Fri	Sat	Sun

					1	2
3	4	5	6	7	8	9
10	11	12	13	14	15	16
17	18	19	20	21	22	23
24	25	26	27	28	29	30
31