NameDateSize

..09-Apr-202036

__init__.pyH A D09-Apr-202099

addr_utils.pyH A D09-Apr-2020779

auto_infea.pyH A D09-Apr-20204.8 KiB

bench.pyH A D09-Apr-20204.7 KiB

borg.pyH A D09-Apr-2020513

call_graph_utils.pyH A D09-Apr-20204 KiB

chronos/H09-Apr-20205

conflict.pyH A D09-Apr-202019.5 KiB

convert_loop_bounds.pyH A D09-Apr-20204.5 KiB

cplex.pyH A D09-Apr-20205.6 KiB

dot_utils.pyH A D09-Apr-20204.4 KiB

elf_correlate.pyH A D09-Apr-202019.4 KiB

elf_file.pyH A D09-Apr-20203.7 KiB

elf_parser.pyH A D09-Apr-20203.9 KiB

graph_refine/H09-Apr-202036

graph_to_graph.pyH A D09-Apr-20203.5 KiB

imm_utils.pyH A D09-Apr-20207.3 KiB

loop_counts.pyH A D09-Apr-20204.1 KiB

pydot.pyH A D09-Apr-202056.3 KiB

README.mdH A D09-Apr-20208.5 KiB

reconstruct.pyH A D09-Apr-202015 KiB

tests.xmlH A D09-Apr-2020455

wcet_scripts/H09-Apr-20205

README.md

