l4-hackers August 2008

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

9 participants
8 discussions

Back to UTCB IPC
by Marc CHALAND 11 Oct '09

11 Oct '09

Hi, I am back with my problem with UTCB IPC. To sum up the context : I use pure l4env applications. Here is the scenario between my server and my client : 1. client makes an UTCB IPC to manager. Manager does an l4rm_area_reserve, creates a rcv_fpage, creates worker and sends back worker thread id to client. 2. client allocates memory and associated flexpage and sends it to server. 3. UTCB IPC is sent to worker with 3 parameters : - on client side : utcb->values=0xbff00200: arg1=0x2 arg2=0x1 arg3=0x6 - on server side : utcb->values=0xbff00200: arg1=0x241401 arg2=0x0 arg3=0x7069776c It seems that 0xbff00200 is not mapped on the same memory on client and server side. As there is no problem for first IPC (utcb->values is also 0xbff00200), is there any potential problem with flexpage ? As utcb->values is still the same, what happens if several threads try to make UTCB IPC ? Another question : when I link my application with liblogserver.a, I have strange logs : .rm.sem.mainMain function returned. It seems that .rm .sem and .main are added by l4env, but I didn't find where. Regards Marc

4 9

Questions about L4 API V2
by Sean 06 Sep '08

06 Sep '08

Dear We are currently working on the ukernel design and survey the L4 API interface. For Fiasco, it is implemented on L4/V2 and L4/X.0 interfaces. If we implement a new u-kernel by ourselves that follows the same L4 API interface, will it still support the L4Env and L4Linux which will be put above this u-kernel? I think this issue is reasonable. Thanks a lot! Best Regards, Sean

3 4

ORe communication problems
by fei li 29 Aug '08

29 Aug '08

Hi, all: These days I tried to boot ORe in my machine and start the l4linux at the same time, my menu.lst is: title ORe kernel /bootstrap -serial -modaddr 0x2000000 module /fiasco -serial_esc -comport 1 module /sigma0 module /roottask task modname "bmodfs" attached 5 modules module /names module /log module /l4io module /events module /dm_phys --isa=0x00800000 -v --events module /simple_ts module /rtc module /ore module /mini_http_uip module /con --vbemode 0x11 module /loader --fprov=BMODFS l4linux.cfg module /bmodfs module /vmlinuz module /l4linux.cfg module /libloader.s.so module /libld-l4.s.so module /drops-rd.rd In qemu I can start the l4linux correctly. I set the ip address and it can access the internet, then in another qemu I started a second l4linux, but when I finished setting the ip addr, the previous one suspend accidently, ore | L4RM: [PF] read at 0x0000b014, ip 01802401, src C.04 ore | [C.0] l4rm/lib/src/pagefault.c:81:__unknown_pf(): ore | unhandled page fault --PANIC, 'g' for exit------------------------------------IP: 018267a5 [ore.rm] (c.00) jdb: t maybe this is helpless, but it told me that the l4linux is down, how can I start two l4linux with ORe modules installed and they can communicate with each other, I added "ORe instances" in the kernel command line, but it is helpless. I wish your help and thanks a lot.

2 3

2nd CFP: JAR Special Issue on OS Verification
by Hendrik Tews 29 Aug '08

29 Aug '08

[apologies for crossposting, here is a CFP that might be interesting for those that are into formal methods -- Hendrik] 2nd 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

Building self-debuggable system on L4?
by Derek Peschel 22 Aug '08

22 Aug '08

Someone in Russia was working on a source-level debugger for L4, I noticed, but I didn't see much else in the list archives relating to my question. (I searched for "[Dd]ebug" in the subject lines.) Has anyone investigated L4 as a foundation for interactive application and OS debugging? On UNIX (which I am most familiar with) program debugging is easy enough but kernel debugging is very disruptive. It would be interesting to see a system allowing most of itself to be changed while, in some sense e.g. for other tasks, it continues to run. Is L4 suited to building a system like that? What if portability was also a goal? L4 has jdb/kdb, but they stop the microkernel as I recall. However, that may not be a problem in my case. Ideally L4 would be small enough, and bug-free, so that my hypothetical new OS would never need to affect L4 proper. -- Derek

1 0

Fiasco on Intel Macbooks?
by Steffen Schulz 10 Aug '08

10 Aug '08

Hi all, Did anyone manage to start the Fiasco kernel on the Intel MacBooks? I have a MacBook Pro and get an error about the memory region beeing used by a BIOS. The reason is probably the BIOS emulation: For booting legacy BIOS-based operating systems, Apple takes a completely non-standard approach. The CSM (compatibility support module) is not loaded at all by default. When the decision is made to boot a BIOS-based operating system, a special EFI application is loaded from the firmware ROM to kick off the BIOS boot process. When the user chooses Windows as the default operating system in the “Startup Disk” pane, the NVRAM variables are actually set to point at this special loader, plus a parameter that tells it which device to boot from. - http://refit.sourceforge.net/info/boot_process.html If that is an unknown problem, maybe there's some memory offset somewhere that I can try to adjust? thanks, Steffen

2 1

Genode Operating System Framework
by Christian Helmuth 08 Aug '08

08 Aug '08

The initial version of the Genode OS Framework is available for download from http://genode.org/download/latest-release. Genode is an operating-system architecture, which addresses the root of the complexity problem, which is the lack of organization and overly permissive security policies. By applying a strict organizational structure to all system components including classical operating-system services, Genode is able to dramatically reduce the critical system complexity. The targeted application domains include high-security computing, dependable systems, automotive applications, and mobile devices. Even though we mainly address specialized applications in the mid-term, we believe that the implemented mechanisms scale well towards the needs of a general-purpose operating system. The Genode OS Framework (http://genode.org) is the reference implementation of the architecture and developed as an open-source community effort coordinated by the original creators of the project. Genode is an offspring of the L4 community. Until spring 2008, it was conducted internally within the TU Dresden OS research group. The foundation of Genode Labs by the original creators of Genode marks the transition of Genode to a community project. At present, the implementation is not complete but it is a solid starting point for a community effort. The initial version contains all base components, services, and device drivers to execute a provided interactive demonstration scenario on both Linux via libSDL and bare PC hardware via the L4/Fiasco microkernel and our custom device drivers. Release notes for the version 8.08 ---------------------------------- The release 8.08 is the first official version of the Genode OS Framework. It contains the following components: * The base framework including all libraries and interfaces as described in the Base API documentation * The 32bit Linux version of the base framework, which is the recommended platform for testing and developing * The 32bit L4/Fiasco version of the base framework * Drivers * Frame buffer driver for VESA and libSDL * PS/2 keyboard and mouse driver * PCI driver * Timer driver * Services and applications * Nitpicker GUI server * Scout tutorial browser * Graphical application launcher * XML-configurable init process * Complete demonstration scenario with graphical test applications such as liquid frame buffer, testnit, and nitlog. * Ported libraries * libz * libpng Regards -- Christian Helmuth Genode Labs http://www.genode-labs.com/ · http://genode.org/

1 0

Genode Operating System Framework
by Christian Helmuth 08 Aug '08

08 Aug '08

1 0

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 August 2008