l4-hackers August 2012

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

21 participants
27 discussions

Call for Papers: System Software Verification Conference (SSV 2012)
by Toby Murray 17 Aug '12

17 Aug '12

[Note: Submission Deadline is 19 September 2012] 7th Systems Software Verification Conference (SSV 2012) November 28--30, 2012 Sydney, Australia http://www.ssv-conference.org/ *Scope 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 that are invalidated by complex embedded systems 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 with the goal of finding real, applicable solutions. By “real” we mean problems such as time-to-market or reliability that the industry is facing. 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. In this workshop we will discuss software analysis and development techniques and tools; this forum will 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 restricted to: • Model checking • Automated and interactive theorem proving • Static analysis • Automated testing • Model-driven development • Embedded systems development • Programming languages • Verifying compilers • Software certification • Software tools • Experience reports *Submissions Submissions must be made electronically through the EasyChair system (https://www.easychair.org/conferences/?conf=ssv2012) until September 19th, 2012. Papers should be up to 15 pages in pdf format and formatted in EPTCS style. 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. *Publication The proceedings will be published with EPTCS (http://eptcs.org). *Important Dates Abstract Submission: September 14, 2012 Paper Submission: September 19, 2012 Notification: October 19, 2012 Conference: November 28–30, 2012 *Location The workshop will be held in Sydney, Australia at NICTA NRL Laboratory. *Organization Organizing Committee and PC Chairs • F. Cassez, NICTA, Sydney, Australia • R. Huuck, NICTA and UNSW, Sydney, Australia • G. Klein, NICTA and UNSW, Sydney, Australia • B. Schlich, ABB Corporate Research, Ladenburg, Germany Program Committee • Cyrille Artho, AIST, RISEC, Japan • Stefan Berghofer, Secunet, Germany • Frédéric Boniol, ONERA, France • Alessandro Coglio, Kestrel, USA • Joe Hurd, Intel, USA • Stefan Kowalewski, RWTH Aachen University, Germany • Thomas Kropf, Robert Bosch GmbH & U. of Tübingen, Germany • Kim G. Larsen, CISS, Aalborg University, Denmark • Toby Murray, NICTA, Sydney, Australia • Jan Peleska, Verified Systems International GmbH and University of Bremen, Germany • John Regehr, University of Utah, USA • Natarajan Shankar, SRI, USA • Zhong Shao, Yale, USA • Konrad Slind, Rockwell Collins, USA • Jun Sun, National University of Singapore, Singapore The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

L4Re/Fiasco IO memory map.
by Daniel Waddington 15 Aug '12

15 Aug '12

Hi, I have a SATA controller card. When I try to map in the IO memory from the PCI BAR regs an NMI is generated - and the mapping doesn't seemed to have worked (fully?). What might generate this NMI? The same platform/device works fine in Linux. Thanks Daniel

2 2

Fiasco-for ppc32
by Vishal Gupta 15 Aug '12

15 Aug '12

Hello!! I am using fiasco-2012081219 and i want to make fiasco image file for ppc32-[p2041]. but i read Makefiles there is one makeconf.ppc32 but i am not able to make buildir for ppc32. please send me some options. Thanks & Regards, vishal linux

2 1

NUL_problem
by oleg 15 Aug '12

15 Aug '12

2 1

Re: NUL_problem
by oleg 14 Aug '12

14 Aug '12

1 0

NUL_problem
by oleg 14 Aug '12

14 Aug '12

2 1

Problem Booting x86_64 kernel in qemu
by Markus Pfeiffer 12 Aug '12

12 Aug '12

Dear all, I tried building the Fiasco kernel (x86_64, from svn) together with the hello demo inside a qemu as it is shown on the website under "Getting started". Unfortunately the kernel traps while booting (Unexpected trap while booting Fiasco). The trap number seems to be invalid (-8029759185026510704). Any pointers towards where to look for a fix? Cheers Markus -- Markus Pfeiffer, University of St Andrews email: markus.pfeiffer(a)morphism.de | xmpp: markus.pfeiffer(a)jabber.morphism.de

