Can't run examples about pok HOT 7 OPEN

I also have this problem

from pok.

From the error messages, it is likely that the makefile is using an env. variable that is missing

from pok.

From the error messages, it is likely that the makefile is using an env. variable that is missing

thanks, I make a mistake... we need to set "export POK_PATH=/where/you/have/the/pok/sources" again. but after set the environment and installed ‘ocarina-2017.1-suite-linux-x86_64-20170204’, I still can't compile example/case-study-osadl11,with the error message:
pok/kernel/include/core/sched.h:26:33: error: ‘POK_CONFIG_NB_PROCESSORS’ undeclared here (not in a function)
extern uint32_t current_threads[POK_CONFIG_NB_PROCESSORS];

from pok.

pok/kernel/include/core/sched.h:26:33: error: ‘POK_CONFIG_NB_PROCESSORS’ undeclared here (not in a function)
extern uint32_t current_threads[POK_CONFIG_NB_PROCESSORS]; the same

from pok.

Hi,
I found the same issue running example examples/partitions-threads and I tried various ways to solve it by myself.

• Pok version: git branch origin/main with commit 8bda891
• Ocarina version: Ocarina v2021.1-7-g563ae64 (Working Copy from r563ae649)
• System info: gcc version 9.3.0 (Ubuntu 9.3.0-17ubuntu1~20.04)

Check compliance of Health Monitoring service for modules............. validated 
Check that connections support appropriate security levels (MILS)..... validated 
Check Partitions Memory requirements.................................. validated 
Check error coverage.................................................. validated 
Check for permanent errors between partitions......................... validated 
Check that each virtual bus with a different security level has a different cipher key validated 
Check that each virtual bus provides protection mechanisms............ validated 
Check Biba security policy............................................ validated 
Check that virtual processors contain virtual buses................... validated 
Check that partition component share the same memory level............ validated 
Check that AADL model contain memory components....................... validated 
Check Threads Memory requirements..................................... validated 
Check Bell-Lapadula security policy................................... validated 
Check that each partition is executed at least one time by the module. validated 
Check that buses provides virtual buses............................... validated 
Check compliance of Health Monitoring service for partitions.......... validated 
Check compliance of Health Monitoring service for partitions processes validated 
Check for transient errors between partitions......................... validated 
Check Major Time Frame compliance..................................... validated 
Check that partitions declare their criticality level................. validated 
Will execute ocarina -aadlv2 -f -g pok_c model.aadl $POK_PATH/misc/aadl-library.aadl 
model.aadl:91:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
model.aadl:91:04: Warning: The value of source_language has been converted into a list.
model.aadl:98:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
model.aadl:98:04: Warning: The value of source_language has been converted into a list.
model.aadl:105:04: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
model.aadl:105:04: Warning: The value of source_language has been converted into a list.
aadl-library.aadl:406:04: Warning: Source_Language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
aadl-library.aadl:406:04: Warning: The value of Source_Language has been converted into a list.
Backends: error : Compute execution time not declared
Backends: warning : generated-code already exists
Compile node cpu (generated-code/cpu)

You have to add a missing line

compute_execution_time => 1ms .. 2ms;

in model.aadl

After that, when it proceed to compile, the aforementioned same error still occurs

Compile node cpu (generated-code/cpu)
In file included from ../..//kernel/include/arch.h:113,
                 from partition.c:21:
../..//kernel/include/arch/x86/spinlock.h:22:22: error: ‘POK_CONFIG_NB_PROCESSORS’ undeclared here (not in a function); did you mean ‘POK_CONFIG_NB_NODES’?
   22 | extern int spinlocks[POK_CONFIG_NB_PROCESSORS];
      |                      ^~~~~~~~~~~~~~~~~~~~~~~~
      |                      POK_CONFIG_NB_NODES
make[4]: *** [../..//misc/mk/rules-common.mk:50: partition.o] Error 1
make[3]: *** [Makefile:41: core/core.lo] Error 2
make[2]: *** [/mnt/data/Courses/EI6701/pok/misc/mk/rules-kernel.mk:22: /mnt/data/Courses/EI6701/pok/kernel/pok.lo] Error 2
make[1]: *** [Makefile:12: build-kernel] Error 2
Code generation failed
make: *** [/mnt/data/Courses/EI6701/pok/misc/mk/examples.mk:7: build] Error 1

However, examples that don't use generated code to compile can run without problem, e.g. examples/semaphores

I check the generated code, POK_CONFIG_NB_NODES is defined in generated_code/cpu/kernel/deployment.h, and this macro is not recognized by current version of pok kernel. So it seems that ocarina is using a older veresion of pok-kernel to generate code according to model.aadl and it causes conflicts.

My question is

• Is there a stable version of pok + ocarina combination that we can use to correctly run the examples, more generally, use AADL code generation without errors?
• Or what should we change in pok source to make these examples work?
  @Etienne13 @yoogx

Thank you

from pok.

@yoogx @Etienne13 I am also running into this particular issue. The generated code is missing several macros.

I went into generated-code\kernel\deployment.h and added the following line
#define POK_CONFIG_NB_PROCESSORS 1

Upon doing so, it moved past the error in @XingZYu 's issue above, and produced the following error:

`[CC] multiprocessing.c multiprocessing.c:20:43: error: ‘POK_CONFIG_PROCESSOR_AFFINITY’ undeclared here (not in a function)
20 | uint64_t partition_processor_affinity[] = POK_CONFIG_PROCESSOR_AFFINITY;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
make[4]: *** [../..//misc/mk/rules-common.mk:50: multiprocessing.o] Error 1
make[4]: Leaving directory '/home/c115360/Desktop/pok/kernel/core'
make[3]: *** [Makefile:41: core/core.lo] Error 2
make[3]: Leaving directory '/home/c115360/Desktop/pok/kernel'
make[2]: *** [/home/c115360/Desktop/pok/misc/mk/rules-kernel.mk:22: /home/c115360/Desktop/pok/kernel/pok.lo] Error 2
make[2]: Leaving directory '/home/c115360/Desktop/pok/examples/partitions-threads/generated-code/cpu/kernel'
make[1]: *** [Makefile:12: build-kernel] Error 2
make[1]: Leaving directory '/home/c115360/Desktop/pok/examples/partitions-threads/generated-code/cpu'
make: *** [Makefile:2: all] Error 2

`

As such, I believe it likely that the code generation libraries are broken in some way.

from pok.

@tfinnegan937 I believe ocarina for pok is broken in some way. As I am not a developer of Ocarina, I cannot provide support for this.

As I wrote in issue#32, some of pok examples should work with RAMSES (see this comment).

You will need to

1. Install OSATE.
2. From OSATE, install RAMSES (Menu Help --> Install additional OSATE components --> RAMSES).
3. From OSATE, import the AADL projects added to pok examples (Menu File --> Import --> General --> existing projects into workspace ... then select pok/examples to see available projects for OSATE).

More documentation on RAMSES here.

from pok.