Hi,
For my verification of Fiasco I would like to test some of the assumptions I am making in the proof. One way to test these assumptions is to add these assumptions as assert() calls in the kernel and check if they fire when the kernel is running a stress-test. The idea is to create an L4Linux instance and run an IPC-intensive application on it.
For the compilation of l4-env and Fiasco I followed the instructions on this webpage: http://os.inf.tu-dresden.de/L4/LinuxOnL4/build-2.6.shtml. However, when I tried to execute step 3 (Go to the l4 directory and call make config) the system complained: make config does not work: need to give builddir with O=.../buildir. Stop. Of course this was easy to correct but I thought Id notify you anyway.
After compiling Fiasco and l4-env, I thought Id try out the hello module. I moved the fiasco, irq0 and ux-con files from the Fiasco build directory to the DROPS build directory after which I started Fiasco as follows: ./fiasco l hello
This resulted in the following:
Bootstrapping...
Welcome to Fiasco(ux)! DD-L4(v2)/x86 microkernel (C) 1998-2006 TU Dresden Rev: Thu Dec 21 08:55:14 2006 compiled with gcc 3.4.6 for Intel Pentium
CPU: AuthenticAMD (6:6:2:0) Model: Athlon (Palomino) at 1160 MHz
16/256 Entry I TLB (4K pages) 8 Entry I TLB (4M pages) 32/256 Entry D TLB (4K pages) 8 Entry D TLB (4M pages) 64 KB L1 I Cache (2-way associative, 64 bytes per line) 64 KB L1 D Cache (2-way associative, 64 bytes per line) 256 KB L2 U Cache (8-way associative, 64 bytes per line)
Freeing init code/data: 24576 bytes (6 pages)
Calibrating timer loop... done. SIGMA0: Hello! KIP @ 39f5000 Found Fiasco: KIP syscalls: yes allocated 4KB for maintenance structures
--Interception--------------------------------------ESP:00096748 EIP:000907cf (2.00) jdb: As you can see we automatically entered the debugger, any attempt to continue (using the g command) failed. I compiled Fiasco with the following options: Target platform: UX Exception IPC: Y Handle and preserve segments: Y Graphical console: Y Generate inline code: Y
I also tried to run a test of Fiasco using: ./fiasco T which indicates that something is wrong:
Fiasco-UX on Linux 2.6.18-1.2798.fc6 (i686) Mapped 64 MB Memory + 0 KB Framebuffer + 0 MB Input Area on FD 3
Bootstrapping...
Welcome to Fiasco(ux)! DD-L4(v2)/x86 microkernel (C) 1998-2006 TU Dresden Rev: Thu Dec 21 08:55:14 2006 compiled with gcc 3.4.6 for Intel Pentium
CPU: AuthenticAMD (6:6:2:0) Model: Athlon (Palomino) at 1160 MHz
16/256 Entry I TLB (4K pages) 8 Entry I TLB (4M pages) 32/256 Entry D TLB (4K pages) 8 Entry D TLB (4M pages) 64 KB L1 I Cache (2-way associative, 64 bytes per line) 64 KB L1 D Cache (2-way associative, 64 bytes per line) 256 KB L2 U Cache (8-way associative, 64 bytes per line)
Freeing init code/data: 24576 bytes (6 pages)
Calibrating timer loop... done.
KERNEL: 2.0 (tcb=20080000) killed: Unhandled trap
EAX 00000000 EBX 0000c000 ECX 039f5000 EDX 00000000 ESI 00000000 EDI 00000000 EBP 00000000 ESP bf9ee09c EIP 00002000 EFLAGS 00200246 CS 0002 SS 007b DS 007b ES 007b FS 0000 GS 0007 trap 13 (General Protection), error 00000402, from user mode (internal event regarding IDT gate descriptor no. 0x80)
--Interception--------------------------------------ESP:20000790 EIP:0004ee8b (0.00) jdb: Do you have any idea what might be wrong?
With regards,
Erik Schierboom
---------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program.
Hi,
On Thu Mar 29, 2007 at 09:26:46 +0200, eschierb@sci.kun.nl wrote:
For my verification of Fiasco I would like to test some of the assumptions I am making in the proof. One way to test these assumptions is to add these assumptions as assert() calls in the kernel and check if they fire when the kernel is running a stress-test. The idea is to create an L4Linux instance and run an IPC-intensive application on it.
For the compilation of l4-env and Fiasco I followed the instructions on this webpage: http://os.inf.tu-dresden.de/L4/LinuxOnL4/build-2.6.shtml. However, when I tried to execute step 3 (Go to the l4 directory and call make config) the system complained: make config does not work: need to give builddir with O=.../buildir. Stop. Of course this was easy to correct but I thought Id notify you anyway.
Thanks, I fixed it.
After compiling Fiasco and l4-env, I thought Id try out the hello module. I moved the fiasco, irq0 and ux-con files from the Fiasco build directory to the DROPS build directory after which I started Fiasco as follows: ./fiasco l hello
This resulted in the following:
Bootstrapping...
Welcome to Fiasco(ux)! DD-L4(v2)/x86 microkernel (C) 1998-2006 TU Dresden Rev: Thu Dec 21 08:55:14 2006 compiled with gcc 3.4.6 for Intel Pentium
CPU: AuthenticAMD (6:6:2:0) Model: Athlon (Palomino) at 1160 MHz
16/256 Entry I TLB (4K pages) 8 Entry I TLB (4M pages) 32/256 Entry D TLB (4K pages) 8 Entry D TLB (4M pages) 64 KB L1 I Cache (2-way associative, 64 bytes per line) 64 KB L1 D Cache (2-way associative, 64 bytes per line) 256 KB L2 U Cache (8-way associative, 64 bytes per line)
Freeing init code/data: 24576 bytes (6 pages)
Calibrating timer loop... done. SIGMA0: Hello! KIP @ 39f5000 Found Fiasco: KIP syscalls: yes allocated 4KB for maintenance structures
--Interception--------------------------------------ESP:00096748 EIP:000907cf (2.00) jdb:
I have a suspicion but would like to see your sigma0 binary to verify. Can send it to me?
As you can see we automatically entered the debugger, any attempt to continue (using the g command) failed. I compiled Fiasco with the following options: Target platform: UX Exception IPC: Y Handle and preserve segments: Y Graphical console: Y Generate inline code: Y
Nothing wrong with these options.
I also tried to run a test of Fiasco using: ./fiasco T which indicates that something is wrong:
As this is just a switch switch for developemnt this behaviour is ok.
Adam
On Thu Mar 29, 2007 at 10:07:17 +0200, Adam Lackorzynski wrote:
After compiling Fiasco and l4-env, I thought Id try out the hello module. I moved the fiasco, irq0 and ux-con files from the Fiasco build directory to the DROPS build directory after which I started Fiasco as follows: ./fiasco l hello
This resulted in the following:
Bootstrapping...
Welcome to Fiasco(ux)! DD-L4(v2)/x86 microkernel (C) 1998-2006 TU Dresden Rev: Thu Dec 21 08:55:14 2006 compiled with gcc 3.4.6 for Intel Pentium
CPU: AuthenticAMD (6:6:2:0) Model: Athlon (Palomino) at 1160 MHz
16/256 Entry I TLB (4K pages) 8 Entry I TLB (4M pages) 32/256 Entry D TLB (4K pages) 8 Entry D TLB (4M pages) 64 KB L1 I Cache (2-way associative, 64 bytes per line) 64 KB L1 D Cache (2-way associative, 64 bytes per line) 256 KB L2 U Cache (8-way associative, 64 bytes per line)
Freeing init code/data: 24576 bytes (6 pages)
Calibrating timer loop... done. SIGMA0: Hello! KIP @ 39f5000 Found Fiasco: KIP syscalls: yes allocated 4KB for maintenance structures
--Interception--------------------------------------ESP:00096748 EIP:000907cf (2.00) jdb:
I have a suspicion but would like to see your sigma0 binary to verify. Can send it to me?
I see nothing wrong with the sigma0 binary itself. I now suspect your FC host kernel is doing something different. Do you have a chance to test on a rather unmodified Linux host kernel?
Adam
Adam Lackorzynski adam@os.inf.tu-dresden.de writes:
I see nothing wrong with the sigma0 binary itself. I now suspect your FC host kernel is doing something different. Do you have a chance to test on a rather unmodified Linux host kernel?
Eriks binaries run fine on my machine (debian etch) and on lilo.science.ru.nl (Fedora Core release 5 (Bordeaux)).
Bye,
Hendrik
l4-hackers@os.inf.tu-dresden.de