I actually think I may have figured it out by poking around. I see that you can define the test you would like to run as a regex in menuconfig. So I think if you create a custom test and define it using similar syntax as the other tests it should be able to be pulled up from the menuconfig. For example

DEFINE_TEST(CUSTOM001, "Custom test seL4_Send + seL4_Wait Benchmark", custom_test_send_wait)

where you can define your own function called custom_test_send_wait. Then for the REGEX in menuconfig under seL4 Libraries-->sel4test printing library-->Tests to perform you can just choose to run "CUSTOM" as your regex and it should run all of your custom tests.

From there, your test gets built into the image and you can run it like you normally would.

Is this correct?

Matthew Scaperoth

Jr. Programmer Analyst

The George Washington University

Academic Technologies

Tel: 202-994-6907

On Fri, Sep 19, 2014 at 5:26 PM, Matthew Scaperoth <mscapero@gwu.edu> wrote:

Hello All,

First I wanted to say thank you for this dev forum. The more I learn about SeL4 the more I am amazed with how well it is written.

I am working on a 32-bit Ubuntu 14.04 and I would like to run your individual test suites in the sel4-manifest with a 32-bit build. Specifically some of the tests from the https://github.com/seL4/sel4test/tree/master/apps/sel4test-tests/src directory. For example, I'd like to alter the code a little bit and run qemu to output cycle time for IPC or memory mapping. So potentially I would boot up the image, the files would load and I would get an output saying "Intra-as IPC 151 cycles" or something along those lines after the test was automatically run.

I was reading through the files and noticed that the main.c accepts arguments to say which test I'd like to run using the find_test() method with the argv passed in. I am now trying to find a way to use the main.c file in sel4test-tests to achieve the build I am after.

I also noticed that a .bin file and a another file in stage/ia32/pc99/bin/sel4test-tests are generated when you run the first top-level make after the configuration. So I have tried booting the sel4test-tests file in qemu with

qemu-system-i386 -m 512 -serial stdio -kernel images/kernel-ia32-pc99 -initrd stage/ia32/pc99/bin/sel4test-tests

but nothing happens. My thought process was that it could replace the driver image for ia32 pc99 (sel4test-driver-image-ia32-pc99) .

So I am missing a piece here (or pieces?). I am not sure if there is a Makefile that I can alter to include only a specific test, or if it's something else entirely. I'd be happy to clarify what I aim to achieve or details about my system if necessary.

Also, I am really enjoying the code that generates these tests in the main.c file mentioned earlier. I feel like it is a much more graceful solution to running these tests than other l4 systems I've worked with.

Thanks again,

Matt