Graph-refine Toolset Usability Issues (for WCET analysis)
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
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
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
Hi Matt, Thanks for the quick reply and advice. I was planning on trying 3.1.0 this arvo :D Is WCET still a research focus of the team? RISC-V aside, for Armv7 v8 (and x64), measurement-based is probably the way forward IMHO. Wish there's more publications on measurement-based WCET of seL4. If the team & the community would like to share insights and discuss this matter, I'd be happy to stick around and ask more questions. Regards, Jack
Hi Jack,
On 5 Nov 2021, at 22:53, Jack Chen via Devel
Is WCET still a research focus of the team? RISC-V aside, for Armv7 v8 (and x64), measurement-based is probably the way forward IMHO. Wish there's more publications on measurement-based WCET of seL4. If the team & the community would like to share insights and discuss this matter, I'd be happy to stick around and ask more questions.
As Matt said, the WCET toolchain is bitrotted. It was used for ARMv6 cores, but Arm stopped providing instruction latency information for their A cores, so WCET analysis on those is no longer possible, which basically means these Arm A cores are no longer usable for hard real-time. Measurement-based WCET analysis is unsound, of course, and not suitable for safety-critical use. RISC-V is different, in particular for the open-source implementations, some of which made it into silicon, with more to come. We’d love to revive the WCET analysis for RISC-V, basing it off the great work Matt & Co did on the translation validation toolchain, which is a core part of the high-assurance WCET evaluation process. It’ll require a fair amount of work and I’m waiting for someone to fund it. I’m sure it’ll happen eventually, given that seL4 still seems to be the only protected-mode RTOS that has undergone a sound WCET analysis on a pipelined processor. Gernot
participants (3)
-
Gernot Heiser -
Jack Chen -
Matthew Brecknell