- l4-hackers - example.com Site

CFP: SSV 2011 - Workshop on Systems Software Verification [deadline extended]
by Hendrik Tews 17 May '11

17 May '11

[The deadline for abstract submissions has just been extended to May 29th. My apologies if you receive multiple copies of this CfP -- Hendrik Tews] ============================================================================= 6th International Workshop on Systems Software Verification (SSV 2011) Real Software, Real Problems, Real Solutions August 26-27 2011, Nijmegen, The Netherlands https://es.fbk.eu/events/ssv2011 Industrial-strength software analysis and verification has advanced in recent years through the introduction of model checking, automated and interactive theorem proving, and static analysis techniques as well as correctness by design, correctness by contract, and model-driven development. 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. The aim of this workshop is to bring together researchers and developers from both academia and industry, who are facing real software and real problems to find real, applicable solutions. By "real" we mean problems such as time-to-market or reliability that the industry is facing and is trying to fix in software that is deployed in the market place. 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. This forum will discuss software analysis/development techniques and tools; it will also serve as a platform to discuss open problems and future challenges in dealing with existing and upcoming systems level code. Topics include (but are not limited to): * model checking * automated and interactive theorem proving * static analysis * model-driven development * embedded systems development * automated testing * programming languages * verifying compilers * software certification * software tools * experience reports Submissions must be made electronically through the EasyChair system [1] until May 29 2011, 23:59h Samoan time. Papers should be up to 15 pages in pdf format and formatted in LNCS style [2]. Additional details may be included in a clearly marked appendix, which will be read at the discretion of the program committee. All will be subject to peer review under normal conference standards. Experience reports and papers on work in progress are welcome as long as there is a clear contribution. Submissions which are based or discuss a non-trivial piece of software are required to make all those non-standard software parts available, which a referee may need, in order to check the claims of the submission. Submitted papers must not have previously appeared in a journal or conference with published proceedings and must not be concurrently submitted to any other peer-reviewed workshop, symposium, conference or archival journal. Any partial overlap with any such published or concurrently submitted paper must be clearly indicated. The workshop proceedings are planned to be published in the form of post-proceedings in the Springer series Lecture Notes in Computer Science (LNCS). Important dates May 29 2011 Abstract Registration Deadline June 03 2011 Paper submission deadline June 30 2011 Notification of accepted papers July 15 2011 Final version August 26-27 2011 Workshop The workshop is organized as a two-day workshop (August 26-27 2011). Location The workshop will be held in Nijmegen, The Netherlands in conjunction with the 2nd International Conference on Interactive Theorem Proving (ITP 2011). Program Chair Jörg Brauer (RWTH Aachen University, Germany) Marco Roveri (FBK-irst, Italy) Hendrik Tews (TU Dresden, Germany) Steering Committee Ralf Huuck (NICTA, Australia) Gerwin Klein (NICTA, Australia) Bastian Schlich (ABB Corporate Research, Germany) Program Committee Dirk Beyer (University of Passau, Germany) Jörg Brauer (RWTH Aachen University, Germany) Adam Chlipala (Harvard, USA) Ansgar Fehnker (NICTA, Australia) Alexey Gotsman (IMDEA, Spain) Chris Hawblitzel (Microsoft Research, USA) Andy King (University of Kent, UK) Stefan Kowalewski (RWTH Aachen University, Germany) Thomas Kropf (Bosch, Germany) Kim G. Larsen (Aalborg University, Denmark) Wolfgang Reif (University of Augsburg, Germany) Marco Roveri (FBK-irst, Italy) Axel Simon (TU Munich, Germany) Nishant Sinha (NEC Labs, USA) Hendrik Tews (TU Dresden, Germany) Michael Whalen (UMSEC -- University of Minnesota, USA) Kwangkeun Yi (Seoul National University, Korea) Invited Speakers Following a tradition established over the past iterations of SSV, this years workshop will feature at least two keynote talks. The invited speakers will be announced soon. [1] http://www.easychair.org/conferences/?conf=ssv2011 [2] http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0

1 0

L4 on ARM: cache coherency and virtual address space
by Michal Schulz 11 May '11

11 May '11

Hello, I am implementing an USB stack for ARM machine maintained by the L4 microkernel. It works quite well at the moment - USB hubs and HID devices are working properly. However, there are few open issues there: 1. Since ARM machine I use does not provide cache snooping, i.e. I have to flush/invalidate the caches manually, I've attempted to use the l4_cache_dma_coherent function. It did worked to some degree, but it flushed/invalidated only *some* lines of cache within requested region, instead of *all* lines of cache. Since I've failed to trace the bug, I've extended sigma0 with new functionality - ability to map uncached memory. I still don't like my hack though and I would like to find an official way to either change the attributes (from cached to uncached) of given page, or have fully working l4_cache_dma_coherent. 2. The USB stack is a multithreaded app where I would like to have different servers (e.g. server for HID input events, server for mass storage devices). Unfortunately a server seemed to work only when started from the main thread. Why is it so? Was that my fault? 3. When the mass storage server receives either read or write call, it needs to map caller's memory in uncached manner. Moreover, USB stack needs *physical* address of the caller's buffer. How can I find that out? with best regards, Michal. -- Michal Schulz

2 3

Rename compund to compound
by Christian Ehrhardt 04 May '11

04 May '11

Hi, in the past weeks I've been reading through the fiasco kernel code. This is the start of a series of patches that clean up stuff or fix bugs that I think I found. Comments appreciated. The first patch renames a method called compund to compound, more important patches follow :-) regards Christian diff --git a/src/kernel/fiasco/src/abi/l4_msg_item.cpp b/src/kernel/fiasco/src/abi/l4_msg_item.cpp index bbb92ef..1155a5f 100644 --- a/src/kernel/fiasco/src/abi/l4_msg_item.cpp +++ b/src/kernel/fiasco/src/abi/l4_msg_item.cpp @@ -16,7 +16,7 @@ public: }; explicit L4_msg_item(Mword raw) : _raw(raw) {} - Mword compund() const { return _raw & 1; } + Mword compound() const { return _raw & 1; } Type type() const { return Type(_raw & 8); } bool is_void() const { return _raw == 0; } bool is_small_obj() const { return _raw & 2; } diff --git a/src/kernel/fiasco/src/kern/thread-ipc.cpp b/src/kernel/fiasco/src/kern/thread-ipc.cpp index f8e1995..3288b2a 100644 --- a/src/kernel/fiasco/src/kern/thread-ipc.cpp +++ b/src/kernel/fiasco/src/kern/thread-ipc.cpp @@ -948,7 +948,7 @@ Thread::transfer_msg_items(L4_msg_tag const &tag, Thread* snd, Utcb *snd_utcb, --items; - if (!item->b.compund()) + if (!item->b.compound()) buf_iter->next(); }

2 9

I have a problem when I built the L4Re environment
by 王彬彬 04 May '11

04 May '11

> ==> Installing crti.o to local build-tree > ... Compiling crtn.o > initfini.c: Assembler messages: > initfini.c:29: Error: .size expression for _init does not evaluate to a > constant > initfini.c:29: Error: .size expression for _fini does not evaluate to a > constant > make[3]: *** [crtn.o] Error 1 > make[3]: Leaving directory > `/home/wegrzyn/Fiasco/L4re-build/pkg/ldscripts/OBJ-x86_core2' > make[2]: *** > [/home/wegrzyn/Fiasco/L4re-build/pkg/ldscripts/OBJ-x86_core2] Error 2 > make[2]: Leaving directory `/home/wegrzyn/Fiasco/src/l4/pkg/ldscripts' > make[1]: *** [ldscripts] Error 2 > make[1]: Leaving directory `/home/wegrzyn/Fiasco/src/l4/pkg' > make: *** [pkg] Error 2 Can anyone venture a guess what I need to correct? TYXL HFUT,China

