MATLAB: Prepare Multitasking Code – R2014b

multitasking r2014b random volatile preparation codePolyspace Code ProverPolyspace Code Prover Server

Hello,
In the help of Polyspace R2014b I found for "Prepare Multitasking Code" the below piece of code:
 void upper_approx_C_sequencer(void)
 {
   volatile int random;
   while(1){
    if (random) tsk_10ms();
    if (random) tsk_30ms();
    if (random) tsk_50ms();
    ...
   }
 }
I have 2 questions:
1) Shouldn't actually be something like below?
    ...
    if (random > 0) tsk_10ms();
    ...
In your example the probability to call the function tsk_10ms() is
p_call = ("Nr. of values in int range" - 1) / "Nr. of values in int range" = 1 (approximately)
While the probability to not call the function tsk_10ms() is
p_NoCall = 1 / "Nr. of values in int range" = 0 (approximately)
If the intention is to have the same probability for calling and for not calling the function than we should use a solution similar to what I proposed.
If this is not the case, could you please explain why?
2) I read that Polyspace for volatile variables it can give them any value from the range of the variable. I want to know how this is performed, especially for the code used in multitasking, like the one above. Is Polyspace instrumenting the code? For example between the below lines it introduces others which give to the "random" variable a random value?
    if (random) tsk_10ms();
    if (random) tsk_30ms();

Best Answer

Hi Daniel!
The word "execution" should not be interpreted as a real (and dynamic) execution. The wikipedia page about abstract interpretation talks about "partial execution". Maybe "abstract execution" would describe this process better. This sentence of the documentation just means that the end of the main should be reached in this abstract execution. If there is a red error, the main is indeed not completly verified since Polyspace can not continue the verification after a red check. And when the main is not completly verified, the tasks are not "launched". The power of abstract interpretation is that it is similar to an execution, this is why use the same words (execution, launched,...) but we are still in a formal domain. And for your first question, again since there is no random values for the 'if', we can't talk about probability. Ranges are used instead of discrete values, and Polyspace propagates these ranges in this abstract execution.
Regards
-- Alex
Related Question