Hi Jack,
Unfortunately, the graph-to-graph WCET tools have not received much attention since the papers you mention, and are currently somewhat bitrotted. The graph-to-graph code lags behind the rest of graph-refine, and I believe that leads to a number of incompatibilities. Additionally, kernel developments in recent years have exposed some bugs in the graph-refine stack analysis module, as you've discovered. We used a simpler stack analysis in recent RISC-V binary verification work, but due to resource constraints, have not yet merged that work with the ARM tools. You might be able to find the right combination of older versions of all the components (including the kernel) to reproduce the result in the WCET paper, but I'm afraid even that might be challenging. If you want to try, I would suggest starting with the 3.2.0 manifest:
https://github.com/seL4/verification-manifest/blob/master/3.2.0.xml
You might need a Debian-ish OS environment from around that time, and you might also need to use a Linux host rather than WSL.
Best wishes, Matt
On Fri, 5 Nov 2021 at 16:08, Jack Chen via Devel devel@sel4.systems wrote:
Greetings
I'm recently conducting research on WCET analysis of seL4-based systems. Graph-to-graph seems to be a good starting point. However the toolset doesn't seem to be fully working in my setup.
My setup: x86, 16GB RAM, Windows10 WSL Ubuntu 20.04 Goal: To replicate the static WCET analysis decribed in the paper [Sewell et al. 2016], using graph-to-graph and graph-refine/seL4-example build.
Steps taken:
- repo setup with "verification-manifest"
- fetched 2 versions: defalut (10/21/2021), and 12.1.0
- followed READMEs: preparing isabelle, HOL4, standalone c-parser, and
their dependencies (according to graph-refine/seL4-example/readme)
- L4V_ARCH=ARM
- [./run_tests] in l4v
- [make tar] in graph-refine/seL4-example
- [python graph-refine.py <targetdir> all]
Results (default version) :
- seL4-example [make tar]: all things seem normal except
- Graph spec failed in _start for pos 0xe0000008.
- Graph spec failed in _start for pos 0xe0000008.
- l4v run_tests: 43/51 passed
- HaskellKernel STUCK (probably due to internet access issue for my
region), CParserTest Failed
- graph-refine: KeyError: 'kernel_devices'
- This one is interesting. The seL4 code fetched with this "default"
manifest contains a "kernel_device_frames", which I think is called "kernel_devices" in previous versions of seL4 kernel code. In kernel.elf.rodata they seem to be associated with the same block of assembly code.
Results (12.1.0):
- seL4-example [make tar]: same as default, graph spec fails
- l4v run_tests: 29/51 passed
- HaskellKernel STUCK as usual, CParserTest Failed, CBaseRefine
TIMEOUT, AInvs TIMEOUT, a lot others SKIPPED due to dependency
- graph-refine: There's no KeyError now because "kernel_devices" is
present in this version of seL4 code, but I got this instead: ###======================================= ### Doing stack analysis for 'cap_get_capPtr'. (48 of 575) ### Traceback (most recent call last): ### File "graph-refine.py", line 31, in <module> ### args = target_objects.load_target_args () ### ... ### ... ### File "stack_logic.py", line 223, in get_ptr_offsets ### assert not fail_early, (v, ptr) ### AssertionError: ((3758178040, Expr ('Var', Type ('Word', 32), name = 'r13')), 'r13_after_3758178040_3758178040=i+0') ###=====================================
Here are my questions:
- Are these issues common, or is my setup & installations just wrong? Any
way to resolve these issues? (big questions, and hence the long email, and hence I'm here asking the experts)
- Is solver.py currently broken? (dug up some clues in
seL4-example/Makefile)
- for graph-to-graph, phantom_preempt.py seems required in the
convert_loop_bounds step: Any guide on how to write this file, e.g. format, content?
- To replicate the WCET experiment in the 2016 paper, should I download
the specific version of the verification repo of that time?
- static vs. measurement-based WCET analysis: Going forward, on more
advanced ARM archs (e.g., Armv8), is static WCET analysis still worth it (or even feasible)? Is hybrid approach the way to go? Is the TS team still working on WCET tools for seL4 on ARM systems? (saw papers from the team many years ago discussing the combination of static cache analysis and probabilistic measurement)
Regards, Jack _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems