CertiCAN: A Coq certifier of CAN analysis results

Instructions for RTAS’19 Artifact Evaluation

Overview

This document presents the artifact for the paper “CertiCAN: A tool for the Coq certification of CAN analysis results” to be presented at RTAS’19.The theories and tools presented in our paper have been formally specified using the Prosa library and verified using the Coq proof assistant. Therefore, the correctness of proofs can be automatically and mechanically verified. It is possible to reproduce all results presented in our paper following the instructions below.

The rest of this document is structured as follows:

1. Summary
2. Installation
3. Checking the correctness of proofs
4. Locating the specifications and the main theorems
5. Experimental evaluation

I. Summary

II. Installation

In order to compile and mechanically check our proofs, the Coq proof assistant and the Mathematical Components library must be installed. For this, we recommend using our VM image for the artifact evaluation, which provides an operating system Ubuntu 16.04.5 and all required tools (eg. Ocaml, Coq, Coqide …). The Coq and OCaml sources  as well as test files can be found in the Desktop directory.

To boot the VM image you must:

1. Download and install VirtualBox
2. Download our packaged VM image file
3. Double-click on the downloaded VM image file certican.ova and then choose the Import button (before importing the VM, you can set the size of memory, 2Gb by default. Set more memory if you have, which can be helpful for the experiments).
   If it does not work, please check the size of memory and disk reserved for the VM. It requires at least 2Gb of memory and 10Gb of disk.
4. Start the VM (user name and password are both: certican)

By default, the keyboard layout is set as English QWERTY, you can change it by using the command setxkbmap if you like (e.g., setxkbmap fr for a French layout).

Manual installation (Skip if you choose to use the VM)

If you prefer to install the environment in your system, please install the following versions:

• Coq 8.8.2
• Mathcomp1.7.0

and our proofs as well as other related files can be downloaded here.

If you would like to use Coqide to read our Coq files (*.v), please set “Edit -> Preferences -> Project -> project file” as “_CoqProject_coqide” inside coqide GUI.

III. Checking the correctness of proofs

In the following, we suppose that you use the VM and are in the directory /home/certican/Desktop.

The correctness of our proofs can be automatically checked by running the following commands in Terminal.

First of all, you need to access the directory certican-v0.1/Coq-source (Recall: In the VM, the complete path should be /home/certican/Desktop/certican-v0.1/Coq-source); Then,

1) Generate makefile

$ ./create_makefile.sh

2) Remove binary files

$ make clean

3) Verify the proofs

$ make validate

This command will compile the proofs to generate compiled binary files (*.vo) then run coqchk, a stand alone Coq verifier.

After a few minutes, you will obtain the following output:

CONTEXT SUMMARY ===============* Theory: Set is predicative* Axioms: mathcomp.ssreflect.finfun.FunFinfun.finfunE mathcomp.ssreflect.finfun.FunFinfun.fun_of_finE mathcomp.ssreflect.fintype.SubsetDef.subsetEdef mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef mathcomp.ssreflect.finfun.FunFinfun.fun_of_fin mathcomp.ssreflect.tuple.FinTuple.enumP mathcomp.ssreflect.tuple.FinTuple.enum mathcomp.ssreflect.bigop.BigOp.bigopE mathcomp.ssreflect.finfun.FunFinfun.finfun mathcomp.ssreflect.tuple.FinTuple.size_enum mathcomp.ssreflect.fintype.CardDef.card Coq.Logic.Classical_Prop.classic mathcomp.ssreflect.fintype.CardDef.cardEdef mathcomp.ssreflect.bigop.BigOp.bigop mathcomp.ssreflect.fintype.SubsetDef.subset mathcomp.ssreflect.fintype.Finite.EnumDef.enum

In the output, there are a list of axioms:

• mathcomp.*: files from the Mathematical Components library. Inside these files, defined axioms are not real axioms but interfaces used in Module system.
• Coq.Logic.Classical_Prop.classic: a file from the Coq standard library. Indeed, our proof uses the classic axiom: P \/ ~P.

Our files (starting with rt.*) do not use any other axiom. This means that our proofs are complete and correct.

Note that the Coq verifier coqchk only checks the logical information i.e. type, syntax and proof etc. One still need to manually check that specifications and the main theorems are indeed what they are supposed to be.

IV. Locating the specifications and the main theorems

