- l4-hackers - example.com Site

RE: ore problems
by Bjoern Doebel 17 Jun '08

17 Jun '08

Hi Li, Please consider using the l4-hackers mailing list for such questions, because you might get faster answers there. > I install ore in my machine and start it in qemu, but I get > these informations, what's the problem, thanks. > > First I'll show you my menu.lst > > title ORe > kernel /bootstrap -serial -modaddr 0x2000000 > module /fiasco -serial_esc -comport 1 > module /sigma0 > module /roottask task modname "bmodfs" attached 1 modules > module /names > module /log > module /l4io > module /events > module /dm_phys > module /simple_ts > module /bmodfs > module /ore > module /loader -fprov=BMODFS ore The menu.lst looks fine so far. > The output in qemu is > > io | Using platform configuration 'x86' > io | PCI: Using configuration type 1 > io | PCI: Probing PCI hardware > io | PCI: Probing PCI hardware (bus 00) > io | PCI: PIIX3: Enabling Passive Release on 00:01.0 > io | Limiting direct PCI/PCI transfers. > io | Activating ISA DMA hang workarounds. > io | 00000000-ffffffff : PCI mem > io | e0000000-e1ffffff : Cirrus Logic GD 5446 > io | e2000000-e2000fff : Cirrus Logic GD 5446 > io | e3000000-e30000ff : Realtek Semiconductor Co., Ltd. RTL-8139/8139C/ > io : 8139C+ Ok. So you configure Qemu to emulate an RTL8139 network interface. > io | 0000-ffff : PCI IO > io | 0cf8-0cff : PCI conf1 > io | 1000-100f : Intel Corporation 82371SB PIIX3 IDE [Natoma/Triton II] > io | 1400-14ff : Realtek Semiconductor Co., Ltd. RTL-8139/8139C/8139C+ > io | b100-b11f : Intel Corporation 82371AB/EB/MB PIIX4 ACPI > bmodfs | Passed the following modules: > bmodfs | module "/ore" (2176kB) > loader | "ore" is a valid binary image > loader | ore: Starting sigma0-style application > loader | ore: Loading binary > loader | ore,#d: Entry at 00009f8c => 01800000 > loader | ore,#d: Started > io | Available IRQs=[ <!0> 1 <!2> 3 <!4> 5 6 7 8 9 a b c d e f 10 11 ] > ore | Softirq daemon starting > ore | Initializing DDE page cache > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | _add_ddekit_device: Detected device: 8086:7000 > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | _add_ddekit_device: Detected device: 8086:7010 > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | _add_ddekit_device: Detected device: 8086:7113 > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | _add_ddekit_device: Detected device: 1013:b8 > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | _add_ddekit_device: Detected device: 10ec:8139 > ore | <6>e100: Intel(R) PRO/100 Network Driver, 3.5.17-k2-NAPI > ore | <6>e100: Copyright(c) 1999-2006 Intel Corporation Here we see, that the e100 NIC driver is trying to initialize. However, there is no such NIC in your setup and therefore there is no eth0 available. Go to l4/pkg/ore/server and run "make config" and configure ORe to use the RTL8139 network driver. > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | unimplemented: pci_fixup_device > ore | l4dde26_register_rx_callback: New rx callback @ 0x018012f0. > ore | main(): initialized DDELinux2.6 > ore | main(): loopback: 0 > ore | <6>device lo entered promiscuous mode > ore | main(): Initialized 1 network devices. > ore | Device = lo, IRQ = 0, MAC = 00:00:00:00:00:00 > ore | main(): Registering 'ORe' at names... > ore | main(): Ready for service. Kind regards, Bjoern

1 0

Compiling L4 with a different Fiasco Config
by Stefan Kögel 13 Jun '08

13 Jun '08

I downloaded the svn (version 373) hello module and would like to compile it. I use: - make -C l4 O=/my-build oldconfig - make O=/my-build Here "make" always compiles the kernel using the ia32short template. Compiling Fiasco separately with a different config works fine. Now my questions: Is it possible to build L4 using a different Fiasco Config? If so, how? Is it possible to compile L4 hello module without building the kernel and use this together with the separately build kernel? If so, how? Thanks for your help. Kind Regards, Stefan

2 2

CFP: JAR Special Issue On Operating Systems Verification
by Hendrik Tews 11 Jun '08

11 Jun '08

