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=… [View More]

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 /… [View More]

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 … [View More]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 [View Less]

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 … [View More]

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 … [View More]

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 … [View More]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/ [View Less]

1 0

Genode Operating System Framework
by Christian Helmuth 08 Aug '08

08 Aug '08

1 0

2025

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