Our proofs are built on top of the Prosa library, therefore the basic specifications (e.g. arrival sequence, schedule, busy window… etc.) have been defined in Prosa and manually checked. In addition, we have also introduced a few specifications for model of transactions with tasks with offsets and the FPNP scheduling policy.

In the following, we provide links to the main notions and theorems used in our development. Whenever a specification is from Prosa, we mark it explicitly.

IV.1. System behavior

Arrival sequences (AS) (from Prosa)

Definition: A valid arrival sequence respects:

• Consistent arrival times
• No duplicate arrivals
• Valid job parameters

Schedule  (from Prosa)

Definition: A valid schedule respects:

• Scheduled jobs are from AS
• Jobs must arrive to execute
• Completed jobs don’t execute

Definition of a work-conserving schedule

IV.2. Task model: Transaction with offsets

A transaction is defined as a list of tasks which

• are periodic with offsets
• share the same local clock (i.e., respect transaction model)

IV.3. Scheduling policy

Definition of the FPNP scheduling policy

Jobs from the same task execute in FIFO order

IV.4. Workload bound function

Definition of the workload bound function for a single task

Proof of correctness of the workload bound within a busy window related to the precise analysis

Proof of correctness of the workload bound within a queueing prefix related to the precise analysis

Proof of correctness of the workload bound within a busy window related to the approximate analysis

Proof of correctness of the workload bound within a queueing prefix related to the approximate analysis

IV.5. Analysis

Busy window

Definition of busy interval  (from Prosa)

Definition of queueing prefix

Response time analysis

Proof of correctness of the generic response time analysis by abstracting the type of candidates

Proof of correctness of the precise analysis (Related to Theorem 1 in the paper)

Proof of correctness of the approximate analysis (Related to Theorem 2 in the paper)

Proof of correctness of the implementation for computing the precise result

Proof of correctness of the implementation for computing the approximate result

Algorithm of the combined analysis

Proof of correctness of the combined analysis (Related to Theorem 3 in the paper)

Algorithm of the result certification (CertiCAN)

Proof of correctness of the result certification (Related to Theorem 4 in the paper)

V. Experimental evaluation

After having completed the proofs, we can use the Coq extraction technique to automatically generate four Ocaml tools. They can be found in the files CAN_analyzer_offset.ml(i) in the directory certican-v0.1/Ocaml-tools. They contain the following functions:

• analyzer_rt_precise (AP): the analyzer based on the precise analysis
• analyzer_rt_appro (AA): the analyzer based on the approximate analysis
• analyzer_rt_combined (AC): the analyzer based on the combined analysis
• certican: the certifier of CAN analysis results (response times)

These files can also be re-extracted by uncommenting the last line of the file analyzers_all_fp.v (i.e. remove characters “(*” and “*)”) and executing make inside certican-v0.1/Coq-source. The new files will be generated in the directory certican-v0.1/Coq-source/analysis/uni/offset.

The Coq extraction technique is used for building certified functional programs by extracting them from the verified Coq functions or specifications.

Because the functional programs has been kept simple (unoptimized) to facilitate their certification, they require a large stack and memory to compute. So, you may need to increase the stack size and the memory size (if your computer allows).

Set the stack size unlimited
$ ulimit -s unlimited
Check the stack size
$ ulimit -s

Note that this setting is temporary; you have to reset it once you exit the Terminal

The folder certican-v0.1/Experiment contains the following directories and files:

• Example/:  contains a small example for testing the four extracted Ocaml tools;
• Example-CertiCAN/:  contains an example for testing certican only;
  
• MyGenerator/:  contains the source code of a CAN system generator;
• data-fig*/: used for saving the computed results for Fig.{3, 4, 5 ,6} of the paper (inside data-fig*, the format of the corresponding result can be seen in the file readme);
  
• system_f*/:   contains a collection of systems analyzed by RTaW-Pegase for Fig.5 & 6 of the paper;
  
• CAN_analyzer_offset.ml and .mli: these 2 extracted files contain the extracted tools (copied from certican-v0.1/Ocaml-tools);
• other *.ml: files that are used to call the extracted Ocaml tools;
  
• *.sh: bash files that are used to compile the above *.ml/mli files and run those tools.

V.1. Examples

Ex.1

A small example for testing the three analyzers and certican can be found in the directory certican-v0.1/Experiment/Example.

