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