OIL files selection (-osek-multitasking) - Set up multitasking configuration from OIL file definition

Description

Specify the OIL files that Polyspace^® parses to set up the multitasking configuration of your OSEK project.

Set Option

Set the option using one of these methods:

Polyspace user interface (desktop products only): In your project configuration, select the Multitasking node and then select this option. See Dependencies for other options you must enable first.
Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Multitasking node and then select this option. See Dependencies for other options you must enable first.
Command line and options file: Use the option -osek-multitasking. See Command-Line Information.

Why Use This Option

If your project includes OIL files, Polyspace can parse these files to set up tasks, interrupts, cyclical tasks, and critical sections. You do not have to set them up manually.

Settings

Off (default): Polyspace does not set up a multitasking configuration for your OSEK project.
On: Polyspace looks for and parses OIL files to set up your multitasking configuration.
auto: Look for OIL files in your project source and include folders, but not in their subfolders.
custom: Look for OIL files on the specified path and the path subfolders. You can specify a path to the OIL files or to the folder containing the files.

When you select this option, in your source code, Polyspace supports these OSEK multitasking keywords:

TASK
DeclareTask
ActivateTask
DeclareResource
GetResource
ReleaseResource
ISR
DeclareEvent
DeclareAlarm

Polyspace parses the OIL files that you provide for TASK, ISR, RESOURCE, and ALARM definitions. The analysis uses these definitions and the supported multitasking keywords to configure tasks, interrupts, cyclical tasks, and critical sections.

To see how Polyspace models the TASK, ISR, and RESOURCE definitions from your OIL files, open the Concurrency window from the Dashboard pane.

Polyspace uses this decision tree to determine whether a task is an entry point or a cyclic task:

Task is entry point or cyclical decision tree

Example: Analyze Your OSEK Multitasking Project

This example shows how to set up the multitasking configuration of an OSEK project and run an analysis on this project. To try the steps in this example, use the demo files in the folder polyspaceroot/polyspace/examples/doc_cxx/External_multitasking/OSEK or polyspaceroot/polyspace/examples/doc_cxx/External_multitasking/OSEK. polyspaceroot is the Polyspace installation folder. The analysis results apply to this example code.

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3; 

DeclareAlarm(Cyclic_task_activate);
DeclareResource(res1);
DeclareTask(init);
TASK(afterinit1);

TASK(init) // task
{
 
  
  var2++;
  ActivateTask(afterinit1);  
  var3++;
  GetResource(res1); // critical section begins
  var1++;
  ReleaseResource(res1); // critical section ends
}

TASK(afterinit1) // task
{
  var3++;
  var2++;
  GetResource(res1); // critical section begins
  var1++;
  ReleaseResource(res1); // critical section ends

}
int var4; 
void func()
{
  var4++; 
}

TASK(Cyclic_task) // cyclic task
{
  func();
}

void main()
{}

To set up your multitasking configuration and analyze the code:

Copy the contents of polyspaceroot\polyspace\examples\doc_cxx\External_multitasking\OSEK to your machine, for instance in C:\Polyspace_worskpace\OSEK.

Run an analysis on your OSEK project by using the command:

Bug Finder:

polyspace-bug-finder -sources ^
C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^ 
-osek-multitasking auto

Code Prover:

polyspace-code-prover -sources ^
C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^
-osek-multitasking auto

Bug Finder Server:

polyspace-bug-finder-server -sources ^
C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^ 
-osek-multitasking auto

Code Prover Server:

polyspace-code-prover-server -sources ^
C:\Polyspace_workspace\OSEK\example_osek_multitasking.c ^
-osek-multitasking auto

Bug Finder detects a data race on variable var3 because of multiple read and write operation from tasks init and afterinit1. See Data race.

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3;

There is no defect on var2 since afterinit1 goes to an active state (ActivateTask()) after init increments var2. Similarly, there is no defect on var1 because it is protected by the GetResource() and ReleaseResource() calls.

Code Prover detects that var3 is a potentially unprotected global variable because it is used in tasks init and afterinit1 with no protection from interruption during the read and write operations. The analysis also shows that the cyclic task operation on var4 can potentially cause an overflow. See Potentially unprotected variable and Overflow.

#include <assert.h>
#include "include/example_osek_multi.h"

int var1; 
int var2; 
int var3;

...
void func()
{
  var4++;
}

Variable var2 is not shared because afterinit1 goes to an active state (ActivateTask()) after init increments var2. Variable var1 is a protected variable through the critical sections from the GetResource() and ReleaseResource() calls.

Additional Considerations

Make sure that you declare all tasks by using the DeclareTask or TASK keywords before you pass those tasks as parameters to functions or macros that expect a task. For example , if you pass task foo to ActivateTask without using DeclareTask(foo); first, Polyspace considers task foo undefined which results in a compilation error.
The analysis ignores TerminateTask() declarations in your source code and considers that subsequent code is executed.
Polyspace ignores syntax elements of your OIL files that do not follow the syntax defined here.
This option is supported only for projects that use C code.

Dependencies

To enable this option in the user interface of the desktop products:

Set the value of the option Source code language (-lang) to C.
Select the value osek for the option External multitasking configuration (renamed to External file for multitasking in the Polyspace Platform user interface).

Command-Line Information

Parameter: -osek-multitasking

Value: auto |

custom='file1 [,file2,
                        dir1,...]'

Default: Off

Example (Bug Finder):

polyspace-bug-finder -sources source_path -I
                        include_path -osek-multitasking
                    custom='path\to\file1.oil, path\to\dir'

Example (Code Prover):

polyspace-code-prover -sources source_path -I
                        include_path -osek-multitasking
                    custom='path\to\file1.oil, path\to\dir'

Example (Bug Finder Server):

polyspace-bug-finder-server -sources source_path
                    -I include_path -osek-multitasking
                    custom='path\to\file1.oil, path\to\dir'

Example (Code Prover Server):

polyspace-code-prover-server -sources
                        source_path -I
                        include_path -osek-multitasking
                    custom='path\to\file1.oil, path\to\dir'

OIL files selection (`-osek-multitasking`)