• system_test.ml contains a system to be analyzed;
• CAN_analyzer_offset.ml and .mli contain the extracted tools (copied from certican-v0.1/Ocaml-tools);
• program_test.ml contains a program used to test these tools.

Execute the following bash file to test them.
$ ./prog_oneTime_test.sh

This command compiles the *.ml and *.mli files then calls the four different tools to analyze the system from system_test.ml.

After a few seconds, the results should appear:

#trans	#tasks/trans	AA run time (s)	AP run time (s)	AC run time (s)	certican run time (s)	certified result
3	6	xxx	xxx	xxx	xxx	true*

*: When the result to certify is greater than or equal to the result computed by AP, certican returns true; otherwise false. In this example, because the input of certican is set as the result computed by AP, obviously it is true.

Meanwhile, three files (precise_test.txt, appro_test.txt, combined_test.txt) containing the computed results have been generated in the current directory.

Ex.2

Another example for testing certican alone is available in the directory certican-v0.1/Experiment/Example-CertiCAN.

• result contains the result computed by AP for the system presented in system_test.ml

Execute the following bash file to test certican.
$ ./certican.sh

This command compiles the *.ml and *.mli files then calls certican to verify the result (from the file result) for the system system_test.ml.

The format of the output is of the form:

run time | true/false | the id of the first detected task which is associated with a false result (0 when there is no false result)

You may increase/decrease the value inside the file result and observe the output change.

V.2. System generator

In order to evaluate our tools, we provide a system generator which is able to generate CAN systems for the following configurations:

Payload	1 – 8 bytes
Period	{20, 50, 100, 200, 500}
Offsets	{10, 20, …, 500}
Priority	unique, arbitrary distribution
Transmission speed	500 kbit/s

Obtain the executable file of this generator by executing

$ make

in the directory certican-v0.1/Experiment/MyGenerator.

A system of x transactions and y tasks in each transaction can be generated by running the following command:
$ ./generator x y

A file Generator.ml containing that system will be generated after running that command.

Additionally, you can obtain a file x-y.csv containing that system with the format of the RTaW-Pegase input file by adding “0” following the above command. I.e.,
$ ./generator x y 0

 

V.3. Evaluation

Note that the following procedure cannot produce exactly the same results as the ones in the paper but the observed trends should be the same.  The results (which are execution times) cannot be exactly the same for the following reasons: 1)  Executing the code in a VM is much less efficient compared to the direct execution on a physical machine. 2) Since paper submission, some optimizations have been performed (and certified). The analyses and certican are now slightly more efficient than at submission time. 3) Systems used for the Fig.3 and Fig.4 are randomly generated at each test.

Still, the trends that you observe should be the same as those in the figures shown in the paper and also here.

• Fig.3 presents the comparison between the three certified analyzers in term of execution times (Pass to the next step if you prefer to have the results of Fig.3 and Fig.4 together): For systems used in this figure, we fix the number of transactions to 5 and vary the number of tasks in each transaction from 1 to 25. The trend of the result can be obtained by executing the following command in the directory certican-v0.1/Experiment
  $ ./prog-fig3.sh
  This command will take around 40 minutes¤ to terminate and its results will be saved in the *.txt files of the sub-directory data-fig3. In this experiment, we generate one system per number of tasks (as specified by the parameter  “number = 1” in the file prog-fig3.sh). To obtain the same number of systems as in Fig.3 (10 for each number of tasks from 1 to 25), “number = 1” must be replaced by “number = 10” (but it results in longer running times: ~ 3 hours).
• (Fig.3 and) Fig.4 presents the comparison between the precise analyzer and the combined analyzer in terms of number of precise scenarios evaluated: For systems used in this figure, we fix the number of transactions to 5 and vary the number of tasks in each transaction from 1 to 25. To obtain the trend of the result, we need to manually add some counters inside the 2 extracted files (CAN_analyzer_offset.ml and .mli) to count the number of performed scenarios. So you need to replace these 2 files by the files with the same name found in the directory certican-v0.1/Ocaml-tool/With-counters before running the following command:
  $ ./prog-fig34.sh
  This command will take up to 40 minutes to terminate¤ and its results will be stored in the *.txt files of the sub directory data-fig34. The number of systems generated for each number of tasks can be set by updating “number = 1” in the file prog-fig34.sh. To obtain the same number of results as in Fig.4 in the paper, it must be set to 10 (it results in longer running times: ~ 3 hours).
