headers
Saya Sheng (盛淑蕙 | 6 Jun 10:13
Picon

Driving audio card

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
Permalink | Reply | 2 comments |
headers
Michael Roitzsch | 6 Jun 16:49
Picon
Favicon

Re: Driving audio card

Hi,

> 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?

There is a document from a student undergraduate thesis about a sound  
driver port to L4 available here:
http://os.inf.tu-dresden.de/papers_ps/mueller-beleg.pdf

It's a bit dated and with today's DDE, you would probably do some  
things differently. Unfortunately, there is no driver porting guide  
for DDE available that I know of.

Michael
Permalink | Reply | 0 comments |
headers
eric johnson | 7 Jun 05:57
Picon

timing right

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

_______________________________________________
l4-hackers mailing list
l4-hackers <at> os.inf.tu-dresden.de
http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
Permalink | Reply | 1 comment |
headers
Martin Pohlack | 7 Jun 20:00
Picon
Favicon
Gravatar

Re: timing right

Hi Eric,

eric johnson wrote:
> 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.

If you seriously want to prevent system calls you have three options:

 - Use the time stamp counter of your machine (if it has one, you didn't
   specify your hardware).  Usual problems are, frequency stability of
   you do dynamic frequency scaling and synchronicity on MP.  TSC has a
   very low overhead.

 - Your program could be allowed hardware access to a timer device, such
   as the HPET and drive it.

 - You have an external clock server which provides the current time in
   a shared memory page.  This could be a userland program or the
   kernel.  In both cases, the timer interrupt would have to be at least
   1kHz for you required resolution.

Cheers,
Martin
Permalink | Reply | 0 comments |
headers
Bjoern Doebel | 6 Jun 17:54

RE: Driving audio card

Hi Sheng,

> 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?

Generally, the approach to get any driver running with the DDE 
works as follows (note, when I speak of DDE examples, I mean the 
ones in l4/pkg/dde as well as larger examples such as l4/pkg/ore):

1) Start a new L4 application consisting of a main() function
   calling the DDE initialization routines. There are several
   ones depending on which DDE subsystems you want to use
   (timers, memory, pci, ...). Please consult the DDE examples
   for that.

2) After calling the init functions, call l4dde26_do_initcalls().
   This will execute all the functions Linux functions marked as
   *_initcall(), such as the init function of your driver.

3) Compile your application (consisting of your main function and
   the driver you want to use) and link it with the DDE libraries
   as you can see from the DDE examples.

4) If your type of device is already supported by the DDE (such
   as network, block and TPM devices), then this should give you
   a working executable which you then just boot and there goes
   your driver. Proceed to step 6 in this case.

5) If your type of device is not yet supported, which will 
   be the  case for sound devices, then you will encounter
   potentially lots of linker errors in step 3. In this case
   * Find out whether the missing function is necessary. If
     you can get away without it, then implement it as an
     empty function returning a default good value.
   * If the function does something necessary:
     * Check if you can reuse the implementation from the
       Linux kernel. This is the case for functions that
       use default Linux features that are provided by the
       DDE, such as kmalloc(), request_region() etc.
     * In some cases reusing things from Linux will result
       in too much unnecessary Linux code ending up in your
       application or it might prove too hard to get all of
       it compile. If this occurs, consider reimplementing
       the feature to the extent needed by your application.

   Note, that step 5) is the real hard part and it often takes
   a lot of time to understand which code you can copy from
   Linux and which one you should replace with code written
   by yourself.

   If everything compiles, proceed to step 6.

6) If the Linux part of your driver compiles and starting the
   application boots and initializes the driver, it is time to
   add some L4 glue code, so that external applications can
   use your driver.

7) Have fun with your driver server.

After gaining some experience with extending DDE, you will be
able to identify which pieces of your newly written code are
only needed for your specific application and which ones should
be provided for future device drivers, too. The latter should
then be incorporated into a DDE subsystem (e.g., a library in
the DDE package), but I recommend, you don't worry about this
at the current point.

Bjoern
Permalink | Reply | 0 comments |
headers
Hendrik Tews | 11 Jun 15:19
Picon
Favicon

CFP: JAR Special Issue On Operating Systems Verification

[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
Permalink | Reply | 0 comments |
headers
Stefan Kögel | 13 Jun 13:22
Picon
Picon

Compiling L4 with a different Fiasco Config

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
Permalink | Reply | 2 comments |
headers
Bjoern Doebel | 13 Jun 14:20

RE: Compiling L4 with a different Fiasco Config

Hi Stefan,

> Now my questions:
> Is it possible to build L4 using a different Fiasco Config? 
> If  so, how?

When by L4 you mean building the L4 packages in l4/pkg - sure.
They are in no way elated to the Fiasco build config. (Note, that
the L4 build directory is even different from the Fiasco one.)
You can change the L4 config easily by going to your L4 build
Directory and running "make config".

> Is it possible to compile L4 hello module without building the
> kernel and use this together with the separately build kernel? 
> If so, how?

Sure.

$> make O=<path_to_l4_build_dir>/pkg/hello

Will do the trick as well as manually going to 
<path_to_l4_build_dir>/pkg/hello and running make.

Bjoern
Permalink | Reply | 1 comment |
headers
Bjoern Doebel | 13 Jun 15:07

RE: Compiling L4 with a different Fiasco Config

Ups...

> $> make O=<path_to_l4_build_dir>/pkg/hello

Should be: make O=<builddir> -C l4/pkg/hello

Bjoern
Permalink | Reply | 0 comments |
headers
Bjoern Doebel | 17 Jun 10:48

RE: ore problems

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
Permalink | Reply | 0 comments |

Gmane