3 5

Questions about Shared Memory Area and IRQ
by ZhangEditing 10 Aug '12

10 Aug '12

Hello. I have been trying to use the shared memory library and have learnt that it uses signals to notify parties that participate in communication. When I looked into the library code, I found that it implements signals with IRQs. However, I could not figure out which IRQ the library use. I have noticed that l4shmc_add_signal creates an IRQ object, but no IRQ number is used. The only thing that appear like an IRQ number is the second argument of l4_irq_attach, which is called by l4shmc_attach_signal_to. But I haven't found any clue about the meaning of the argument. Would you please tell me what the second argument of l4_irq_attach is? I have also noticed that l4shmc_add_signal registered an IRQ object to the namespace of the shared memory area. Does this mean that the IRQs used to implement signals are guaranteed not to conflict with any IRQ used by the hardware or any other software IRQ, regardless of the ORDER in which they are created? Thank you in advance!

2 1

i.MX53QSB port + IOmem access
by Andy Wagner 08 Aug '12

08 Aug '12

PT checks are probably adequate <those should not be modifiable from usr> but any user-context that can map the pages gets access. IO and the io configuration enforce resource assignment policy here and granularity is adequately fine to segregate resources via .cfg file entries. Agreed that trapping slows down IO process but could make porting more transparent. Tradeoff is the amount of work required to manage within the BSP and have that correspond to IO <or wherever the handler would be most suitable>. There is work in either case and it is probably more easily achieved by having the bits cleared at boot or init and minimizing changes required to linux. TZ would be still more entertaining to support. thanks, Andy On Tue Aug 07, 2012 at 13:41:56 -0700, Andy Wagner wrote: > Clearing sp for opacr21 allows the access to complete without fault. > It would be very nice if the sp could remain enabled and have the > fault handler trap to supervisor so that hardware enforcement can > be leveraged as well as software resource allocation check. > > Since mprot and opacr assignments are SoC specific this > would have to be implemented as part of the BSP framework perhaps > over complicating the issue. Preference is to keep things simple > and probably leave in the underlying linux, where the drivers > are located <executing code localization>, without making fiasco > or l4 more aware of the hardware than necessary. Instruction > emulation could be a bit messy due to differing memory maps > between faulting and exception handling contexts. Well, the hardware enforcement used is the page table which makes sure that a client can only access those devices it is given access to. Which benefit does a user/supervisor access check add here? Trapping any access to io memory would also slow down access to devices, plus someone would need to check if the access is valid, which would not be the kernel. Adam -- Adam adam at os.inf.tu-dresden.de Lackorzynski http://os.inf.tu-dresden.de/~adam/

2 1

i.MX53QSB port + IOmem access
by Andy Wagner 07 Aug '12

07 Aug '12

Clearing sp for opacr21 allows the access to complete without fault. It would be very nice if the sp could remain enabled and have the fault handler trap to supervisor so that hardware enforcement can be leveraged as well as software resource allocation check. Since mprot and opacr assignments are SoC specific this would have to be implemented as part of the BSP framework perhaps over complicating the issue. Preference is to keep things simple and probably leave in the underlying linux, where the drivers are located <executing code localization>, without making fiasco or l4 more aware of the hardware than necessary. Instruction emulation could be a bit messy due to differing memory maps between faulting and exception handling contexts. Most simply, the sp bits can be cleared by a call into the bsp and leave the boot loader alone. Many thanks for your help and insight. Work now proceeds to migrate the drivers. thanks & best regards, Andy >I'd guess that access from user-mode is the 'problem' here. Could you >check the setting of AIPSTZ_OPACR21 and possibly adapt accordingly? Adam -- Adam adam at os.inf.tu-dresden.de Lackorzynski http://os.inf.tu-dresden.de/~adam/ Previous message: i.MX53QSB port + IOmem access Next message: Ethernet device Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] More information about the l4-hackers mailing list

2 1

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 2012