search

pok-kernel / pok

POK kernel. Safe and secure for safety-critical systems.
https://pok-kernel.github.io/
BSD 2-Clause "Simplified" License
94 stars 61 forks source link

Can't run examples #24

Open syrba4eva opened 3 years ago

syrba4eva commented 3 years ago

Hi! I've installed POK on Ubuntu 18.04.4 and try to run the examples. Unfortunately I get an error when I try to run any example except of "semaphores":

olga@olga-H270M-DS3H:~/pok/examples/partitions-scheduling$ make all Makefile:4: /misc/mk/examples.mk: No such file or directory make: *** No rule to make target '/misc/mk/examples.mk'. Stop.

"semaphore" example works well and I'm not sure where is the problem. I'm also not very experienced with Ubuntu. Any help would be highly appreciated.

leonhxx commented 3 years ago

I also have this problem

yoogx commented 3 years ago

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

leonhxx commented 3 years ago

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];

wenting83 commented 3 years ago

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

XingZYu commented 2 years ago

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

First, this is the code generation error given by ocarina

```shell 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

Thank you

tfinnegan937 commented 2 years ago

@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.

Etienne13 commented 2 years ago

@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.