项目作者: PatrickTrentin88

项目描述 :
Semantic-Based Worst Case Execution Time of Loop-Free C Programs using Optimization Modulo Theory
高级语言: Shell
项目地址: git://github.com/PatrickTrentin88/wcet_omt.git
创建时间: 2017-01-04T15:01:07Z
项目社区:https://github.com/PatrickTrentin88/wcet_omt

开源协议:Other

下载


DESCRIPTION

This project aims to reproduce the results obtained in the paper

  1. [HAL-14]
  2. How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics
  3. Julien Henry (VERIMAG - IMAG), Mihail Asavoae (VERIMAG - IMAG), David Monniaux (VERIMAG - IMAG), Claire Maïza (VERIMAG - IMAG)
  4. HAL-00998138 https://hal.archives-ouvertes.fr/hal-00998138

We expand over [HAL-14] in the following way:

  • new and improved build-chain and framework
  • new and improved benchmarking functionality with support for z3 and OptiMathSAT
  • minor fixes and general update to original smtopt source code for compatibility with newer z3’s API
  • updated smt2 formula encoding to use Optimization Modulo Theory language extensions
  • added two additional formula encodings
  • added default omt solver configurations for benchmarks

The original work of [HAL-14] is made available within Pagai’s sources, and
is located in the path tools/pagai/WCET after installation.

LIMITATIONS

There are a number of inherent limitations in this work, some of which are caused by
the use of outdated version of libraries and tools (clang, llvm, z3) and others arising
directly from Pagai.

Known issues:

  • Pagai running out of memory / stuck
  • opt running out of memory when performing loop unrolling over some benchmarks
  • no support for bytecode with loops which have not been unrolled (also in [HAL-14])

REQUIREMENTS

This project has been tested on linux-gnu only. In case support for another OS is needed, contact
the project maintainer https://github.com/PatrickTrentin88/wcet_omt.

INSTALLATION

The project comes with an installation script which attempts to download and configure the
required dependencies. In case of failure, please refer to wcet_omt/setup_tools/REAME.md
for manual installation.

Type

  1. ~$ make -f Makefile.master install

in the root directory and follow the instructions.

Please note that the following packages and tools, or their equivalent for your own distribution,
should be installed on your system in order to successfully install the required resources:

  • coreutils # (timeout, realpath)
  • make
  • g++
  • curl
  • cmake
  • flex
  • bison
  • libgmp3-dev
  • libmpfr-dev
  • libboost-all-dev
  • libncurses5-dev

TESTING INSTALLATION

Follow the instructions found in wcet_omt/test/README.md.

USAGE

To run a simple experiment, type

  1. ~$ pushd test/bench
  2. ~$ make optimathsat_0 optimathsat_2_dl_1
  3. ~$ popd

Here, optimathsat_0 and optimathsat_2_dl_1 are compilation targets, scroll this
file for more information.

As the experiment runs, the following folder structure is added to the file-system:

  1. wcet_omt
  2. |-- test
  3. |-- stats
  4. |-- bench
  5. |-- optimathsat_0
  6. | |-- optimathsat_0.txt # summary of relevant benchmark information
  7. | |-- benchmark_1.log
  8. | |-- ...
  9. | |-- benchmark_i.log # the omt solver's output for i-th benchmark
  10. | |-- ...
  11. | |-- benchmark_N.log
  12. |
  13. |-- optimathsat_2_dl_1
  14. |-- optimathsat_2_dl_1.txt # summary of relevant benchmark information
  15. |-- benchmark_1.log
  16. |-- ...
  17. |-- benchmark_i.log # the omt solver's output for i-th benchmark
  18. |-- ...
  19. |-- benchmark_N.log

To modify the experimental conditions (e.g. change TIMEOUT), the Makefile within the target
benchmark directory should be edited. Please avoid any change to Makefile.master.

TARGETS

Benchmark targets are defined in Makefile.master, and correspond to the list of HANDLER_UIDS
mentioned by

  1. ~$ ./bin/run_experiment.sh -h
  2. ...
  3. HANDLER UIDS
  4. z3_0 -- z3 + default encoding
  5. z3_0_cuts -- z3 + default encoding + cuts
  6. smtopt_0 -- smtopt + default encoding
  7. smtopt_0_cuts -- smtopt + default encoding + cuts
  8. optimathsat_0 -- optimathsat + default encoding
  9. optimathsat_0_cuts -- optimathsat + default encoding + cuts
  10. optimathsat_1_sn -- optimathsat + assert-soft enc. + + sorting networks
  11. optimathsat_1_cuts_sn -- optimathsat + assert-soft enc. + cuts + sorting networks
  12. optimathsat_2 -- optimathsat + diff. logic enc.
  13. optimathsat_2_cuts -- optimathsat + diff. logic enc. + cuts
  14. optimathsat_2_dl_1 -- optimathsat + diff. logic enc. + + dlSolver + short tlemmas
  15. optimathsat_2_cuts_dl_1 -- optimathsat + diff. logic enc. + cuts + dlSolver + short tlemmas
  16. optimathsat_2_dl_2 -- optimathsat + diff. logic enc. + + dlSolver + long tlemmas
  17. optimathsat_2_cuts_dl_2 -- optimathsat + diff. logic enc. + cuts + dlSolver + long tlemmas
  18. optimathsat_2_dl_3 -- optimathsat + diff. logic enc. + + dlSolver + both tlemmas
  19. optimathsat_2_cuts_dl_3 -- optimathsat + diff. logic enc. + cuts + dlSolver + both tlemmas
  20. ...

Each HANDLER_UID corresponds to a specific combination of SMT2 encoding, OMT solver
and solver parameters wrapped into a function that acts as a benchmark handler. These
handlers are defined within wcet_omt/bin/wcet_lib/wcet_handlers.sh.

DEBUG

The scripts are designed to print any error that might be encountered. However, to keep the
output nice and clean, relevant debugging information is hidden by default. To enable it, type:

  1. ~$ pushd bench/test
  2. ~$ export WCET_DEBUG=1
  3. ~$ make all
  4. ~$ popd

LOOP UNROLLING

Loops are not supported and need to be unrolled. By default, loops in the bytecode are not
optimized out. To enable this feature, type:

  1. ~$ pushd bench/test
  2. ~$ export WCET_UNROLL=1
  3. ~$ make all
  4. ~$ popd

Loop unrolling might fail, please refer to the loop unrolling log file for more information.