2 1

64 bit support in L4Linux
by Stefan Kalkowski 03 May '11

03 May '11

Hi, I've a short question related to L4Linux for 'x86_64'. When looking at the L4-specific architecture-files, I got the impression that the 64-bit support from the x86 port got retained. But my attempts to enable 64-bit in L4Linux failed. (Setting environment variables, tweaking configuration, hacking Kconfig a bit...) Does that mean 64-bit isn't supported by now, or if it is, what is the recommended way to enable it? Any advice on approach is welcome. Thanks, Stefan

2 2

how i can determine utcb loaction in order to make thread
by Jason Philip 01 May '11

01 May '11

I am very puzzled, I can't seem to find utcb location in L4Ka::pistachio. One example do this: L4_ThreadId_t mylocalid = L4_MyLocalId (); utcb_base = *(L4_Word_t *) &mylocalid; utcb_base &= ~(L4_UtcbAreaSize (kip) - 1); where the current thread is initial thread (main), but i try this it do not work. Can someone suggest proper way to determine the utcb location so that I can create a new thread? Please

3 13

Ethernet on Beagleboard xM with Ankh+L4Linux ?
by Julien Heyman 22 Apr '11

22 Apr '11

Hello, I am trying to understand what it would take to have access to (physical) ethernet from L4Linux running on a Beagleboard xM. As far as I understood/read, I can either try to integrate the native ethernet driver in L4Linux, or rely on Ankh networking server. Since I am running two instances of L4Linux, I'd rather use the Ankh solution. >From what I see Ankh does not currently include an appropriate driver for the BB xM's ethernet chip. Is it doable to pick an existing ethernet driver for the BB xM from, say, the Angström linux distribution for Beagleboard, and integrate it to Ankh ? Assuming this is possible, do I understand correctly that I would then only have to enable the Ankh driver option in the L4Linux configuration, to get an ethernet access in L4Linux ? Regards, Julien

2 2

Assertion failed: 'prev_next' [ret=0xf000e9c8] (arm qemu realview pbx system)
by Siegfried Podesser 19 Apr '11

19 Apr '11