[apologies for crossposting, here is a CFP that might be interesting for those that are into formal methods -- Hendrik] Call for Papers Special Issue On Operating Systems Verification Journal of Automated Reasoning Industrial-strength software analysis and verification has advanced in recent years through the introduction of model checking, automated and interactive theorem proving, static analysis techniques, as well as correctness by design. However, many techniques are working under restrictive assumptions which are invalidated by complex (embedded) system software such as operating system kernels, low-level device drivers or microcontroller code. This special issue will be devoted to the formal verification of operating systems and similar low-level systems code. The emphasis is on techniques and methods that provide real solutions to real software problems. A real solution is one that is applicable to the problem in industry and not one that only applies to an abstract, academic toy version of it. Submissions are encouraged, but not limited to, the following topics and their application to operating systems or low-level systems code: * model checking * automated and interactive theorem proving * embedded systems development * programming languages * verifying compilers * software certification Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. Papers should be in pdf format, following the JAR guidelines for authors, and be submitted via EasyChair at: http://www.easychair.org/conferences/?conf=jarosv08 Please do not use the Springer online submission system for the special issue at this stage, but EasyChair instead. To encourage a speedy review cycle, it will be expected that authors of submissions also serve as referees. For more information, please see http://www.cse.unsw.edu.au/~kleing/JAR-OSV-08/ Guest Editors Gerwin Klein, NICTA, Australia, gerwin.klein at nicta.com.au Ralf Huuck, NICTA, Australia, ralf.huuck at nicta.com.au Bastian Schlich, RWTH Aachen, Germany, schlich at cs.rwth-aachen.de Important Dates Sep 15 2008 Submission Deadline Dec 15 2008 Notification of accepted papers Jan 15 2009 Final version

1 0

timing right
by eric johnson 07 Jun '08

07 Jun '08

i need to write a user land program which would measure the times in milliseconds . how do i do this ? i wouldnt want to make a system call. ej

2 1

Driving audio card
by Saya Sheng (盛淑蕙) 06 Jun '08

06 Jun '08

Hi all, Does anybody know whether there are some documents in English for teaching how to drive a audio card such that a application on l4 can use it? It is known that driver can be ported via DDE but how to do that? I am a newbie in this area, Could you please give me some advice? Thanks in advance Saya

3 2

New list member Mike Jolley
by John van V. 31 May '08

31 May '08

Hi Mike (and all), I am writing about L4, its hopeful development path, and how ubiquity in systems can lead to information democracy. The goals are naturally social, but the technology layer is key. I think you have good ideas and I hope you are able to bring them to fully working level. I hope you can be verbose about your research and can supply all your resources, and perhaps images, for the pubic. I have two sites that I want use as a vehicles for this research direction, http://thinman.com , which is the culmination of my work and also my fully independent degree in Information Technology. While I was in financial technology (1990-2003), I used my time to develop the Thinman model, which is a purely sharing ubiquitous model whose sharing is inspired by Perl's CPAN system, where this type of component module system works at the OS level rather than in userland. I also have information at the Linux Society blog, which is an artifact from the very active free systems clubs of the 1990s in NYC. There I have some writing by Gernot about the need for an OS learning path in middle schools; something that Abe Maslow would agree with. I was in technology from 1990 to 2003, when developmental technology was moved to India. Since the I have pursued teaching, but now I work in retail and study social psychology. John Empathy http://thinman.com/empathy Photography http://thinman.com/photography Technology http://thinman.com

1 0

New list member Mike Jolley
by Mike Jolley 31 May '08

31 May '08

Hi all, I'm new to this mailing list but I've done a little study of the source code, history, and other things surrounding Pistachio and L4-Hurd. My knowledge of L4 is very limited. I have a goal of a drop-in Linux replacer built on much better technology, such as L4 or the kind of work being done at VPRI. I have a rough design for such a thing but a lot of major pieces are missing. On the other hand, a totally new (to me) system with enough apps to get me through the day would be good too. The system I'm currently looking at is Coyotos, which is based on EROS and KeyKOS. These systems feature capability security, and I read somewhere that L4 was designed with this in mind. I can't find much info about that. I'd appreciate any information about any of this that seems relevant, even if it has nothing to do with any specific thing I've mentioned. If this list wouldn't be interested in what you have to say, you can email me privately at mikejolley(a)sbcglobal.net. Thanks a lot, Mike Jolley

2 1

Question about ipcmon and assembler IPC shortcut
by Marc CHALAND 30 May '08

30 May '08

Hi, I've made a little test with ipcmon. This test is a simple application launched by loader which makes an IPC to names (05) and to log server (06). With assembler IPC shortcut, I don't need to set an accept rule to names. ipcmon doesn't handle requests to names. If I activate jdb IPC monitoring, then IPC to names are handled by ipcmon. After some more checking, it seems that assembler IPC shortcut doesn't care about parity. For example, if 4 (roottask) is allowed, then 5 is also allowed only for assembler code. I tried to find a bug, but I don't know where capability is checked in assembler code (ia32). Does anybody know where this check is done ? Regards Marc

2 1

How to eliminate echoes when loading module
by Shih-I Huang 27 May '08

27 May '08

Hi all, I am currently trying to use microkernel in our platform (X86 platform). However, I found the Fiasco returns many echoes when booting and I would like to remove them. Is there any way to remove these echoes? Besides, is there any way to display an image when booting system? (like usplash in Ubuntu) Thanks in advance. Eric.

2 1

fiasco can't start correctly
by fei li 27 May '08

27 May '08

