Prepare Multitasking Code - R2014b

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();

Answer 1

[Alexandre De Barros]

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

Answer 2

[Alexandre De Barros]

Hello Daniel,

1) Talking about probability doesn't make sense in the case of formal tools like Polyspace, since there is no execution of the code. Follow this link for more information on how Polyspace works and the power of abstract interpretation: http://www.mathworks.com/discovery/abstract-interpretation.html

2) a volatile variable will be considered "always full-range" by Polyspace (by the way this is the nature of a volatile variable!). The code is not instrumented (again, there is no execution) and Polyspace will simply consider that for the 'if (random)' statements, the if can be true or not. And because random is volatile, Polyspace will also consider that the two values of random can be different for each statement.

Hope that helps!

Last but not least, these topics are covered in the Polyspace trainings.

Best regards,

Alex

[Daniel Popu]

Hello Alex,

Thanks for your attempt to answer.

If I read Polyspace help I can easily assume that the code is executed. See the below a snap shot from R2014b help:

"Polyspace® requires that before tasks begin, the main function has completed execution."

OK, Polyspace do not run code. However, my first question is still not yet answered.

I would appreciate, if possible, a straight answer to my first question.

All the best, Daniel