1<!--
2     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4     SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7The Graph-To-Graph WCET Toolset
8====================
9Building on the Data 61 Graph Refinement toolset, this tool estimates the Worst Case Execution Time of conforming C code.
10
11Dependencies
12----------
13You will need an operational setup of the graph-refine toolset, follow the instructions on:
14https://github.com/seL4-projects/graph-refine
15
16We have tested SONOLAR
17(http://www.informatik.uni-bremen.de/agbs/florian/sonolar/) and
18CVC4(http://cvc4.cs.nyu.edu/downloads/) and for this setup. The specific
19versions we used were SONOLAR-2014-12-04, CVC4-1.4.
20
21Refer to graph-refine/seL4-example/README.md for details.
22We have tested with this following .solverlist setup:
23
24---
25
26SONOLAR: offline : (path to sonolar dir/bin/sonolar) --input-format=smtlib2
27CVC4: online: (path to the cvc4-1.4 binary) --incremental --lang smt -tlimit=5000
28
29---
30
31*NUS Chronos*
32
33The toolchain expects our modified version of the NUS Chronos WCET toolchain (http://www.comp.nus.edu.sg/~rpembed/chronos/) to live at (verification)/chronos4.2/
34Which is avaliable via:
35
36`git clone https://github.com/seL4-projects/chronos4.2`
37`cd chronos4.2`
38`make`
39
40*IBM Cplex 12.6.0.0*
41
42CPLEX can be obtained, free of charge, under the IBM Academic Initiative for qualifying academics.
43Use the exact version, 12.6.2 in particualr is incompatible with graph\_to\_graph.
44
45A JRE bugs may crashes the launcher for any but extremely short prompt name, you can work around it with:
46`PS1= ./cplex_studio126.linux-x86-64.bin`
47
48Then add cplex to your path.
49
50Setting up graph-refine
51---------
52The graph-to-graph directory needs to contain a symbolic link named graph\_refine to the top level directory so it can import its modules:
53
54    `ln --symbolic ../ graph_refine`
55
56    Your setup should look like this:
57    verification/
58        chronos4.2
59        graph-refine
60            __init__.py (blank file)
61            .solverlist
62            graph_to_graph/
63                graph_refine (symbolic link to parent directory)
64
65Using the toolset to estimate WCET
66--------
67To estimate the WCET of a target with dummy loopheads:
68
69Firstly generate the dummy loop counts with
70
71`python graph_to_graph.py targetDirectory entryFunction --l`
72
73this generates loop\_counts.py under the target directory with dummy loop counts.
74
75then invoke
76
77`python graph_to_graph.py targetDirectory entryFunction --L`
78to generate an ILP problem with the loop counts in targetDirectory/loop\_counts.pyand solve it with chronos.
79
80The toolset can also automatically determine loop bounds, to do this firstly generate the loopheads (and dummy loop bounds) with the --l flag, then execute:
81
82`python convert_loop_bounds.py targetDirectory`
83
84to automatically determine all loop bounds. Note this can take hours depending on the target. The derived results may be manually overwritten by editing loop\_counts.py
85
86Finally use the automatically deduced loopbounds to estimate the WCET with:
87
88`python graph_to_graph.py targetDirectory entryFunction --L`
89
90The resulting estimated WCET is only usable if the loop\_counts.py file contains no dummy entry. If it does and the user knows the loop bounds, they can be manually annotatedby modifying the loop\_counts.py file.
91
92Infeasible paths elimination
93--------
94
95Firstly, we strip the footer off the .ilp file with automatically annotated loop bounds that we got when we ran graph\_to\_graphy.py with the --L flag.
96
97`python cplex.py targetDirectory/handleSyscall.imm.ilp --f `
98
99We can then instructs conflict.py to produce the first round of candidate infeasible paths with blank conflict files. conflicty.py accepts two conflict file so that a manual file can be used in addition to an automatically produced one.
100'python conflict.py targetDirectory/handleSyscall.imm.map blank\_file blank\_file targetDirectory/handleSyscall.imm'
101
102Using the toolset on seL4
103--------
104You can refer to sel4.systems on how to get a cross compiler (required by graph\_refine).
105cd into the seL4-example directory and build it (see graph-refine for instructions).
106
107seL4 contains loops that are only bounded by preemption points, and the
108apparatus cannot determine the bounds for those loops. Thus the loop\_counts.py
109file (under the target directory) will contains dummy loop bounds. The
110preemption annotations, which is part of the infeaisble paths elimination
111process will resolve them properly. This means when we invoke
112graph\_to\_graph.py Cplex will return a unrealistically large number, that's
113expected. All we need from it is the .ilp file.
114
115Using handleSyscall as the entry function:
116
1171. Generate the loop bounds file with dummy loop counts
118    `python graph_to_graph.py ../seL4-example handleSyscall --l`
1192. Automatically deduce the loop bounds with
120    `python convert_loop_bounds.py seL4-exapmle `
1213. Generate the ILP file with theese automatically derived loop bounds, disregard the resulting WCET, because the loop bounds file contain
122    `python graph_to_graph.py ../seL4-example handleSyscall --L`
1234. Strip the ilp file of its footer
124    `python cplex.py ../seL4-example/handleSyscall.imm.ilp --f`
1255. Invoke conflict.py to produce an annotated ilp files with the preemption points and run cplex on it
126    `python conflict.py ../seL4-example/handleSyscall.imm.map blank\_file ../seL4-example/refutes_manual_open_sys.txt ../seL4-example/handleSyscall.imm.ilp_nofooter newIlp.ilp ../seL4-example --cx 5 new.sol`
127
128    Graph to graph also provides an automated shorthand for carrying out the above five steps:
129    `python graph_to_graph.py ../seL4-example handleSyscall --x ../seL4-example ../seL4-example/refutes_manual_open_sys.txt`
130
131seL4-example/refutes\_manual\_open\_sys.txt should contains, and mark the binary loops that are bounded only by phantom preemption points. These are the loops in cancelAllIPC, cancelAllSignals and cancelBadgeSends. The format is:
132`[loop address (refer to the generated loop\_counts.py)]:phantom_preemp_point`
133
134Overview
135--------
136
137 - [addr\_utils.py](addr\_utils.py): Miscellanous utility functions
138 - [bench.py](bench.py): Ties the WCET estimation tools together, also contains utilities for debugging CFG conversions.
139 - [convert\_loop\_bounds.py](elf\_parser.py): Interfaces with graph-refine's loop\_bounds.py and stores its results in targetDirectory/loop\_counts.py
140 - [cplex.py](cplex.py): Utility functions for interfacing with the CPLEX solver
141 - [elf\_correlate.py](elf\_correlate.py): Defines the immFunction format and uses it to translate a graph-refine function, and all the function that it calls into a Control Flow Graph (CFG)
142
143 - [elf\_parser.py](elf\_file.py): Various (text dumped) elf file parsing utility functions
144 - [reconstruct.py](reconstruct.py): Reconstruct the worst case from a ILP solution.
145 - [conflict.py](conflict.py): Annotate a given ILP problem with trace\_refute and artificial/phantom preemption points.
146 - [auto\_infea.py](auto\_infea.py): Repeatedly and automatically eliminate infeasible paths
147 - [graph\_to\_graph.py](graph\_to\_graph.py): The command line interface to graph\_to\_graph.
148 - [dot\_utils.py](dot\_utils.py): Visualize function graphs, used to debug CFG conversion. It's outdated and requires rewritings.
149 - [py\_dot.py](py\_dot.py): A direct copy of Graphviz's dot language Python interface. It's distributed under the MIT license.
150 - [chronos/parser.py](chronos/parser.py): An single instruction parser used to emit the IMM file that chronos accepts
151 - [chronos/emitter.py](chronos/emitter.py): Our interface to Chronos, generates a CFG in Chronos's IMM format from an immFunction
152
153
154Files in a Target directory
155--------
156 - [loop\_counts.py]: Generated by graph\_to\_graph, you can manually enter the loop bounds to this file after that. Automatical loop bounds discovery will update this file too.
157                      this is recorded as  a dictionary named loops_by_fs of function to dictionaries of binary loop head address to a triple (bound, comment, worker_id).
158                      If the comment contains the keyword ignored, convert_loop_bounds.py will not search for its bound. The worker_id is used for a undocumented parallesation scheme, and should be ignored and preserved by the user.
159 - [entryFunctionName.imm]: input to Chronos
160 - [entryFunctionName.imm.ilp]: ilp file generated by Chronos
161 - [entryFunctionName.imm.map]: Describes how the block ids in the .ilp file maps to the binary addresses.
162 - [phantom\_preempt.py]: Manual annotations that direct graph\_to\_graph to inject phantom preemption points into functions inside the target. Renders the result unsound, can only used for debugging purposes.
163
164
165