hello together, If I try to run the L4Linux or the hello example via a patched QEMU (with trustzone support) I get the following error message: ------------ ./qemu-system-arm -M vexpress-a9 -kernel /home/beresford/Work-Repositories/sepia/desastro/l4/build/images/bootstrap_hello.elf -initrd /home/beresford/Downloads/ramdisk-arm.rd -append "console=ttyAMA0 console=tty0 dhcp=on" -m 1024 -s -gdb tcp::5022 erster teilerfolg: Fiasco + L4 hüpfen zumindest mal an... ./qemu-system-arm -M vexpress-a9 -kernel /home/beresford/Work-Repositories/sepia/desastro/l4/build/images/bootstrap_L4linux_ARM.elf -initrd /home/beresford/Downloads/ramdisk-arm.rd -append "console=ttyAMA0 console=tty0 dhcp=off" -m 512 -smp 1 -gdb tcp::1234 -serial stdio bp147: attached 100e6000..100e6fff to TZDECPROT0[6] bp147: attached 100e4000..100e4fff to TZDECPROT0[4] L4 Bootstrapper Build: #3 Tue Apr 19 09:46:31 CEST 2011, 4.5.1 Scanning up to 256 MB RAM Memory size is 256MB (00000000 - 10000000) RAM: 0000000000000000 - 000000000fffffff: 262144kB Total RAM: 256MB mod09: 01500000-01800000: ramdisk-arm.rd mod08: 0124e000-014ff488: vmlinuz.arm mod07: 0124d000-0124d0bd: arm-rv.io mod06: 01162000-0124c7d4: io mod05: 01161000-01161189: l4lx.cfg mod04: 01105000-011601ac: ned mod03: 010e3000-01104488: l4re mod02: 010a5000-010e266c: moe mod01: 01093000-010a4304: sigma0 mod00: 01015000-01092a2c: fiasco Moving 10 modules to 1100000 with offset eb000 moving module 10 { 1500000-1800000 } -> { 15eb000-18eb000 } moving module 09 { 124e000-14ff488 } -> { 1339000-15ea488 } moving module 08 { 124d000-124d0bd } -> { 1338000-13380bd } moving module 07 { 1162000-124c7d4 } -> { 124d000-13377d4 } moving module 06 { 1161000-1161189 } -> { 124c000-124c189 } moving module 05 { 1105000-11601ac } -> { 11f0000-124b1ac } moving module 04 { 10e3000-1104488 } -> { 11ce000-11ef488 } moving module 03 { 10a5000-10e266c } -> { 1190000-11cd66c } moving module 02 { 1093000-10a4304 } -> { 117e000-118f304 } moving module 01 { 1015000-1092a2c } -> { 1100000-117da2c } Scanning fiasco Scanning sigma0 Scanning moe rom/l4lx.cfg Relocated mbi to [0x100f000-0x100f151] Loading fiasco Loading sigma0 Loading moe find kernel info page... found kernel info page at 0x2000 Regions of list regions [ 1000, 19ff] { a00} Kern fiasco [ 2000, 8cfff] { 8b000} Kern fiasco [ 90000, 9e193] { e194} Sigma0 sigma0 [ 140000, 18b48b] { 4b48c} Root moe [ 1000000, 10143eb] { 143ec} Boot bootstrap [ 100f000, 100f24e] { 24f} Root Multiboot info [ 11ce000, 18eafff] { 71d000} Root Modules Memory API Version: (87) experimental Sigma0 config ip:00090000 sp:01013044 Roottask config ip:00140088 sp:00000000 Starting kernel fiasco at 00001000 Realview System ID: Rev=1 HBI=190 Build=f Arch=5 FPGA=00 L2: ID=00000000 Type=00000000 L2 cache enabled Hello from Startup::stage2 Assertion failed: 'prev_next' [ret=0xf000e9c8] /home/beresford/Work-Repositories/sepia/desastro/kernel/fiasco/src/kern/buddy_alloc.cpp:23 at f000e834 --------------------------------- If I remove the assertion check it executes a little bit more and I get the following error: --------------------------------- ... Starting kernel fiasco at 00001000 Realview System ID: Rev=1 HBI=190 Build=f Arch=5 FPGA=00 L2: ID=00000000 Type=00000000 L2 cache enabled Hello from Startup::stage2 Per_cpu_data_alloc: (orig: 0xf007a628-0xf007b030) Initialize page table Number of IRQs available at this GIC: 32 Number of IRQs available at this GIC: 32 Vmem_alloc::init() Cache config: ON ID_PFR0: 00001031 ID_PFR1: 00000011 ID_DFR0: 00000000 ID_AFR0: 00000000 ID_MMFR0: 00100103 ID_MMFR1: 20000000 ID_MMFR2: 01230000 ID_MMFR3: 00002111 Panic: UTCB pointer page allocation failure Press any key to reboot. ---------------------------------- Through the mailing list i found your posting from Thu, 25 Sep 2008 10:57:29 where you have suggested to check the RAM_SIZE_MB in the l4 config file. I've checked it and it is set to 256MB as my qemu is set as well. I tried it further with 512MB and 1GB but it changes nothing. Do you have any further ideas ? kind regards, siegfried

2 1

L4Linux (arm) - change CPU speed
by Siegfried Podesser 12 Apr '11

12 Apr '11

Hello, is there a way or an example source code to change the CPU speed? I'm using the original Fiasco kernal together with the given L4Linux for arm platforms. Thank you for your help! kind regards, siegfried

2 1

How to add more NIC drivers for ankh?
by Alexey Aizatullin 10 Apr '11

10 Apr '11

Hello, Could you please explain what steps should I do to add drivers for other ethernet adapters for ankh? -- --------------------------------------- Alexey Aizatullin

2 1