Hi I have compiled the fiasco and l4 packages in the amd64 environment, now I get some binaries that I try to start the l4 in qemu, next is my menu.lst color 24 52 title Example entry kernel /bootstrap32 -serial -modaddr 0x2000000 module /main module /sigma0 module /roottask module /omega0 Then in the qemu, it says "Read-write (data) checksum does not match", next is the outputs in the qemu window L4 Bootstrapper move modules to 2000000 with offset ed0000 move module 4 start 126e000 -> 213e000 move module 3 start 11d0000 -> 20a0000 move module 2 start 119c000 -> 206c000 move module 1 start 1130000 -> 2000000 Scanning /main Scanning /sigma0 Scanning /roottask Bootloader MMAP: [ 0, 9fc00) RAM (1) [ 9fc00, a0000) reserved (2) [ e8000, 100000) reserved (2) [ 100000, 7ff0000) RAM (1) [ 7ff0000, 8000000) ACPI (3) [ fffc0000, 100000000) reserved (2) Relocated mbi to [0x76000-0x760b8] Loading /main Loading /sigma0 Loading /roottask find kernel info page... found kernel info page at 0x1000 [ 1000, 75fff] Kern /main [ 76000, 761b5] Root Multiboot info [ 9fc00, 9ffff] Arch BIOS [ e8000, fffff] Arch BIOS [ 100000, 10a6df] Sigma0 /sigma0 [ 110000, 2c6fff] Root /roottask [ 2d0080, 2daf57] Boot bootstrap [ 300000, 34a8af] Kern /main [ 213e000, 2187e07] Root Modules Memory [ 7ff0000, 7ffffff] Arch BIOS [ fffc0000, ffffffff] Arch BIOS API Version: (87) experimental Sigma0 config ip:0000000000104780 sp:00000000002da990 Roottask config ip:0000000000110000 sp:0000000000000000 Starting kernel /main at 0000000000300ad0 Now i guess there are problems with the "main" binary, but i don't know what it is. # CONFIG_IA32 is not set CONFIG_AMD64=y # CONFIG_ARM is not set CONFIG_PF_PC=y # CONFIG_PF_UX is not set # CONFIG_PF_REALVIEW is not set # CONFIG_PF_INTEGRATOR is not set # CONFIG_PF_XSCALE is not set # CONFIG_PF_SA1100 is not set CONFIG_ABI_V2=y # CONFIG_ARM_PXA is not set # CONFIG_ARM_SA is not set # CONFIG_ARM_920T is not set # CONFIG_ARM_926 is not set # CONFIG_ARM_1176 is not set # CONFIG_ARM_MPCORE is not set # CONFIG_IA32_486 is not set # CONFIG_IA32_586 is not set # CONFIG_IA32_686 is not set # CONFIG_IA32_P2 is not set # CONFIG_IA32_P3 is not set # CONFIG_IA32_P4 is not set # CONFIG_IA32_PM is not set # CONFIG_IA32_K6 is not set # CONFIG_IA32_K7 is not set # CONFIG_IA32_K8 is not set CONFIG_AMD64_K8=y CONFIG_SCHED_PIT=y # CONFIG_SCHED_RTC is not set # CONFIG_SCHED_APIC is not set # CONFIG_WORKAROUND_AMD_FPU_LEAK is not set # # Kernel options # # CONFIG_PL0_HACK is not set CONFIG_TASK_CAPS=y # CONFIG_USER_LOCKS is not set CONFIG_ASSEMBLER_IPC_SHORTCUT=y CONFIG_CONTEXT_4K=y CONFIG_IO_PROT=y # CONFIG_IO_PROT_IOPL_3 is not set # # Debugging # CONFIG_INLINE=y # CONFIG_NDEBUG is not set CONFIG_NO_FRAME_PTR=y CONFIG_STACK_DEPTH=y # CONFIG_LIST_ALLOC_SANITY is not set # CONFIG_BEFORE_IRET_SANITY is not set CONFIG_SERIAL=y CONFIG_JDB=y CONFIG_JDB_MISC=y CONFIG_POWERSAVE_GETCHAR=y # CONFIG_WARN_NONE is not set CONFIG_WARN_WARNING=y # CONFIG_WARN_ANY is not set # # Compiling # CONFIG_CC="gcc" CONFIG_CXX="g++" CONFIG_HOST_CC="gcc" CONFIG_HOST_CXX="g++" CONFIG_VERBOSE=y CONFIG_MAINTAINER_MODE=y CONFIG_LABEL="" CONFIG_EXPERIMENTAL=y CONFIG_PERF_CNT=y CONFIG_BIT64=y CONFIG_WARN_LEVEL=1 CONFIG_XARCH="amd64" CONFIG_IA32_TARGET="AMD Opteron" CONFIG_ABI="v2" CONFIG_DECEIT_BIT_DISABLES_SWITCH=y I choose amd64 in the "cpu type" option, then i get the errors I have mentioned, then i keep the default config and when I start the l4 in qemu, it says Scanning /main This is an invalid binary, fix it. I don't know why, i hope someone could help me and thanks.

2 4