This note shows how a small Ada program for the SPARC/ERC32 is analysed by Bound-T and what the results are. Both execution time (WCET) analysis and stack-usage analysis are demonstrated.
The example is organized as follows:
The example program consists of a singe Ada source file, exa.adb. The source code is is displayed with line numbers for reference. When it can, Bound-T uses source-line numbers in its outputs to identify the relevant part of the program, for example a loop or a call. Here is a ZIP archive with all the files in case you prefer to browse them directly.
This program does nothing useful, but has been designed to illustrate several features and limitations of Bound-T with a compact example. For an overview of the example you can take an advance peek at the call graph, as drawn by Bound-T.
Some points to be noted in this example are:
For this example, the program has been compiled and linked for the SPARC/ERC32 target processor, using the GNAT Ada compiler from AdaCore (version GAP 2006). A build script (build.sh) for this compilation and linking is included in the ZIP archive, as is the executable file.
The executable file is named "exa" and is in ELF form. This is the main input to Bound-T.
The operation and usage of Bound-T are explained in the User Guide, the Reference Manual, and the relevant Application Note documents. The following examples show some ways to use Bound-T/SPARC to analyse this example program for its worst-case execution time and stack usage.
The only files from this folder that are actually needed for these example analyses are the SPARC/ERC32 executable "exa" and the assertion file "assertions.txt". In particular, the Ada source-code file is not necessary; Bound-T does not use the source-code files. The output from Bound-T includes references to source-code files and line-numbers, but these are all taken from the debugging information that the compiler generated and placed in the ELF file.
As a first example we use Bound-T to analyse the subprogram (Ada procedure) Count25. The following command will do that:
boundt_sparc -erc32 exa exa__count25
Note that there are two consecutive underline (_) characters in the second argument, exa__count25.
The components of this command are:
The result of this commmand is the following output. Line numbers are added here for reference.
1 Loop_Bound:exa:exa.adb:exa__count25:51-55:12 2 Wcet:exa:ccN1JN58.s:.umul:12-77:41 3 Wcet:exa:exa.adb:exa__count25:41-55:624 4 Block_Wcet:exa:ccN1JN58.s:.umul:12-77:0:0..0:0:0:0 5 Block_Wcet:exa:exa.adb:exa__count25:41-55:0:0..0:0:0:0
The first output line (line 1) reports that Bound-T has determined that the loop in the Count25 procedure, on lines 51-55 in the file "exa.adb", repeats at most 12 times. (In fact the body of the loop — the assignment to X.all — is executed 13 times. The Loop_Bound that Bound-T finds is only 12 because the compiler has generated code for a "bottom-test" loop and Bound-T shows the number of times the code jumps backwards to repeat the loop once more.)
Line 2 reports that Bound-T has determined an upper bound of 41 machine cycles on the worst-case execution time (WCET) of the library function, .umul. This is a library routine that implements multiplication of unsigned integers. The line also shows that the .umul function seems to be located in a source file called "ccN1JN58.s" at lines 12-77; the suffix ".s" indicates that this is an assembly-language file, which is not surprising for such a function.
Line 3 reports that the WCET bound for Count25, including the WCET for .umul, is 624 machine cycles. The line also shows that Count25 is located in the source-file "exa.adb" on lines 41-55.
The two last output lines, lines 4 and 5, report the amount of pipeline blocking (pipeline stalls) that Bound-T has included in the WCET bounds for .umul and Count25, respectively. The meaning of these output lines is explained in the Application Note for the SPARC/ERC32 version of Bound-T.
To analyse the top-level Main procedure in the example program, you can try the command
boundt_sparc -erc32 exa exa__main
which asks Bound-T to analyse the Main procedure. However, there are some loops for which Bound-T cannot find iteration bounds, so the output of this command, displayed below, includes some warnings and error messages (some of these are rather long, so you may have to scroll right to see them in full). Line numbers are added here for reference.
1 Warning:exa:exa.adb:exa__main:167-:Eternal loop (no exit edges). 2 Loop_Bound:exa:exa.adb:exa__count25:51-55:12 3 Loop_Bound:exa:exa.adb:exa__solve:126-135:7 4 Warning:exa:exa.adb:exa__foo7@93-=>exa__count:73:Unreachable flow to instruction at [02001580-020015A4] 5 Loop_Bound:exa:exa.adb:exa__foo7@93-=>exa__count:73-77:3 6 Warning:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:73:Unreachable flow to instruction at [02001580-020015A4] 7 Loop_Bound:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:73-77:4 8 Warning:exa:exa.adb:exa__main:142-167:Non-returning subprogram. 9 Wcet:exa:ccN1JN58.s:.umul:12-77:41 10 Wcet:exa:exa.adb:exa__count25:41-55:624 11 Wcet_Call:exa:exa.adb:exa__foo7@93-=>exa__count:62-77:202 12 Wcet:exa:exa.adb:exa__foo7:84-96:226 13 Wcet_Call:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:62-77:249 14 Wcet_Call:exa:exa.adb:exa__main@163-=>exa__foo:101-110:261 15 Error:exa:exa.adb:exa__main:142-167:Could not be fully bounded. 16 17 18 exa__main 19 Loop unbounded (eternal) at exa.adb:167-, offset 0000004C 20 exa__main@167-=>exa__solve@129-=>exa__ones 21 Loop unbounded at exa.adb:26-32, offset 00000014 22 exa__main@167-=>exa__solve@135-=>exa__count 23 Loop unbounded at exa.adb:73-77, offset 00000014
The "Wcet" output lines that come before the "Error" line show the results that Bound-T gets for those subprograms where the analysis succeeds. Ignore these outputs for the moment.
In the output quoted above, line 1 reports that Bound-T has found an eternal (non-terminating) loop in the Main procedure after line 167 in the file "exa.adb". (The loop is actually on lines 171-173, but it seems that the compiler has not generated an exact mapping of this loop-code to source lines.)
The four Loop_Bound lines (lines 2, 3, 5, and 7) report the iteration bounds that Bound-T determines for four loops. Some of these bounds are context-dependent, meaning that they are valid only for a particular call path. For example, line 5 reports that the loop in the procedure Count (linker name "exa__count"), at lines 73-77 in "exa.adb", has an upper bound of 3 repetitions when Count is called from the procedure Foo7 through the call at line 93. (The line-number is given in the form "93-", with a trailing hyphen, because we are using the default Bound-T option "-lines around", which allows an approximate line-to-code mapping, and the compiler did not map the actual call instruction to line 93, but some instruction just before the call was mapped to line 93.)
The fourth Loop_Bound (line 7) shows that the same loop in Count has a different bound when Count is called in a different context.
The two Warning lines that mention "unreachable flow" (lines 4 and 6) show that Bound-T has found a certain conditional branch in Count to be infeasible. If you look at the generated code (for example in the flow graph of Count) you will see that the compiler has made a test to check if the loop should be executed at all, and Bound-T finds that this check must be true in certain contexts (with certain parameter values), so the "false" branch is unreachable in these contexts.
The Warning on line 8 says that the Main procedure never returns to its caller. This is of course due to the eternal loop at the end of Main.
Line 15 reports, as an Error, that Bound-T could not find a WCET bound for the Main routine. The indented, hierarchical listing after the Error line shows that the problems are the eternal loop in Main, a loop in the function Ones, which is called from the procedure Solve, and the loop in Count when Count is called from Solve. This is the same loop for which Loop_Bounds were found when Count was called from two other contexts (see output lines 5 and 7), but those context-specific bounds do not apply when Count is called from Solve.
The reasons why Bound-T cannot find bounds on these loops are explained in comments in the source-code file (exa.adb). For such loops, the user must support Bound-T by stating assertions on the program's behaviour. We do that in the next section of this example.
To compute a WCET bound for the example program, we must help Bound-T find bounds on the loops reported in lines 16 through 20 above. This is done by writing an assertion file. This can be done in several ways, for example as in the following text (line numbers added for reference):
1 subprogram "exa__ones" 2 loop repeats 32 times; end loop; 3 end "exa__ones"; 4 5 subprogram "exa__solve" 6 variable "exa__solve|k" <= 32; 7 end "exa__solve"; 8 9 subprogram "exa__main" 10 loop repeats 1 time; end loop; 11 end "exa__main";
Line 1 above declares that the following lines, up to line 3, refer to the subprogram Ones (using its linker name "exa__ones"). Line 2 specifies that the loop in Onesrepeats at most 32 times in any call of Ones. This is because the Unsigned_Int variable X is 32 bits long and can be divided by 2 (shifted right) at most 32 times before it becomes zero. For the same reason, the value returned from Ones is always between 0 and 32.
Line 5 in the assertion file above declares that the following lines, up to line 7, refer to the subprogram Solve. Line 6 asserts that within this loop the variable K, which is local to Solve, has a value that is at most 32. This holds because K is assigned the return value from Ones, which is between 0 and 32 as explained above.
Assuming that the assertion file is named "assertions.txt", the following command invokes Bound-T as above to analyse the main function, but under these assertions:
boundt_sparc -erc32 -assert assertions.txt exa exa__main
This time, the analysis succeeds without error messages. The output is the following, with line numbers added here for reference:
1 Warning:exa:exa.adb:exa__main:167-:Eternal loop (no exit edges). 2 Loop_Bound:exa:exa.adb:exa__count25:51-55:12 3 Loop_Bound:exa:exa.adb:exa__solve:126-135:7 4 Loop_Bound:exa:exa.adb:exa__solve@135-=>exa__count:73-77:15 5 Warning:exa:exa.adb:exa__foo7@93-=>exa__count:73:Unreachable flow to instruction at [02001580-020015A4] 6 Loop_Bound:exa:exa.adb:exa__foo7@93-=>exa__count:73-77:3 7 Warning:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:73:Unreachable flow to instruction at [02001580-020015A4] 8 Loop_Bound:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:73-77:4 9 Warning:exa:exa.adb:exa__main:142-167:Non-returning subprogram. 10 Wcet:exa:ccN1JN58.s:.umul:12-77:41 11 Wcet:exa:exa.adb:exa__count25:41-55:624 12 Wcet_Call:exa:exa.adb:exa__foo7@93-=>exa__count:62-77:202 13 Wcet:exa:exa.adb:exa__foo7:84-96:226 14 Wcet_Call:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:62-77:249 15 Wcet_Call:exa:exa.adb:exa__main@163-=>exa__foo:101-110:261 16 Wcet:exa:exa.adb:exa__ones:10-36:176 17 Wcet_Call:exa:exa.adb:exa__solve@135-=>exa__count:62-77:766 18 Wcet:exa:exa.adb:exa__solve:115-135:7706 19 Wcet:exa:exa.adb:exa__main:142-167:8840 20 Block_Wcet:exa:ccN1JN58.s:.umul:12-77:0:0..0:0:0:0 21 Block_Wcet:exa:exa.adb:exa__count25:41-55:0:0..0:0:0:0 22 Block_Wcet:exa:exa.adb:exa__foo7@93-=>exa__count:62-77:0:0..0:0:0:0 23 Block_Wcet:exa:exa.adb:exa__foo7:84-96:1:1..1:1:0:1 24 Block_Wcet:exa:exa.adb:exa__main@163-=>exa__foo@110-=>exa__count:62-77:0:0..0:0:0:0 25 Block_Wcet:exa:exa.adb:exa__main@163-=>exa__foo:101-110:0:0..0:0:0:0 26 Block_Wcet:exa:exa.adb:exa__ones:10-36:0:0..0:0:0:0 27 Block_Wcet:exa:exa.adb:exa__solve@135-=>exa__count:62-77:0:0..0:0:0:0 28 Block_Wcet:exa:exa.adb:exa__solve:115-135:0:0..0:0:0:0 29 Block_Wcet:exa:exa.adb:exa__main:142-167:0:0..0:0:1:1
The output still contains the warnings about the eternal loop, the fact that Main never returns, and that some branches are unreachable, but no longer complains that Main could not be bounded. There are some new Loop_Bound lines, thanks to the assertions, and new Wcet and Wcet_Call lines, too. The overall result is shown by the "Wcet" line for the Main subprogram, line 19, which is:
19 Wcet:exa:exa.adb:exa__main:142-167:8840
Thus, Bound-T has found a WCET bound of 8840 cycles for the Main procedure.
The output ends with the Block_Wcet lines that show how much pipeline blocking is included in the WCET values, as in our first example.
If we add the command-line option "-table", Bound-T writes a tabular form of the analysis results as a number of output lines beginning with the keyword Time_Table:
Time_Table:exa:exa.adb:exa__main:142-167:8840:23:1:8840:8840:exa__main:exa.adb:142-167 Time_Table:exa:exa.adb:exa__main:142-167:624:91:1:624:624:exa__count25:exa.adb:41-55 Time_Table:exa:exa.adb:exa__main:142-167:6150:6150:150:41:41:.umul:ccN1JN58.s:12-77 Time_Table:exa:exa.adb:exa__main:142-167:226:24:1:226:226:exa__foo7:exa.adb:84-96 Time_Table:exa:exa.adb:exa__main:142-167:6579:962:10:202:766:exa__count:exa.adb:62-77 Time_Table:exa:exa.adb:exa__main:142-167:261:12:1:261:261:exa__foo:exa.adb:101-110 Time_Table:exa:exa.adb:exa__main:142-167:7706:170:1:7706:7706:exa__solve:exa.adb:115-135 Time_Table:exa:exa.adb:exa__main:142-167:1408:1408:8:176:176:exa__ones:exa.adb:10-36
The table is best viewed by passing the output through a script that formats the table for easy reading, with this result:
Total Self Num Time Per Call Time Time Calls Min Max Subprogram ----- ---- ----- ------------- ---------- 8840 23 1 8840 8840 exa__main 7706 170 1 7706 7706 exa__solve 6579 962 10 202 766 exa__count 6150 6150 150 41 41 .umul 1408 1408 8 176 176 exa__ones 624 91 1 624 624 exa__count25 261 12 1 261 261 exa__foo 226 24 1 226 226 exa__foo7
As you can see, the table shows at a glance which subprograms are used in the worst-case scenario, how many times each subprogram is called, how much time is spent in the subprogram including its callees, and how much of this time is spent in other subprogram itself, excluding callees.
If we add the command-line options "-dot graphs.dot" and "-draw total", Bound-T draws the call-graph of Main and the control-flow graphs of each analysed subprogram. The graphs are written to the file named in the -dot option (here graphs.dot) in a textual notation called the DOT form (from Drawer Of Trees). The program dot, from the Bell Labs GraphViz package, converts the graphs to other forms such as Postscript. The images that you can open from the links below have been converted to the PNG (Portable Network Graphics) form.
The control-flow graphs can be labeled with various kinds of information. For example, the option "-draw decode" will show the disassembled instructions in each graph node; this option was used to generate the graphs presented above. The "-draw" options are explained in the Bound-T Reference Manual.
The execution time of a SPARC program can be increased by handling the traps caused by overflows and underflows of the SPARC register window file. Bound-T can analyse the places (calls and returns) where such traps may happen and include the execution time of the trap handlers in the WCET bounds. This analysis is enabled with the option "-rw". We also add the option "-lines exact" for reasons explained later.
The following command repeats the earlier analysis of the procedure Count25, but now with register-window traps included:
boundt_sparc -erc32 -rw -lines exact exa exa__count25
The output from this command, as follows, contains the same results as in the earlier analysis, but also some new stuff (line numbers added here for reference):
1 Trap_Handler:exa::02000050:[02000050]:Register Window overflow 2 Trap_Handler:exa::02000060:[02000060]:Register Window underflow 3 Warning:exa::02000050:[02000054]:Dynamic control flow. 4 Warning:exa::02000060:[02000068]:Dynamic control flow. 5 Warning:exa::02000050:[02000054]:Indirect jump to 020011EC 6 Warning:exa::02000060:[02000068]:Indirect jump to 02001228 7 Loop_Bound:exa:exa.adb:exa__count25:51-55:12 8 Wcet:exa::02000050:[02000050-02001224]:53 9 Wcet:exa::02000060:[02000060-02001270]:42 10 RWin:exa:ccN1JN58.s:.umul:12-77:2:0..0:0:0:0 11 Wcet:exa:ccN1JN58.s:.umul:12-77:41 12 RWin:exa:exa.adb:exa__count25:41-55:2:1..1:0:0:0 13 Wcet:exa:exa.adb:exa__count25:41-55:624 14 Block_Wcet:exa::02000050:[02000050-02001224]:0:0..0:0:0:0 15 Block_Wcet:exa::02000060:[02000060-02001270]:0:0..0:0:0:0 16 Block_Wcet:exa:ccN1JN58.s:.umul:12-77:0:0..0:0:0:0 17 Block_Wcet:exa:exa.adb:exa__count25:41-55:0:0..0:0:0:0
The lines 1 and 2 that start with the keyword "Trap_Handler" report the trap vector addresses that Bound-T assumes for the overflow and underflow trap handlers. These depend on the option "-trap_base" which, for the ERC32 (-erc32) has the default value 2000000 hex which agrees with the trap vector address used in the example program. Other SPARC programs may use other trap vector addresses and then you must use the Bound-T command-line option "-trap_base" to tell Bound-T where the trap vector is.
Bound-T automatically analyses the trap handlers to find WCET bounds. As part of this analysis, it finds that there are jumps from the trap vector to the actual handler code, and these jumps are "indirect", that is, the address is taken from a register rather than defined statically in the instruction. The two first "Warning" lines (lines 3 and 4) show the presence of such indirect jumps and the next two "Warning" lines (lines 5 and 6) report the actual target addresses that Bound-T has computed for these jumps.
The two new "Wcet" output lines (lines 8 and 9) report the WCET bounds that Bound-T has determined for the trap handlers: 53 cycles for the overflow handler at address 2000050 and 42 cycles for the underflow handler at address 2000060.
The two output lines (lines 10 and 12) that start with the keyword "RWin" report the results of the register-window trap analysis for the two subprograms .umul and Count25, respectively. The final zeros show that neither subprogram can cause traps (in the context of this analysis). This explains why the WCET for Count25 from this analysis is the same (624 cycles) as from the earlier analysis which ignored the possibility of register-window traps. Register-window traps can become important when the program under analysis contains longer (deeper) call-paths.
The meaning of the "RWin" output lines is explained more fully in the Application Note for the SPARC version of Bound-T. Note that the register-file analysis depends on the assumed occupancy of the register file on entry to the "root" subprogram, here Count25.
The two new "Block_Wcet" lines report the pipeline blocks in the trap handlers; there are none in this program.
The option "-lines exact" was useful in this analysis because under the default option "-lines around" Bound-T reports the wrong source file and line-numbers for the trap handlers, for example:
Wcet:exa:b~exa.adb:02000050:-15:53
This happens because these subprograms are assembled into code in a way that creates no mapping from source-line to code address. Thus, "-lines around" makes Bound-T find the closest mapping which happens to lie in the binder-generated Ada file "b~exa.adb". The hyphen before the source-line number (-15) shows that the mapping is not exact and that line 15 of "b~exa.adb" is mapped to a code address that comes after the trap handler. The "-lines" option is explained in more detail in the Bound-T Reference Manual.
To compute an upper bound on the amount of SPARC stack space used in the example program, starting from the Main procedure, give the command:
boundt_sparc -erc32 -stack_path -no_time exa exa__main
The option "-no_time" disables WCET analysis so that we need no assertion file (in this example, but assertions may be required for stack-usage analysis of some programs). This gives the following output (line numbers are added here for reference):
1 Warning:exa:exa.adb:exa__main:167-:Eternal loop (no exit edges). 2 Stack:exa:exa.adb:exa__ones:10-36:sp:112 3 Stack:exa:ccN1JN58.s:.umul:12-77:sp:0 4 Stack:exa:exa.adb:exa__count:62-77:sp:112 5 Stack:exa:exa.adb:exa__count25:41-55:sp:112 6 Stack:exa:exa.adb:exa__solve:115-135:sp:224 7 Stack:exa:exa.adb:exa__foo:101-110:sp:224 8 Stack:exa:exa.adb:exa__foo7:84-96:sp:224 9 Stack:exa:exa.adb:exa__main:142-167:sp:336 10 Warning:exa:exa.adb:exa__main:142-167:Non-returning subprogram. 11 Warning:exa::::No time analysis, so IU/FP blocking ignored. 12 Stack_Path:exa:exa.adb:exa__main@159-=>exa__foo7:159-:sp:336:112:112:224 13 Stack_Path:exa:exa.adb:exa__foo7@93-=>exa__count:93-:sp:224:112:112:112 14 Stack_Leaf:exa:exa.adb:exa__count:62-77:sp:112:112::
The two Warnings in lines 1 and 10 are about the eternal loop in Main and the fact that the Main subprogram never returns. This has no effect on the stack analysis. The third Warning in line 11 simply notes that Bound-T will not model the possible blocking delays between the SPARC/ERC32 Integer Unit and Floating Point unit, because the "-no_time" option makes it unnecessary.
The Stack lines show the total stack usage of each analysed subprogram, including all subprograms that this subprogram calls. Thus, the final Stack line (line 9) shows that the total stack usage of the Main subprogram, including all the subprograms that Main calls, is 336 stack locations (336 octets).
The Stack_Path lines and the Stack_Leaf line show the call-path from Main that requires the largest amount of stack space, which is the path Main => Foo7 => Count. The four numbers at the end of these lines show, respectively:
Thus, the first Stack_Path line (line 12) shows that the Main subprogram requires stack space as follows:
The procedures Main, Foo7 and Count each require 112 stack locations for their own uses. The total usage, 336 octets, is simply the sum 112 (Main) + 112 (Foo7) + 112 (Count). Note that there can be other call-paths that have the same stack usage; Bound-T shows just one of these maximal paths.
The reason why each of these subprograms uses the same, rather large amount of stack for its own purposes is the SPARC register-window architecture, which requires space for one whole register window, and some other standard space, in each stack frame. Furthermore, these subprograms have so few local variables that they can be held in registers and do not add to the stack usage.
Note that the total stack usage from boot (reset) of the processor may be larger than computed for Main, because the startup functions may (and typically do) need some stack space, before the Main procedure is entered.
The present version of Bound-T/SPARC has a problem that makes stack analysis fail for the register-window trap handlers. Therefore you should not use the "-rw" option together with stack analysis. The option "-rw" is anyway unnecessary for stack analysis because the register-window traps have no effect on the stack usage, as the space for storing overflowing register sets is statically allocated in each stack frame and thus included in the stack-usage analysis without "-rw".
The SPARC (V7) has no integer division instructions, so compilers provide library functions for this purpose. Unfortunately these functions are usually written in a form that makes the control-flow graph irreducible which means that Bound-T cannot find a WCET bound. The WCET of these routines must be determined in some other way and supplied to Bound-T with assertions.
We have measured the execution time of these functions on an ERC32 for a large number of randomly generated parameters. The file "divrem.txt", included in the ZIP archive, shows the maximum execution time we measured; of course, there is no guarantee that this is actually the WCET for these functions. Moreover, your library may have different versions of these functions (although this seems unlikely).
If your program uses these functions, include the option "-assert divrem.txt" to use these times as the WCET for these functions. Note that you can put several "-assert" options in one and the same Bound-T command and so use assertions from several files.