Skip to content
Snippets Groups Projects
Commit cb372201 authored by Forget Julien's avatar Forget Julien
Browse files

Test, update, authors.

parent d6aeced4
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
README.md
+ 22
− 12
View file @ cb372201
...@@ -2,15 +2,16 @@ ...@@ -2,15 +2,16 @@
WSymb: Symbolic Worst-Case Execution Time (WCET) computation. WSymb: Symbolic Worst-Case Execution Time (WCET) computation.
* Version 1.0.0 (for OTAWA v2), April 2020 * Version 1.1 (for OTAWA v2), December 2023
---- ----
## Authors ## Authors
* Clement Ballabriga <Clement.Ballabriga@nospamuniv-lille.fr> * Clement Ballabriga <Clement.Ballabriga@nospamuniv-lille.fr>
* Julien Forget <Julien.Forget@nospamuniv-lille.fr> * Julien Forget <Julien.Forget@nospamuniv-lille.fr>
* Celestine Sauvage <celestine.sauvage@nospamgmail.com>
* Sandro Grebant <sandro.grebant@nospamuniv-lille.fr> * Sandro Grebant <sandro.grebant@nospamuniv-lille.fr>
* Giuseppe Lipari <giuseppe.lipari@nospamuniv-lille.fr>
* Celestine Sauvage <celestine.sauvage@nospamgmail.com>
License: GPL 2.1 or higher. License: GPL 2.1 or higher.
...@@ -20,12 +21,12 @@ Please remove "nospam" from the email addresses. ...@@ -20,12 +21,12 @@ Please remove "nospam" from the email addresses.
## Introduction ## Introduction
WSymb is a WCET analysis tool. Its main specificity is that, instead of WSymb is a WCET analysis tool. Its main specificity is that, instead
a constant WCET, it computes a *WCET formula*, where symbols (or of a constant WCET, it computes a *WCET formula*, where symbols (or
parameters) can correspond to various kinds of values unnkown at analysis parameters) can correspond to various kinds of values unnkown at
time. The formula can later be *instanciated*, when parameter values are analysis time. The formula can later be *instanciated*, when parameter
known. For more details on the underlying theory, check out the papers values are known. For more details on the underlying theory, check out
[1,2]. the papers [1,2].
WSymb consists of several separate parts: WSymb consists of several separate parts:
...@@ -43,6 +44,12 @@ WSymb consists of several separate parts: ...@@ -43,6 +44,12 @@ WSymb consists of several separate parts:
* The instantiation of the WCET formula relies on an API documented in * The instantiation of the WCET formula relies on an API documented in
`pwcet/include/pwcet-tuntime.h`. `pwcet/include/pwcet-tuntime.h`.
* `WCET-procedure-arguments-as-parameters.md`: this file describes an
extension to the original analysis, which analyzes the binary code
of a procedure to produce a WCET formula that represents the WCET of
the procedure as a function of its arguments. It implements the
approach presented in [2].
A complete example covering all these different parts is provided in A complete example covering all these different parts is provided in
directory `example`. directory `example`.
...@@ -163,8 +170,11 @@ so: ...@@ -163,8 +170,11 @@ so:
---- ----
## References ## References
[1] Ballabriga, C., Forget, J., & Lipari, G. (2018). Symbolic WCET computation. ACM Transactions on Embedded Computing Systems (TECS), 17(2), 39. [1] Ballabriga, C., Forget, J., Lipari, G. (2018). Symbolic WCET
ISO 690 computation. ACM Transactions on Embedded Computing Systems (TECS),
17(2), 39. https://hal.science/hal-01665076
[2] https://arxiv.org/abs/1709.09369
[2] Grebant S, Ballabriga C, Forget J, Lipari G. WCET analysis with
procedure arguments as parameters. InProceedings of the 31st
International Conference on Real-Time Networks and Systems 2023 Jun 7
(pp. 11-22). https://hal.science/hal-04118213
WCET-procedure-arguments-as-parameters.md
+ 5
− 11
View file @ cb372201
# WCET analysis with procedure arguments as parameters # WCET analysis with procedure arguments as parameters
* Version 1.0.0, November 2023
---- ----
## Authors ## Authors
...@@ -27,12 +25,10 @@ arguments. It implements the approach presented in [1]. ...@@ -27,12 +25,10 @@ arguments. It implements the approach presented in [1].
Required packages: Required packages:
- WSymb, cloned from its - WSymb, cloned from its
[git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/polymalys) [git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/polymalys);
branch ``input conditionals``;
- Otawa for WSymb (see instructions in the README.md of WSymb); - Otawa for WSymb (see instructions in the README.md of WSymb);
- Polymalys, cloned from its - Polymalys, cloned from its
[git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/WSymb), [git](https://gitlab.cristal.univ-lille.fr/otawa-plugins/WSymb);
branch ``input conditionals``;
- Otawa for Polymalys (see instructions in the README.md of Polymalys); - Otawa for Polymalys (see instructions in the README.md of Polymalys);
- Basic compilation tools (make, gcc, g++, as well as the arm - Basic compilation tools (make, gcc, g++, as well as the arm
versions). versions).
...@@ -71,12 +67,10 @@ In the following, the required version is specified when necessary. ...@@ -71,12 +67,10 @@ In the following, the required version is specified when necessary.
### Polymalys ### Polymalys
Compile Polymalys (using Otawa for Polymalys): Compile Polymalys (using Otawa for Polymalys):
```shell ```shell
./do_in.sh polymalys cd <polymalys>; make install cd tests; make poly ./do_in.sh polymalys make -C <polymalys> install; make -C <polymalys>/tests poly
``` ```
### WSymb ### WSymb
...@@ -84,7 +78,7 @@ Compile Polymalys (using Otawa for Polymalys): ...@@ -84,7 +78,7 @@ Compile Polymalys (using Otawa for Polymalys):
Compile and install WSymb (using Otawa for WSymb): Compile and install WSymb (using Otawa for WSymb):
```shell ```shell
./do_in.sh wsymb cd <wsymb>; make install; cd simplify; make; cd libpwcet; make ./do_in.sh wsymb make -C <wsymb> install; make -C <wsymb>/simplify; make -C <wsymb>/libpwcet
``` ```
---- ----
...@@ -106,7 +100,7 @@ file wih Otawa (any of the two Otawa versions should produce the same ...@@ -106,7 +100,7 @@ file wih Otawa (any of the two Otawa versions should produce the same
result): result):
```shell ```shell
./do_in.sh wsymb <otawa-wsymb>/bin/mkff <programme>.elf [function] > programme.elf ./do_in.sh wsymb <otawa-wsymb>/bin/mkff <programme>.elf [function] > <programme>.ff
``` ```
Specifying the function is optional. If the function is not specified, Specifying the function is optional. If the function is not specified,
......
do_in.sh
+ 3
− 5
View file @ cb372201
#!/bin/sh #!/bin/sh
# update the two first variables as necessary # update the two variables below as necessary
OTAWA_POLY=/home/forget/Code/WSymb-procedures/polymalys/otawa OTAWA_POLY=/home/forget/Code/polymalys/otawa
OTAWA_WSYMB=/home/forget/Code/WSymb-procedures/otawa OTAWA_WSYMB=/home/forget/Installs/otawa-wsymb/otawa
case $1 in case $1 in
"polymalys" ) "polymalys" )
echo "Executing with Otawa version Polymalys"
export PATH=$OTAWA_POLY/bin/:$PATH export PATH=$OTAWA_POLY/bin/:$PATH
export LD_LIBRARY_PATH=$OTAWA_POLY/lib/:$OTAWA_POLY/lib/otawa/otawa/:$LD_LIBRARY_PATH export LD_LIBRARY_PATH=$OTAWA_POLY/lib/:$OTAWA_POLY/lib/otawa/otawa/:$LD_LIBRARY_PATH
shift shift
$*;; $*;;
"wsymb" ) "wsymb" )
echo "Executing Otawa version WSymb"
export PATH=$OTAWA_WSYMB/bin:$PATH export PATH=$OTAWA_WSYMB/bin:$PATH
export LD_LIBRARY_PATH=$OTAWA_WSYMB/lib:$OTAWA_WSYMB/lib/otawa/otawa:$LD_LIBRARY_PATH export LD_LIBRARY_PATH=$OTAWA_WSYMB/lib:$OTAWA_WSYMB/lib/otawa/otawa:$LD_LIBRARY_PATH
shift shift
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment