Project

General

Profile

History

Documentation for the GenoM3 fiacre/model template

The fiacre/model GenoM3 template is invoked with:

genom3 fiacre/model <module(s).gen>

It will create a tina subdirectory containing a number of files.

cd tina
autoreconf -vif
./configure --prefix=${HOME}/work

Note that for the configure to succeed, you need first to define both HIPPO_DIST and TINA_DIST environment variables. Put these variables (tune the values for your installation) in your .bashrc file.

export HIPPO_DIST=${HOME}/work/hippo-2.6.5
export TINA_DIST=${HOME}/work/tina-3.6.0

The fiacre/model template takes many different arguments to synthesize the smallest model needed for the verification you may want to carry.

genom3 fiacre/model -h

FIACRE (Tina) component generation.

This template synthesize a Tina version.

Supported options:
  -C, --directory dir	output files in dir.
  -p, --preserve	do not overwrite existing files.
  -M, --port_mapping port_mapping_file	use this file as a dict for mapping in port in out port (compin_portin compout_portout)
  -w, --wcet wcetfile	use the file as a dict with the wcet value.
  -r, --rqst rqstfile	use the file as a dict with included rqst in the model.
  -W, --wcet_exec	worst case execution of codel.
  -c, --client file	insert the content of a client file in the model.
  -g, --generic_client	produces a generic client.
  -n, --exp_name name	use this name as a "multi component" experiment.
  -s, --slow		specify the slow down factor as a frequency (1 time unit = 1/frequency).
  -m, --MaxCore	specify the max numberof core available.
      --TANoException	Fiacre model without GenoM exception.
      --TASimpleControl	Fiacre model with simple control task model.
      --TANoInterrupt	Fiacre model interrupt between services.
      --TANoDefServ	Fiacre model without default services.
      --TANoBeforeAfter	Fiacre model without services before/after.
      --TANoPort		Fiacre model  without port access checking/locking.
      --TAShiftedStart		Timer, ET and CT have their start shifted to prevent massive 0 time state interleaving.
  -h. --help		print usage summary (this text)

Let’s explain the various fiacre specific arguments:

  • -M, --port_mapping port_mapping_file Ports in GenoM3 are specified as in or out in the .gen file. In any regular experiment, the connect_port request is used to connect in port to out port at runtime. For these connection to be taken into account in the synthesize model, one can specify the mapping in a file as a tcl dict to map in port to out port with the syntaz: component-name-in_port-name_in component-name-out_port-name-out. Note that GenoM3 multiple ports are not supported.

  • -w, --wcet wcetfile Use the content of wcetfile as a tcl dict with the wcet value for each codel of the experiment. The wcet value is given in second.

  • -r, --rqst rqstfile use the file as a dict with included rqst in the model. Only the request present in this file will modeled. This can be usefull if you know your experiment isonly using this specific requests, or if you want to limit the seach to these. Note that the default requests (connect_port, connect_service, abort-activity and kill) will not be present if you do not include them.

  • -W, --wcet_exec worst case execution of codel. If this option ispresent, the Fiacre model consider that codel execution takes exactly the wcet value i.e. [wcet,wcet], insteaad of [0,wcet].

  • -c, --client file insert the content of a client file in the model. The client specified in the file will be inserted in the model. Most usefullif you want to test a specific sequence of requests.

  • -g, --generic_client produces a generic client. The model will include a generic client which can send any request at any time…​ Probably not what you want for a large model.

  • -n, --exp_name name use this name as a "multi component" experiment. When including more than one genom3 component, it is often good to have a name for the whole experiment/model.

  • -s, --slow Specify the slow down factor as a frequency (1 time unit = 1/frequency). Fiacre and TINA only use integer (no float), so time values must be given as int. For this, wcet and period are multiply by this number. -s 1000 means that the model will be synthesized with time values in milliseconds. If you have a wcet of 0.025 seconds, it will become 25 in the model. Similarly, a task with aperiod of 20 Hz (50 ms), witll have a cycle of [50,50].

  • -m, --MaxCore This can be used to specify the max number of core available on your target. 0 means unlimited, any other number will be used as a strick limit of the number of possible codel execution in the verification. This is enforce with a guard on the codel execution.

All the following arguments tend to abstract the fiacre model in some way (TA stands for Tina Abstraction), by not including some particular aspect of the model. Most of these option have a real impact on the execution and verification, use with caution.

  • --TANoException Fiacre model without GenoM exception. The possible exception returned by codels are not modelled. This assume that all execution are nominal, no exception.

  • --TASimpleControl Fiacre model with simple control task model. The control part of request is composed of different phases, (run_maps, prologue, validate, middle, control, inter, report_or_transfer). This option is an attemps to simplify this…​

  • --TANoInterrupt Fiacre model with no interrupt between request. The interrupt code, and thus the capacity to enforece the interrupt field of the request genom specification is not synthesized.

  • --TANoDefServ Fiacre model without default services. The model does not include the default services: connect_port, connect_service, abort-activity and kill

  • --TANoBeforeAfter Fiacre model without services before/after. The before after part of the model is not enforced.

  • --TANoPort Fiacre model without port access checking and locking.

  • --TAShiftedStart All Fiacre process (Timer, Execution Tasks and Control Tasks) have their start shifted to prevent massive 0 time state interleaving.