• Fig.5 and Fig.6: We need the commercial tool RTaW-Pegase to fully reproduce the results of Fig 5 and Fig 6. Unfortunately, the tool cannot be installed on a VM and RTaW cannot grant academic licenses to anonymous users. Furthermore, we only have a license on a laptop which cannot be remotely accessed. In order to reproduce the results of Fig 5 and Fig 6 (more on this below), we have therefore generated a set of systems that we analyzed with RTaW-Pegase, which can be found in the directory system_fig5 for Fig.5 and system_fig6 for Fig.6 respectively. In these two directories, there are three kinds of files:
  • system-x-y-z.ml: system of x transactions and y tasks in each transaction. The variable z is used for numbering the systems of the same size;
  • rtaw-result-x-y-z.txt: results performed by RTaW-Pegase for that system;
  • rtaw-runtime-x-y-z.txt: a value representing the time used for analyzing that system by RTaW-Pegase.
• In the files prog-fig5.sh and prog-fig6.sh we have set the number of systems to one (“number = 1“) by default for shorter running times.:
  • Fig.5 presents the comparison between certican and RTaW-Pegase in terms of execution times: For systems used in this figure, we fix the number of transactions to 5 and vary the number of tasks in each transaction from 1 to 40.
    $ ./prog-fig5.sh
    This command will take several minutes¤ and the result will be saved in the directory data-fig5.
  • Fig.6 presents the execution times of certican for 2 sets of systems: The first set contains 50 systems of 10 transactions and 10 tasks in each transaction; the other set contains 50 systems of 10 transactions and 15 tasks in each transaction.
    $ ./prog-fig6.sh
    This command takes several seconds up to 1.5 hours¤ and its result is stored in the directory data-fig6.

To get the same number of results as in Fig.5 and Fig.6, one must set  “number = 10” in the file prog-fig5.sh and  “number = 50” in the file prog-fig6.sh respectively (long execution times should be expected: ~ 20 minutes and 10 hours respectively).

As mentioned earlier, the computation of Fig. 5 and Fig.6 presented above is a little different from that of the paper. In the paper, we used RTaW-Pegase directly to analyze systems and then to certify the results. Here, we collected and stored a set of systems arbitrarily generated by our generator and analyzed by RTaW-Pegase. If you would like to test certican on other systems, you may proceed as follows:

1. Generate a set of systems using our generator. E.g., generate a system of 10 transactions and 10 tasks in each transactions by running the following command:
   $ MyGenerator/generator 10 10 0
   2 files will be generated after running the above command:
   • Generator.ml: an Ocaml file contains the system generated (this file needs to be stored and will be used in the 4th step)
   • 10-10.csv: a file contains the system generated with the format of RTaW-Pegase input file
2. Then, to get the results analyzed by RTaW-Pegase for those systems, send them (i.e., 10-10.csv) to the AE chair, Alessandro Biondi, who will contact the company RTaW and obtain the analysis results computed by RTaW-Pegase. The results (10-10_WorstCaseAnalysis.csv) will be sent back to you via the AE chair.
3. Extract the corresponding results from 10-10_WorstCaseAnalysis.csv and store them in rtaw-results-10-10.txt
   $ grep -o -P '(?<=system;).*?(?=;)' "10-10_WorstCaseAnalysis.csv"|
tr ',' '.' > rtaw-results-10-10.txt
4. Use certican to verify the results computed by RTaW-Pegase.
   $ ocamlopt -o run CAN_analyzer_offset.mli CAN_analyzer_offset.ml Generator.ml rtaw_certifer_f6.ml && ./run

¤: Time measured in the VM installed on a 64bits, Intel i7, 2.6GHz, 8Gb laptop.

Notes

• In the extraction process, we extract by default natural numbers of Coq (nat) into the Ocaml integers (63 bits on a 64 bits system are able to express values up to 4611686018427387903 which is more than enough for our applications). Natural numbers could also be extracted to Ocaml big integers (big_int) by uncommenting the corresponding lines at the end of analyzers_all_fp.ml. Ocaml big_int can represent integers of arbitrary size.
• Potentially, “out of memory” may occur in the terminal output if you do not allocate enough memory for the VM.
• In the RTaW-Pegase analysis process, an exception will occur if the utilization of a system to analyze exceeds 1. Therefore those systems with a utilization greater than 1 are skipped automatically and will not be stored in our collections. Specifically, for Fig.5, such systems are skipped in the directory system_fig5.