Home

POK User Guide

1. pe ej time management services xy prre J extern void TIMED WAIT in SYSTEM TIME TYPE delay time out RETURN CODE TYPE return code D c M extern void PERIODIC WAIT out RETURN CODE TYPE return code p e extern void GET TIME out SYSTEM TIME TYPE system time out RETURN CODE TYPE return code y rcc A eee ee ee IE Ea SPP sa S void REPLENISH SYSTEM_TIME_TYPE budget_time RETURN_CODE_TYPE return_c Uu Top voor NE endif endif CHAPTER 8 POK API 67 8 2 4 Error handling ifdef POK NEEDS ARINC653 ERROR ifndef APEX ERROR define APEX ERROR ifndef POK NEEDS ARINC653 PROCESS define POK NEEDS ARINC653 PROCESS 1 endif include lt arinc653 process h gt include lt arinc653 types h gt define MAK ERROR MESSAGE SIZE 64 typedef APEX INTEGER ERROR MESSAGE SIZE TYPE typedef APEX BYTE ERROR MESSAGE TYPE MAX ERROR MESSAGE SIZE enum ERROR CODE VALUE TYPE DEADLINE MISSED APPLICATION_ERROR NUMERIC_ERROR ILLEGAL_REOUEST STACK_OVERFLOW MEMORY_VIOLATION HARDWARE_FAULT POWER_FAIL Wa we GO BO H O typedef enum ERROR_CODE_VALUE_TYPE ERROR_C
2. 75 in SAMPLING_PORT_ID_TYPE SAMPLING_PORT_ID in MESSAGE_ADDR_TYPE MESSAGE_ADDR by refere in MESSAGE_SIZE_TYPE LENGTH out RETURN CODE TYPE RETURN CODE extern void READ SAMPLING MESSAGE in SAMPLING PORT ID TYPE SAMPLING PORT ID out MESSAGE ADDR TYPE MESSAGE ADDR out MESSAGE SIZE TYPE LENGTH out VALIDITY TYPE VALIDITY out RETURN CODE TYPE RETURN CODE extern void GET SAMPLING PORT ID in SAMPLING PORI NAME TYPE SAMPLING PORT NAME out SAMPLING PORT ID TYPE SAMPLING PORT ID out RETURN CODE TYPE RETURN CODE extern void GET SAMPLING PORT STATUS in SAMPLING PORT ID TYPE SAMPLING PORT ID out SAMPLING PORT STATUS TYPE SAMPLING PORT STATUS out RETURN CODE TYPE RETURN CODE endif endif 8 3 ARINC653 Ada Since partitions can also be written in Ada an ARINC653 Ada layer APEX is available It is just a binding to the C implementation which files can be found in libpok ada arinc653 Although the binding is complete Health monitoring Module schedules and a few other functions are not yet available in the C API Simply use with APEX xxx in your source to use the xxx ARINC module 8 3 1 APEX types and constants This is a compilable Ada 95 specification for the APEX interface derived from section 3 of ARINC 653 The declarations of the services given below are taken from the standard as are the enum
3. 500ms 500ms 500ms 500ms Allocation gt reference partitionl reference partiti x86 gemu four partitions ementation pok kernel x86 gemu four partitions with libmath virtual processor poklib pok partition basic for exampl f t t n2 reference kernel x86_qemu t t n2 reference partitions partition3 extends pok kernel x86 qem with libmath virtual processor poklib pok partition basic for exampl with libmath virtual processor poklib pok partition basic for exampl with libmath 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 CHAPTER 10 ANNEXES partition4 96 virtual processor poklib pok partition basic for exampl with libmath properties POK Major Frame gt 2000ms POK Scheduler gt static POK Slots gt 500ms 500ms 500ms 500ms POK Slots_Allocation gt reference partitionl reference end pok_kernel x86_qemu_four_partitions_with_libmath Unclassified virtual bus virtual bus unencrypted end unencrypted virtual bus implementation unencrypted i properties POK Protocol end unencrypted i unknown blowfish virtual bus subprogram blowfish send fea
4. 100 List of Figures 4 1 7 1 7 2 7 3 Model Based development process 14 Thedifferentpoklayerss 37 Build steps for a partitionedsystem 38 ELF file format of a POK system 38 Chapter 1 Introduction 1 1 What is POK POK is a kernel dedicated to real time embedded systems This kernel works on vari ous architectures The configuration code the deployment code as well as the applica tion userland code can be automatically generated achieving zero coding approach One main goal of POK is to be compliant with many industrial standards In the embedded domain many API exist for different application domains avionics railway automotive However concepts remain the same POK proposes a canonical adaptive kernel compliant with several industrial standards 1 2 Purpose of this document This document provides general information about POK It also present available API describes them and detail how to configure the kernel 1 3 Supported platforms At this time POK supports the following platforms e x86 emulation with QEMU e PowerPC e Leon3 a platform for aerospace applications 1 3 4 x86 The x86 support is included to rapidly develop applications and test them into an emu lator like QEMU or bochs CHAPTER 1 INTRODUCTION 7 1 3 2 PowerPC A PowerPC port is available The port is available for the following BSP e prep
5. abstract implementation vbus des wrapper i subcomponents send subprogram des send i receive subprogram des receive i marshalling type data des data i end vbus des wrapper i virtual bus des end des virtual bus implementation des i properties Implemented As gt classifier poklib vbus des wrapper i POK Protocol gt des end des i ceasar virtual bus subprogram ceasar send features datain in parameter poklib pointed void countin in parameter poklib integer dataout out parameter poklib pointed void countout out parameter poklib integer properties Source Name gt pok protocols ceasar marshall end ceasar send subprogram implementation ceasar send i end ceasar send i subprogram ceasar receive features datain in parameter poklib pointed void countin in parameter poklib integer dataout out parameter poklib pointed void countout out parameter poklib integer properties Source Name gt pok protocols ceasar unmarshall end ceasar receive subprogram implementation ceasar receive i end ceasar receive i data ceasar data end ceasar data data implementation ceasar data i properties Type Source Name gt pok protocols ceasar data t end ceasar data i abstract vbus ceasar wrapper end vbus ceasar wrapper 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288
6. define POK ERROR KIND PARTITION SCHEDULING 32 define POK ERROR KIND PARTITION PROCESS 33 define PO ERROR KIND KERNEL INIT 50 define PO ERROR_KIND_KERNEL_SCHEDULING 51 pok_ret_t pok error handler create void pok error ignore const uint32 t error id const uint32 t thread i void pok error confirm const uint32 t error id const uint32 t thread i pok ret t pok error handler set ready const pok error status t void pok error log const uint32 t error id const uint32 t thread id void pok error raise application error char msg uint32 t msg size pok error get returns POK ERRNO OK if the error pointer was registered and an error was registered It also returns POK ERRNO UNAVAILABLE if the pointer was not registered or if nothing was detected it pok_ret_t pok_error_get pok_error_status_t status endif 8 1 5 Inter partitions communication include lt core dependencies h gt tifndef POK LIBPOK PORTS H define POK_LIBPOK_PORTS_H include lt types h gt include lt errno h gt include lt core syscall h gt typedef enum POK_PORT_QUEUEING_DISCIPLINE_FIFO 1 POK_PORT_QUEUEING_DISCIPLINE_PRIORITY 2 pok_port_queueing_disciplines_t typedef enum POK_PORT_DIRECTION_IN L POK PORT DIRECTION OUT I N 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 5
7. Dispatch Protocol gt Periodic Compute Execution Time gt 0 ms 1 ms uld art O O JA un D i i i i im SOCMIDUNRWNE CHAPTER 10 ANNEXES Period gt 100 Ms end driver_rt18029_thread_poller thread implementation driver_rt18029_thread i connections port incoming_unclassified gt outgoing_unclassified port incoming_secret gt outgoing_secret port incoming_topsecret gt outgoing_topsecret end driver rt18029 thread i thread implementation driver rt18029 thread poller i calls calll pspg subprogram poll end driver rt18029 thread poller i process driver rt18029 process end driver rt18029 process process implementation driver rt18029 process i subcomponents thr thread driver rtl8029 thread i poller thread driver rtl8029 thread poller i properties POK Needed Memory Size gt 160 Kbyte end driver rt18029 process i abstract driver rt18029 end driver rt18029 abstract implementation driver rt18029 i subcomponents p process driver rt18029 process i end driver rt18029 i end rt18029 105 POK header The following file is a part of the POK project Any be made according to the POK licence You CANNOT use of a file for your own project For more information on the POK licence please see our LICENCE FILE Please follow the coding guidelines described in doc CODING GUIDELINES Copyright c 2007 2009 POK team Created by j
8. POK Additional Features libe stdio libo stalib end pok partition basic for example with libmath gt libmath consol amp memory pok memory end pok memory memory implementation pok memory x86 segment end pok memory x86 segment pok partition basic math extends pok partition 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 CHAPTER 10 ANNEXES memory implementation pok_memory x86_main end pok_memory x86_main thread thr_periodic properties Dispatch_Protocol Period Deadline Compute_Execution_Time end thr_periodic thread thr_sporadic properties Dispateh_Protocol Period Deadline Compute_Execution_Time end thr_sporadic subprogram spg_c properties Source Language Source Text end spg c data void properties gt Periodic gt 100ms 100ms gt 5ms 10ms gt Sporadic gt 100ms gt 100ms gt 5ms 10ms user functions Type_Source_Name gt void end void data implementation void i end void i data pointed_void properties Type_Source_Name gt void end pointed_void data implementation pointed_void i end pointed_void i data char properties 0 101 CHAPTER 10 ANN
9. truncf float x endif POK NEEDS LIBMATH 60 CHAPTER 8 POK API 61 8 1 9 Protocol functions ifndef __LIBPOK_PROTOCOLS_H__ define __LIBPOK_PROTOCOLS_H__ file libpok protocols protocols h author Julien Delange date 2009 brief Protocols to marshall unmarshall data This file is a general purpose file to include all protocols in the same time Protocols functions provides features to encode and decode messages before sending data through partitions It is especially useful when you want to encrypt data over the network before sending or adapt application data to a particular protocol For each protocol we have li One function to marshall data ii One function to unmarshall data x One data type associated with the crypto protocol This data type is used to store data when marshalling data and used as an input to unmarshall data More documentation is available in the user manual E jk The DES crypto protocol n include lt protocols des h gt The Blowfish crypto protocol tinclude lt protocols blowfish h gt The Ceasar crypto protocol L include lt protocols ceasar h gt tendif ifndef LIBPOK PROTOCOLS CEASAR H define LIBPOK PROTOCOLS CEASAR H file libpok include protocols ceasar h Nauthor Julien Delange date 2009 brief Ceasar crypto protocol CHAPTER 8 POK API
10. 56 57 58 60 61 62 63 64 65 66 67 68 69 70 71 72 73 D CHAPTER 10 ANNEXES 103 Application Error Numeric Error Illegal_Request Stack Overflow Memory Violation Hardware Fault Power Fail Supported_Recovery_Action type enumeration Ignore Confirm Partition Stop Module Stop Process Stop Process Stop And Start Another Process Restart Partition Restart Module Restart Nothing The difference between ignore and nothing is that ignore does not perform anything but logs the error On the contrary nothing will do nothing the HM CallBack should do everything Supported Access Type type enumeration read write read write Supported Memory Kind type enumeration memory data memory code HM Errors list of Supported Error Code applies to processor virtual processor thread HM Actions list of Supported Recovery Action applies to processor virtual processor thread HM Callback classifier Subprogram Classifier applies to thread virtual processor processor emory Kind Supported Memory Kind applies to memory Access Type Supported Access Type applies to memory Timeout Time applies to data port event data port event port access Supported DAL Type type enumeration LEVEL A LEVEL B LEVEL C LEVEL D DAL Supported DAL Type applies to virtual processor System Overhead Time Time applies to processor virtual processor
11. This is a very basic crypto protocol that just change the order of bytes in data There is no public private key the algorithm is known by the attaker so that it s a very weak crypto protocol Interested people can gather more information about this protocol on http en wikipedia org wiki Caesar_cipher We don t provide an associated marshalling type for the Ceasar protocol since the crypted size is the same than the uncrypted size include lt types h gt ifdef POK_NEEDS_PROTOCOLS_CEASAR Function that uncrypts data wa void pok protocols ceasar unmarshall void crypted data Function that encrypts data Wa void pok_protocols_ceasar_marshall void uncrypted data endif endif 62 pok_size_t crypted_size void pok_size_t unctypted_size ifndef __LIBPOK_PROTOCOLS_DES_H__ define __LIBPOK_PROTOCOLS_DES_H__ file libpok protocols des h Nauthor Julien Delange date 2009 brief DES protocol Implementation of the very basic DES crypto protocol This is a symetric crypto protocol with a shared key so that receiver and sender share the same key More information at http en wikipedia org wiki Data Encryption Standard include lt types h gt void uncrypted_d crypted_d 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 CHAPTER 8 POK API 63
12. private type Partition ID Type is new APEX Integer Null Partition Id constant Partition Id Type 0 pragma Convention C Operating Mode Type pragma Convention C Start Condition Type pragma Convention C Partition Status Type POK BINDINGS pragma Import C Get Partition Status GET PARTITION STATUS pragma Import C Set Partition Mode SET PARTITION MODE END OF POK BINDINGS end APEX Partitions 8 3 8 Processes CHAPTER 8 POK API PROCESS constant and type definitions and management services package APEX Processes is ax Number Of Pro ax Lock Level subtype Process N ull Process Id subtype subtype subtype 0 Max Numbe subtype Priority Min Priority V type Process Stat type Deadline Typ type Process Attr Period Time Capacity Entry Point Stack Size Base Priority Deadline Name end record type Process Stat Deadline Time Current Prior Process State Attributes end record procedure Create Attributes Process Id Return Code procedure Set Pri Process Id Priority Return_Code procedure Suspend Time_Out Return_Code procedure Suspend Process_Id Return_Code procedure Resume Process_Id Return_Code procedure Stop_Se procedure Stop Process_Id Return_Code procedure Start Min_Priority_Value ax_Priority_Value 83 System_Limit_Number_Of_Processeg cesses constant constant 0 constant 249 constant 32 ame Type is Name Typ
13. 148 149 150 151 152 153 154 155 156 157 158 CHAPTER 8 POK API float double float double float double float double float double float int float double double float double float double float ifdef double else double endif Hifdef float else float endif double float double float double float double float double float double float double float double float double float double float endif logf float x log10 double x log10f float x log2 double x log2f float x logb double x logbf float x loglp double x loglpf float x ldexp double value int exp0 ldexpf float value int exp0 matherr struct exception x modff float x float iptr modf double x double iptr nextafter double x double y nextafterf float x float y pow double x double y powf float x float y remainder double x double y remainderf float x float y _SCALB_INT scalb double x int fn scalb double x double fn _SCALB_INT scalbf float x int tn scalbf float x float fn rint double x rintf float x round double x roundf float x scalbn double x int n scalbnf float x int n significand double x significandf float x sin double x sinf float x sinh double x sinhf float x sqrt double x grtf float x tan double x tanf float x tanh double x tanhf float x trunc double x
14. 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 CHAPTER 10 ANNEXES abstract implementation vbus_ceasar_wrapper i subcomponents send subprogram ceasar_send i receive subprogram ceasar_receive end vbus_ceasar_wrapper i virtual bus ceasar end ceasar virtual bus implementation ceasar i properties Implemented_As 2 classifier poklib POR Protocol gt gasari end ceasar i gzip virtual bus subprogram gzip_send features datain in parameter poklib pointed_void countin in parameter poklib integer dataout out parameter poklib pointed void countout out parameter poklib integer properties Source Name pok protocols gzip marshall end gzip send subprogram implementation gzip send i end gzip send i subprogram gzip receive features datain in parameter poklib pointed void countin in parameter poklib integer dataout out parameter poklib pointed void countout out parameter poklib integer properties Source Name gt pok protocols gzip unmarshall end gzip receive subprogram implementation gzip receive i end gzip receive i data gzip data end gzip data data implementation gzip data i properties Type Source Name gt pok protocols gzip data t end gzip data i abstract vbus gzip wrapper end vbus gzip wrapper abstract implementation vbus
15. 36 37 38 39 40 41 42 43 45 46 47 48 CHAPTER 8 POK API 81 Hardware_Fault Power_Fail type Error_Status_Type Error_Code Length Failed Process Id Failed Address Message end record procedure Report Application Message Message Addr in Message Addr Type Length in Message Size Type Return Code out Return Code Type procedure Create Error Handler Entry Point in System Address Type Stack Size in APEX Processes Stack Size Type Return Code out Return Code Type procedure Get Error Status Error Status out Error Status Type Return Code out Return Code Type procedure Raise Application Error is record Error Code Type Error Message Size Type APEX Processes Process Id Type System Address Type Error Message Type Error Code in Error Code Type Message Addr in Message Addr Type Length in Error Message Size Type Return Code out Return Code Type private pragma Convention C Error Code Type pragma Convention C Error Status Type end APEX Health Monitoring 8 3 6 Module schedules package APEX Module Schedules is type Schedule Id Type is private Null Schedule Id constant Schedule Id Type subtype Schedule Name Type is Name Type type Schedule Status Type is record Time Of Last Schedule Switch Current Schedule Next Schedule end record procedure Set Module Schedule Schedule Id in Schedule Id Type Return Code out Return Code Type procedure G
16. Buffer Status Buffer Id in Buffer Id Type Buffer Status out Buffer Status Type Return Code out Return Code Type private type Buffer Id Type is new APEX Integer Null Buffer Id constant Buffer Id Type 0 pragma Convention C Buffer Status Type POK BINDINGS pragma Import C Create Buffer CREATE BUFFER pragma Import C Send Buffer SEND BUFFER pragma Import C Receive Buffer RECEIVE BUFFER pragma Import C Get Buffer Id GET BUFFER ID pragma Import C Get Buffer Status GET BUFFER STATUS END OF POK BINDINGS end APEX Buffers 8 3 4 Events with APEX Processes package APEX Events is Max Number Of Events constant System Limit Number Of Events subtype Event Name Type is Name Type type Event Id Type is private Null Event Id constant Event Id Type type Event State Type is Down Up type Event Status Type is record Event State Event State Type Waiting Processes APEX Processes Waiting Range Type end record procedure Create Event Event Name in Event Name Type Event Id out Event Id Type 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 CHAPTER 8 POK API 80 Return_Code out Return_Code_Type procedure Set_Event Event Id in Event Id Type Return Code out Return Code Type procedure Reset Event Event Id in Event Id Type Return Cod
17. LONG INTEGER 64 bit signed He Se PAA General APEX types x E 52 AA AA AA typedef enum NO_ERROR 0 request valid and operation performed rd NO ACTION 1 status of system unaffected by request NOT AVAILABLE 2 resource required by request unavailable WA INVALID PARAM WA UU w invalid parameter specified in request 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 CHAPTER 8 POK API 65 time out tied up with request has expire PORT DIRECTION TYPE 64 bit signed integg4 INVALID CONFIG 4 INVALID MODE 5 request incompatible with current mode TIMED OUT 6 RETURN CODE TYPE define MAX_NAME_LENGTH 30 typedef char AME TYPE MAX NAME LENGTH typedef void SYSTEM ADDRESS TYPE typedef APEX BYTE ESSAGE ADDR TYPE typedef APEX INTEGER ESSAGE SIZE TYPE typedef APEX INTEGER ESSAGE RANGE TYPE typedef enum SOURCE 0 DESTINATION 1 typedef enum FIFO 0 PRIORITY 1 QUEUING_DISCIPLINE_TYPE typedef APEX_LONG_INTEGER SYSTEM_TIME_TYPE define INFINITE_TIME_VALUE EI endif 8 2 2 Partition management ifdef POK NEEDS ARINC653 PARTITION include lt arinc653 types h gt include lt arinc653 process h gt ifndef APEX_PARTITION define APEX_PARTITION define MAX_NUMBER_OF_PARTITIONS SYSTEM_LIMIT_NUMBER_OF typedef enum IDLE COLD_START WARM_START NORMAL OPERATING_MODE_TYP
18. NEEDS BUFFERS maccro to activate this service 2 Blackboard a shared memory space to store a data New instances of the data replace the older value We can store only one instance of the same data You need to define the POK NEEDS BLACKBOARDS maccro to activate this service 3 Events are used to synchronized tasks It corresponds to POSIX mutexes and conditions You need to define the POK NEEDS EVENTS maccro to activate this service 4 Semaphores counting semaphores as in the POSIX standard You need to define the POK NEEDS SEMAPHORES maccro to activate this service CHAPTER 7 ARCHITECTURE 44 7 4 3 Memory allocator POK also provides a memory allocator This memory allocator was designed to be de terministic and highly configurable You define the amount of memory for the memory allocator and the number of memory slices that can be allocated Consequently the memory allocator can be configured with different maccros The service is activated by defining the POK CONFIG NEEDS ALLOCATOR maccro Then the POK CONFIG ALLOCATOR MEMORY SIZE is used to specify the amount of memory dedi cated for the memory allocator Finally the POK CONFIG_ALLOCATOR_NB_SPACES spec ifies the number of spaces you can allocate with the memory allocator This memory allocator can be used with the legacy layer with the pok allocator allocate or pok allocator free functions or with the C library layer malloc free calloc 7 4 4 Mathemat
19. POK BINDINGS end APEX Processes 8 3 0 Queuing ports QUEUING PORT constant and type definitions and management services CHAPTER 8 POK API with APEX Processes package APEX Queuing_Ports is Max Number Of Queuing Ports constant System Limit Number Of Queuing Ports subtype Queuing Port Name Type is Name Type type Queuing Port Id Type is private Null Queuing Port Id constant Queuing Port Id Type type Queuing Port Status Type is record Nb Message Message Range Type Max Nb Message Message Range Type Max Message Size Message Size Type Port Direction Port Direction Type Waiting Processes APEX Processes Waiting Range Type end record procedure Create Queuing Port Queuing Port Name in Queuing Port Name Type Max Message Size in Message Size Type Max Nb Message in Message Range Type Port Direction in Port Direction Type Queuing Discipline in Queuing Discipline Type Queuing Port Id out Queuing Port Id Type Return Code out Return Code Type procedure Send Queuing Message Queuing Port Id in Queuing Port Id Type Message Addr in Message Addr Type Length in Message Size Type Time Out in System Time Type Return Code out Return Code Type procedure Receive Queuing Message Queuing Port Id in Queuing Port Id Type Time Out in System Time Type Message Addr in Message Addr Type The message address is passed IN although the
20. POK LIBMH include lt types h gt struct exception int type char name double argl double arg2 double retval i define define define define define FP_NAN FP_INFINITE FP_NORMAL FP_SUBNORMAL FP_ZERO Oem W D FL define define define define define define DOMAIN SING OVERFLOW UNDERF LOW TLOSS PLOSS O C 4 W D define fpclassify x sizeof x extern int extern int extern int __fpclassifyf float fpclassifyd double __fpclassify double acos double x float acosf float x double acosh double x float acoshf float x double asin double x float asinf float x double asinh double x float asinhf float x sizeof float long double fpclassifyf float x fpclassifyd d 48 49 50 52 53 54 55 56 57 sg 59 60 61 62 63 65 66 67 68 69 70 n 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 9 92 93 94 95 96 97 98 99 101 102 103 CHAPTER 8 POK API double float double float double float double float double float double float double float double float double float double float double float double float double float int int double float double float double float double float double float int int int int int int double float double float double float double float double float double float double atan double x a
21. TI 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 105 106 107 108 CHAPTER 8 POK API 52 const void data const pok port size t len const uint64 t timeout define pok port queueing status id status pok syscall2 POK SYSCALL MIDDLEWARE OUEUEING STATUS uint32 t id uint32 t status Similar to pok ret t pok port queueing status const pok port id t id x const pok port queueing status t status define pok port queueing id name id pok syscall2 POK SYSCALL MIDDLEWARE QUEUEING ID uint32 t name Similar to pok ret t pok port gueueing id char name pok_port_id_t id A endif ifdef POK_NEEDS_PORTS_SAMPLING Sampling port functions typedef struct pok_port_size_t size pok_port_direction_t direction uint64_t refresh bool_t validity lpok port sampling status t pok ret t pok port sampling create char name const pok port size t size const pok port direction t direction const uint64 t refresh pok port id t 1d pok_ret_t pok_port_sampling_write const pok_port_id_t adi const void data int32 t id CHAPTER 8 POK API 53 109 const pok_port_size_t len 110 111 pok ret t pok port sampling read const pok port id t id 112 void message 113 pok port size t len 114 bool t valid 115 116 define pok port sampl
22. binding between a port and a network interface is specified in the kernel configuration CHAPTER 7 ARCHITECTURE 43 Please note that in POK when you are using partitioning services device drivers are executed in partitions 7 3 5 Scheduling service The scheduling service schedules tasks and partitions according to their timing require ments It relies on the time service Partitions are scheduled using a cyclic scheduling algorithm Partitions threads are scheduled using a Round Robin RMS or other available scheduling algorithms 7 4 libpok services 7 4 1 Thread management Thread management consist in interfacing functions with the kernel It provides func tions to start suspend stop a thread It provides also locking services for mutexes semaphores and so on 74 2 Communication service Libpok provides two kind of communication services e Inter partition communication which consists in kernel interfacing functions to use kernel communication ports e Intra partition communication service which provides communication facili ties to communicate inside a partition In the following we detail intra partition communication services Intra partition communication service provides four communication patterns 1 Buffer thread send data New data are queued according to a specific queueing policy Items are dequeued when a task reads the buffer We can store several instance of the same data You need to define the POK
23. const uint64 t pok ret t pok port buffer status const pok buffer id t const pok buffer status t pok ret t pok buffer id char pok buffer id t tendif endif tendif id data len timeout 99 name size msg size discipline id id timeout data len id Status name id Events CHAPTER 8 POK API ifndef define POK_LIBPOK_EVENT_H POK_LIBPOK_EVENT_H include lt core dependencies h gt include lt types h gt include lt errno h gt 56 pok_ret_t pok_event_create pok_event_id_t id pok_ret_t pok_event_wait pok_event_id_t id const uint64_t timeou pok ret t pok event broadcast pok event id t id pok ret t pok event signal pok event id t id pok ret t pok event lock pok event id t id pok ret t pok event unlock pok event id t id tendif Semaphores ifndef POK KERNEL SEMAPHORE H define POK KERNEL SEMAPHORE H include lt core dependencies h gt ifdef POK_NEEDS_SEMAPHORES include lt types h gt include lt errno h gt define POK_SEMAPHORE_DISCIPLINE_FIFO 1 pok_sem_id_t const pok_sem_value_t const pok_sem_value_t const pok_queueing_discipline_t pok_ret_t pok_sem_create pok_ret_t pok_sem_wait pok_sem_id_t id uint64_t timeout pok_ret_t pok_sem_signal pok_sem_id_t id pok ret t pok sem id char name pok sem id t id pok ret t pok sem status pok sem id t id pok sem
24. currentsite examplemodel html Famil for more information about this initial model Note that we convert this model from AADLv1 to AADLv2 to make it working with Ocarina POK data arrays Test the use of array types and their use in communication with queuing ports Use AADL models to describe types data arrays2 Test the use of array types and their use with sampling ports Use AADL model to describe types esterel Use of a third party language as application layer In this case we use Esterel generated code Use AADL models e events Test the use of events ports between threads located in the same partition DO NOT use AADL models exceptions handled Test the exceptions catching recovery handlers Use AADL models heterogeneous partitions Define two partitions with different architectures Demonstrate that the build system can generate build and run different mod ules that have different architectures libmath Test the inclusion of the libmath library in the libpok layer Use AADL model lustre academic Test the inclusion of Lustre application code inside partition Use AADL models e middleware blackboard Test the use of blackboard service Use AADL mod els e middleware buffer Test the use of buffer service Use AADL models e middleware buffer timed Test the use of buffer service with timeout Use AADL models e middleware queueing Test the use of queuing port service Use AADL mod els CHAPTER 6 EXAMPL
25. designer in the verification of its architecture Our validation process is based on Ocarina and the REAL language which is a constraint language for the AADL Its quite similar than OCL language designed for UML except that is specific to AADL and thus makes easier the validation of AADL model You can have additional information about Ocarina and REAL on http www aadl telecom paristech fr With REAL the user defines one or several the orems that express what we want to check There is a list of the theorems used in the POK toolchain and what we verify 1 MILS requirements enforcements we check that each partition has one se curity level and connected partitions share the same security levels For that the underlying runtime and the connections should support appropriate security levels 2 Bell Lapadula and Biba security policies for connected partitions we check the Bell Lapadula and Biba security policies no read up write down With that we ensure that the architecture is compliant with strict security guidelines 3 Memory requirements we check that required size by a partition is less impor tant than the size of its bounded memory component In other words we check that the memory segment can store the content of the partition We also check that the requirements described on partitions are correct regarding their content threads subprograms size 4 Scheduling requirements Major Time Frame for each pro
26. different tasks but does not provide partitioning functionnalities or a partitioned architecture a kernel isolates tasks in so called partitions in terms of space and time Moreover it was designed to support several API and services But you can finely tune the kernel to avoid unused services reduce memory footprint and ease certifica tion verification efforts Next sections discusses the different architectures that can be used 72 1 Partitioned architecture The partitioned architecture pattern can be used with POK In that case the kernel will execute several partitions on top of the POK kernel and provide time and space partitioning across partitions Each partition contains their memory allocators their runtime and ressources the so called ibpok part Partitions can have different scheduling algorithms to schedule their tasks 39 CHAPTER 7 ARCHITECTURE 40 H device User driver code sercode driver Use pre defined Sand Thread scheduling li b k Middleware and core middleware interface 1 RT POSIX compliance I po libpok ARINC653 compliance Memory allocator IPC services Partition scheduling Core middleware POK Kernel Interupt exception handling Memory manager Figure 7 1 The different pok layers In that case the kernel provides communication isolation across partitions as well as space isolation each partition has its own memory segment The overall arc
27. provided In this example we see that the first partition has one port and the identifier of this port is nodel partition secret outgoing uint8 t nodel partition secret partport 1 nodel partition secret outgoing uint8 t nodel partition topsecret partport 1 nodel partition topsecret outgoing uint8 t nodel partition unclassified partport 1 nodel partition unclassified outgoing uint8 t pok ports nb ports by partition POK CONFIG NB PARTITIONS 1 1 1 uint8 t pok ports by partition POK CONFIG NB PARTITIONS nodel partition secret partport nodel partition topsecret partport nodel partition unclassified partport When you use code generation functionnalities this declaration is automatically created in the deployment c file CHAPTER 5 CONFIGURATION DIRECTIVES 33 5 4 Libpok partition runtime 5 5 Configuration You define the configuration policy by defining some C style maccros There are the list of useful maccros e POK CONFIG NB THREADS specify the number of threads contained in the parti tion e POK CONFIG NB BUFFERS Specify the number of buffers used in the libpok intra partition communication e POK CONFIG NB SEMAPHORES Specify the number of semaphores used in the libpok intra partition communication e POK CONFIG NB BLACKBOARDS Specify the number of blackboard we use for intra partition communications e POK CONFIG NB EVENTS Sp
28. respective message is passed OUT Length out Message Size Type Return Code out Return Code Type procedure Get Queuing Port Id Queuing Port Name in Queuing Port Name Type Queuing Port Id out Queuing Port Id Type Return Code out Return Code Type procedure Get Queuing Port Status Queuing Port Id in Queuing Port Id Type Queuing Port Status out Queuing Port Status Type Return Code out Return Code Type private type Queuing Port Id Type is new APEX Integer Null Queuing Port Id constant Queuing Port Id Type 0 pragma Convention C Queuing Port Status Type POK BINDINGS pragma Import C Create Queuing Port CREATE QUEUING PORT pragma Import 85 C Receive Queuing Message RECEIVE OUEUING MESSAGE pragma Import C Send Queuing Message SEND OUEUING PORT MESSAGE pragma Import C Get Queuing Port Id GET QUEUING PORT ID pragma Import C Get Queuing Port Status GET QUEUING PORT STATUS END OF POK BINDINGS end APEX Queuing Ports CHAPTER 8 POK API 86 8 3 10 Sampling ports package APEX Sampling_Ports is Max_Number_Of_Sampling_Ports constant System_Limit_Number_Of_Sampling_Ports subtype Sampling_Port_Name_Type is Name_Type type Sampling_Port_Id_Type is private Null_Sampling_Port_Id constant Sampling_Port_Id_Type type Validity_Type is Invalid Valid type Sampling_Port_Status_Type is record Refresh_Period S
29. see des h ssl h ceasar h and so on If there is no associated marshalling type then the mar shall unmarshall functions uses the same type as the application type or not particular type are required Details of each protocol can be found in the API section chapter 8 Chapter POK API 8 1 Core C 8 1 1 Error values include lt types h gt extern uint32_t errno K_ERRNO_H__ K_ERRNO_H__ O_OK O_EINVAL O_UNAVAILABLE O_TOOMANY O_EPERM O_EXISTS O_ERANGE O_EDOM O_HUGE_VAL O_EFAULT O_THREAD O_THREADATTR O_TIME POK_ERRNO_PARTITION_ATTR ifndef _ PO define _ PO typedef enum POK_ERRN POK_ERR POK_ERR POK_ERR POK_ERR POK_ERR POK_ERR POK_ERR POK_ERR POK_ERR POK_ERR POK_ERRN POK_ERR POK_ERR O_PORT 46 Ti 49 50 100 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 CHAPTER 8 POK API POK ERRNO NOTFOUND 302 POK ERRNO DIRECTION 303 POK ERRNO SIZE 304 POK ERRNO DISCIPLINE 305 POK ERRNO PORTPART 307 POK ERRNO EMPTY 308 POK ERRNO KIND 309 POK ERRNO FULL 311 POK ERRNO READY 310 POK ERRNO TIMEOUT 250 POK ERRNO MODE 251 POK ERRNO LOCKOBJ UNAVAILABLE 500 POK ERRNO LOCKOBJ NOTREADY 501 POK ERRNO LOCKOBJ KIND 502 POK ERRNO LOCKOBJ POLICY 503 POK ERRNO PARTITION MODE 601 POK ERRNO PARTITION 40 pok ret t endif 47 8 1 2 Memor
30. system implementation main i subcomponents nodel partition topsecret process partitions process_sender i nodel_partition_secret process partitions process_sender i nodel_partition_unclassified process partitions process_sender i node2_partition_topsecret process partitions process receiver i node2_partition_secret process partitions process receiver i node2_partition_unclassified process partitions process receiver i nodel_memory memory memories main memory i node2 memory memory memories main memory i nodel netif device runtime separation netif i POK Hw Addr gt 00 1F C6 BF 74 06 Implemented As gt classifier rt18029 hi node2_netif device runtime separation_neti i POK Hw Addr gt 00 0F FE 5F T1B 2F Implemented As gt classifier rt18029 1 s driver rtl8029 1 t driver rt18029 i 44 45 46 47 48 49 50 51 52 53 54 55 56 57 39 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 CHAPTER 10 ANNEXES nodel node2 rtbus connections Ports of partitions of the first port nodel partition topsecret outgoing port nodel partition secret outgoin port nodel partition unclassified outgoing 108 processor runtime pok_kernel imhpl processor runtime pok kernel impl bus runtime separation bus i node are connected to the devi gt nodel_net
31. 1 3 3 LEON3 A port for the LEON3 architecture a typical architecture in the aerospace domain is currrently in progress Please contact the POK team if you are interested by this port 1 4 Supported standards POK is compliant with the following standards e ARINC653 e MILS To achieve standard compliance POK relies on a minimal API that provides few canonical services These services then interact with the kernel to interact with other nodes processes 1 4 1 ARINC653 support At this time POK is compliant with the ARINC653 standard meaning that it provides partitioning functionnalities On the userland side it provides all the C and Ada API of the first part of ARINC653 However POK does not have an XML parser to automatically create the configu ration deployment code from ARINC653 XML files 1 4 2 MILS MILS stands for Multiple Independent Level of Security POK by defining strong partitioning can be MILS compliant depending on its configuration Most of the time the MILS compliant can be reached with a analysis of the system in terms of security To encrypt data POK relies on the OpenSSL library released under a BSD license see http www openssl org for more information 1 5 Aboutthe POK team POK is a research project It was made to experiment partitioned architectures and build safe and secure embedded systems It was initiated during a PhD thesis at TELE COM ParisTech and LIP6 laboratories The developer leade
32. 25 26 27 28 29 30 31 32 33 34 35 36 37 CHAPTER 8 POK API endif 64 8 2 ARINC653 C An ARINC653 layer is available for partitions This section presents the C layer an Ada layer is also available and described in section 8 3 8 2 1 APEX types and constants ifndef APEX TYPES define APEX TYPES include lt types h gt define SYSTEM_L T_NUMBER_OF_PARTITIONS 32 module scope define SYSTEM_L T_NUMBER_OF_MESSAGES 512 module scope define SYSTEM_L T_MESSAGE_SIZE 8192 module scope define SYSTEM_L T_NUMBER_OF_PROCESSES 128 partition scope define SYSTE L T_NUMBER_OF_SAMPLING_PORTS 512 partition scope define SYSTEM_L T_NUMBER_OF_QUEUING_PORTS 512 partition scope define SYSTEM_L T_NUMBER_OF_BUFFERS 256 partition scope define SYSTEM_L T_NUMBER_OF_BLACKBOARDS 256 partition scope define SYSTEM L T NUMBER OF SEMAPHORES 256 partition scope define SYSTEM L T NUMBER OF EVENTS 256 partition scope ESS oss ES Base APEX types vm aa TM The actual size of these base types is system specific and the f sizes must match the sizes used by the implementation of the underlying Operating System 4 typedef unsigned char APEX BYTE 8 bit unsigned typedef long APEX INTEGER 32 bit signed typedef unsigned long APEX UNSIGNED 32 bit unsigned typedef long long APEX
33. 4 t period uint64 t deadline uint64 t time capacity uint32 t stack size pok thread attr t void pok thread init void pok ret t pok thread create uint32 t thread id const pok thread attr t pok ret t pok thread sleep const pok time t ms pok ret t pok thread sleep until const pok time t ms pok ret t pok thread lock pok ret t pok thread unlock const uint32 t thread id pok ret t pok thread yield unsigned int pok thread current void void pok thread start void entry uint32 t id void pok thread switch uint32 t elected id pok ret t pok thread wait infinite void pok thread wrapper pok ret t pok thread attr init pok thread attr t attr pok ret t pok thread period pok ret t pok thread id uint32 t thread id void pok thread init void define pok thread sleep until time pok syscall2 POK SYSCALL THREAD SLEHP UNTIL uint32 t time 0 define pok thread wait infinite pok thread suspend define pok thread suspend pok syscall2 POK SYSCALL THREAD SUSPEND NUL NULL attr 51 52 53 54 55 56 57 58 59 60 61 62 63 65 66 67 68 69 70 7 72 73 CHAPTER 8 POK API 49 Similar to pok ret t pok thread suspend void Tz define pok thread restart thread id pok syscall2 POK SYSCALL THREAD RES similar to pok ret t pok thread restart uint32 t thread id define pok thread stop self pok syscall2 POK SYSCAL
34. 53 PROCESS define POK NEEDS ARINC653 PROCESS 1 endif include lt arinc653 process h gt include lt arinc653 types h gt define MAX ERROR MESSAGE SIZE 64 typedef APEX INTEGER ERROR MESSAGE SIZE TYPE typedef APEX BYTE ERROR MESSAGE TYPE MAX ERROR MESSAGE SIZE enum ERROR CODE VALUE TYPE DEADLINE MISSED APPLICATION_ERROR NUMERIC_ERROR ILLEGAL_REQUEST STACK_OVERFLOW MEMORY_VIOLATION HARDWARE_FAULT POWER_FAIL J 3 0 da W N H O hi typedef enum ERROR CODE VALUE TYPE ERROR CODE TYPE error status type Seras sas soso ss typedef struct ERROR_CODE_TYPE ERROR CODE MESSAGE SIZE TYPE LENGTH PROCESS ID TYPE FAILED PROCESS ID SYSTEM ADDRESS TYPE FAILED ADDRESS ERROR MESSAGE TYPE MESSAGE ERROR STATUS TYPE py ck ERROR MANAGEMENT SERVICES pe ey extern void REPORT_APPLICATION_MESSAGE MESSAGE_ADDR_TYPE MESSAGE MESSAGE_SIZE_TYPE LENGTH RETURN_CODE_TYPE RETURN_COD extern void CREATE ERROR HANDLER SYSTEM ADDRESS TYPE ENTRY POINT STACK SIZE TYPE STACK SIZE RETURN CODE TYPE RETURN CODE 1 58 59 60 61 62 63 65 66 67 CHAPTER 8 POK API 74 extern void GET ERROR STATUS ERROR STATUS TYPE ERROR STATUS RETURN CODE TYPE RETURN CODE extern void RAISE APPLICATION ERROR ERROR CODE TYPE ERROR CODE MESSAGE ADDR TYPE MESSAGE ERROR MESSAGE SIZE TYPE LENGTH RETURN CODE TYPE RET
35. 7 1 Directories hierarchy 7 2 Schyzophrenic architecture 7 2 1 Partitionedarchitecture 7 2 2 Executive architecture 7 3 Kernel Services soet Tor arue A ee 7 3 1 Partitioning service leen 4 3 2 Thread service s mao erc S RORIS S nee Xe 4 3 3 InneserviC 4 uv ehe y NN veb e Re ees 7 3 4 Communication service CONTENTS 43 3 5 Scheduling service ocios o s e rs TA TibDpok services lt ee 7 4 1 Thread management 7 42 Communication service 7 4 33 Memoryallocator 7 4 4 Mathematiclibraryservice 7 445 Protocols i 42 8 a eh a bee Ge KG SAL N S POK API SL Core Gs ca o ee we A A id 1 1 Erfor values s sata son a Be te e SA 8 1 2 MemoryAllocation 8 1 3 Threads sus RESI REESE NA S 8 1 4 Error handling lens 8 1 5 Inter partitions communication 8 1 6 Intra partitions communications 8 175 C hbraty ie sorde OR Board See INS ERR K 8 1 8 Math functions 8 1 9 Protocolfunctions o lee 8 2 ARINC653Q s KR e rs a a EE eee hc S 82 1 APEX types and constants 8 2 2 Partition management 82 3 Time management y a EKG 82 4 Error handling 8 2 5 Process manag
36. 8 59 60 61 62 63 65 66 CHAPTER 8 POK API 51 pok port directions t typedef pok gueueing discipline t pok port queueing discipline t typedef enum POK PORT KIND OUEUEING 1 POK PORT KIND SAMPLING 2 POK PORT KIND VIRTUAL 2 POK PORT KIND INVALID 10 pok port kinds t ifdef POK NEEDS PORTS VIRTUAL pok ret t pok port virtual create pok ret t pok port virtual destination pok ret t pok port virtual nb destinations pok ret t pok port virtual get global const pok port id t local endif ifdef POK_NEEDS_PORTS_QUEUEING char name pok_port_id_t id const pok port id t id const uimt32_t n uint32 t const pok port id t id uintj2 t result pok port id t global Queueing port functions typedef struct pok_port_size_t size pok_port_direction_t uint8_t uint8 t pok port queueing statu pok ret t pok port queue name size direction discipline id pok ret t pok port queueing receive id timeout maxlen data len pok ret t pok port queue id direction nb messages waiting processes S ts ing create char const pok port size t const pok port direction t const pok port queueing discipline t pok port id t const pok port id t const uint64 t const pok port size t void pok port size t ing send const pok port id t result 67 68 69 70 71 72 73 74 75 76
37. ATION DIRECTIVES 34 e POK_NEEDS_IO needs functions to perform I O These functions are just system calls and ask the kernel to perform them The partition CANNOT make any I O by itself e POK_NEEDS_TIME activate functions that handle time e POK_NEEDS_THREADS activate functions relative to threads e POK NEEDS PORTS VIRTUAL activate functions for virtual ports management Virtual ports are handled by the kernel So activated functions in the libpok are just system call to the kernel to get the port routing policy Since virtual ports represent ports that are located on other nodes this maccro should be used only by partitions that actually implement network device drivers e POK NEEDS PORTS SAMPLING activate interfacing functions with the kernel to use sampling ports e POK NEEDS PORTS QUEUEING activate interfacing functions with the kernel to use queueing ports e POK NEEDS ALLOCATOR activate the memory allocator of the partition This service can be configured with POK CONFIG ALLOCATOR maccros e POK NEEDS ARINC653 PROCESS activate the process service of the ARINC653 layer e POK NEEDS ARINC653 BLACKBOARD activate the blackboard service of the AR INC653 layer e POK NEEDS ARINC653 BUFFER activate the buffer service of the ARINC653 layer e POK NEEDS ARINC653 SEMAPHORE activate the semaphore service of the AR INC653 layer e POK NEEDS ARINC653 QUEUEING activate the queueing service of the ARINC653 layer
38. C653 XML files and automatically produce the C configuration code deployment h and deployment c However the configuration produced is not as complete as the one generated from AADL models Indeed ARINC653 XML files do not contain enough information to generate the whole configuration and is not sufficient to generate the configuration of partitions However this is a good way to have basic configuration files that can be improved by manual edition The tool is located in the misc directory of POK releases You can use it as it misc arinc653 xml conf pl arinc653 configuration file xml When it is invoked this program automatically produces two files deployment h and deployment c These files must be compiled with the kernel for its automatic configuration 5 2 Common configuration The following maccros can be defined for both partitions and kernel e POK GENERATED CODE specify that the code compiled has been generated from AADL so that we can restrict and avoid the use of some functions This maccro is automatically added by Ocarina when it generates code from AADL models 23 CHAPTER 5 CONFIGURATION DIRECTIVES 24 5 3 Kernel configuration 5 3 1 Services activation You can define which functionnalities you want in the kernel by defining some maccros Depending on which maccro you define it will add services and functionnalities in your kernel It was made to make a very tight kernel and ease verification certification ef
39. C653 layer is also available in 1ibpok ada arinc653 and should be used the same way as described above CHAPTER 3 GETTING STARTED 15 3 8 Run POK on Leon3 To build and run POK on Leon3 you must have the TSIM simulator Then perform the following actions 1 2 Add tsim leon3 directory to you PATH environment variable Issue make configure at the top directory of POK Enter the directory examples partitions scheduling by typing this com mand in a terminal cd examples partitions scheduling Invoke make ARCH sparc BSP 1eon3 It will generate configuration and appli cation code with Ocarina Invoke make ARCH sparc BSP leon3 run Using this command TSIM is launched and your system is being executed Evaluation version available at ftp ftp gaisler com gaisler com tsim Chapter 4 Automatic configuration and configuration with AADL models 4 1 Proposed development process Using AADL models can help system designers and developers in the implementation of partitioned architectures POK can be configured automatically using AADL mod els In fact the AADL is very efficient for the design of real time embedded systems designers specify their architecture with respect to their specificites and requirements Then the Ocarina toolsuite analyzes the architecture and automatically generates code for POK The code generation process automatically configures the kernel and the partitions The developpers should p
40. CKBOARD in BLACKBOARD ID TYPE BLACKBOARD ID in SYSTEM TIME TYPE TIME OUT out MESSAGE ADDR TYPE MESSAGE ADDR out MESSAGE SIZE TYPE LENGTH out RETURN CODE TYPE RETURN CODE extern void CLEAR BLACKBOARD in BLACKBOARD ID TYPE BLACKBOARD ID out RETURN CODE TYPE RETURN CODE extern void GET BLACKBOARD ID in BLACKBOARD NAME TYPE BLACKBOARD NAME out BLACKBOARD ID TYPE BLACKBOARD ID out RETURN CODE TYPE RETURN CODE extern void GET BLACKBOARD STATUS in BLACKBOARD ID TYPE BLACKBOARD ID out BLACKBOARD STATUS TYPE BLACKBOARD STATUS out RETURN CODE TYPE RETURN CODE endif endif 8 2 7 Buffer service intra partition communication ifdef POK_NEEDS_ARINC653_BUFFER NI pe TY BUFFER constant and type definitions and management services ay pe e MO PTT ifndef APEX BUFFER APEX BUFFER define ifndef POK_NEEDS_ARINC653_PROCESS POK_NEEDS_ARINC653_PROCESS define endif ce PA CHAPTER 8 POK API include lt arinc653 types h gt include lt arinc653 process h gt define MAX NUMBER OF BUFFERS typedef NAME TYPE typedef APEX INTEGER typedef struct SYSTEM LIMIT NUMBER OF BUFFER NAME TYPE BUFFER ID TYPE MESSAGE RANGE TYPE MESSAGE RANGE TYPE MESSAGE SIZE TYPE WAITING RANGE TYPE NB MESSAGE MA
41. E W PD O typedef APEX INTEGER typedef enum PARTITION ID TYPE NORMAL START 20 PARTITION RESTART 1 HM_MODULE_RESTART 2 HM_PARTITION_RESTART 3 START CONDITION TYPE typedef struct SYSTEM_TIME_TYPE PERIOD SYSTEM_TIME_TYPE DURATION PARTITION_ID_TYPE IDENTIFIER LOCK_LEVEL_TYPE LOCK_LEVEL OPERATING_MODE_TYPE OPERATING_MODE START_CONDITION_TYPE START_CONDITION PARTITION_STATUS_TYPE PARTITIONS parameter incompatible with configuration r with a 1 nanosecond LSB 37 38 39 40 41 42 43 45 CHAPTER 8 POK API 66 extern void GET_PARTITION_STATUS out PARTITION STATUS TYPE PARTITION STATUS out RETURN CODE TYPE RETURN CODE extern void SET PARTITION MODE in OPERATING MODE TYPE OPERATING MODE out RETURN CODE TYPE RETURN CODE endif endif 8 2 3 Time management ifdef POK_NEEDS_ARINC653_TIME ifndef APEX_TIME define APEX_TIME include lt arinc653 types h gt pe E time constant definitions p wy e implementation dependent these values are given as example p c K M PE time type definitions JE i Ss M p
42. ES 38 middleware queueing timed Test the use of queuing port service with timeout Use AADL models middleware sampling Test the use of sampling port service Use AADL mod els mutexes Test mutex service POK layer Use AADL models mutexes timed Test mutex service with timeout Use AADL models network Test network driver rt18029 on x86 architecture Use AADL models partitions scheduling Example with different schedulers Use AADL models partitions threads Test thread instanciation POK layer Use AADL models semaphores Test the use of semaphors POK layer Do not use AADL models simulink Test the inclusion of simulink code Do not work since it needs a dedicated runtime to work It needs additional services in the libpok layer to work This additional work is not so difficult to provide we just need time Chapter 7 Architecture 7 1 Directories hierarchy The project is organized with a hierarchy of several directories e examples sample code that uses pok and libpok Code of examples is mostly generated from AADL models by Ocarina e kernel code of the kernel that provides time and space partitioning services e libpok code of libpok the runtime of each partition It contains libc POSIX and arinc653 compliant abstraction layers e misc misc files such as makefiles various tools to compile POK and so on 72 Schyzophrenic architecture POK can be used as an executive 1 e a kernel that contains
43. EXES 102 434 Type_Source_Name gt char 435 end char 436 437 data implementation char i 438 end char i 439 440 data pointed char 441 properties 442 Type Source Name gt char 443 end pointed char 444 445 data implementation pointed char i 446 end pointed char i 447 448 data integer 449 properties 450 Data Model Data Representation gt integer 451 end integer 452 453 454 data float 455 properties 456 Data Model Data Representation gt float 457 end float 458 459 460 461 462 end poklib 10 5 ARINC653 property set for the AADL 1 Property set for the ARINC653 annex 2 This version comes with the annex draft issued on 20090727 3 4 property set ARINC653 is 5 6 Partition Slots list of Time applies to processor 7 8 Slots_Allocation list of reference virtual processor 9 applies to processor 10 11 Module_Major_Frame Time applies to processor 12 13 Sampling_Refresh_Period Time applies to data port 14 15 Supported_Error_Code type enumeration 16 Module_Config module level errors 17 Module_Init 18 Module_Scheduling 19 Partition_Scheduling partition level errors 20 Partition_Config 21 Partition_Handler 22 Partition Init 23 Deadline Miss process level errors 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 22 53 54 55
44. For each local port we specify the number of destinations Since there can be more than one recipient to a sending port we specify how many ports should receive data We specify that with the pok ports nb destinations array Then we specify the local port routing policy with the pok ports destinations array In this array each value is a pointer to another array that contains the recipient global port values CHAPTER 5 CONFIGURATION DIRECTIVES 30 An example is given below Here the first local port has one recipient The re cipient list is specified with the first elements of the pok ports destinations ar ray which is the nodel partition secret outgoing deployment destinations array Thus we can see that the recipient port identifier is node2 partition secret incoming global uint8 t nodel partition secret outgoing deployment destinations 1 node2 partition secret incoming global uint8 t nodel partition secret partport 1 nodel partition secret outgoing uint8 t nodel partition topsecret outgoing deployment destinations 1 node2 partition topsecret incoming global uint8 t nodel partition unclassified outgoing deployment destinations 1 node2 partition unclassified incoming global uint8 t pok ports nb destinations POK CONFIG NB PORTS 1 1 1 uint8 t pok ports destinations POK CONFIG NB PORTS nodel partition secret outgoing deployment destinations nodel partition topsecre
45. L THREAD STOPSELF similar to pok ret t pok thread stop self define pok thread stop id pok syscall2 POK SYSCALL THREAD STOP id NULL similar to pok ret t pok thread stop const uint32 t tid zy endif POK NEEDS THREADS endif POK THREAD H 8 1 4 Error handling include lt core dependencies h gt ifdef POK NEEDS ERROR HANDLING include lt types h gt include lt errno h gt define POK ERROR MAX LOGGED 100 typedef struct uint8 t error kind xdfit32 t failed thread int32 t failed addr char msg uint32 t msg size pok error status t typedef struct daint32 t thread vint32 t error pok time t when pok error report t extern pok error report t pok error reported POK ERROR MAX LOGGED TART thread id 0 0 31 32 33 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 CHAPTER 8 POK API 50 define POK ERROR KIND DEADLINE MISSED 10 define POK ERROR KIND APPLICATION ERROR 11 define PO ERROR_KIND_NUMERIC_ERROR 12 define PO ERROR ND_ILLEGAL_REQUEST 13 define PO ERROR ND_STACK_OVERFLOW 14 define PO ERROR_KIND_MEMORY_VIOLATION 15 define POK ERROR KIND HARDWARE FAULT 16 define PO ERROR ND POWER FAIL 17 define POK ERROR KIND PARTITION CONFIGURATION 30 define POK ERROR KIND PARTITION INIT Sili
46. Max Number Of Buffers constant System Limit Number Of Buffers subtype Buffer Name Type is Name Type type Buffer Id Type is private Null Buffer Id constant Buffer Id Type type Buffer Status Type is record Nb Message Message Range Type Max Nb Message Message Range Type Max Message Size Message Size Type Waiting Processes APEX Processes Waiting Range Type end record procedure Create Buffer Buffer Name in Buffer Name Type Max Message Size in Message Size Type Max Nb Message in Message Range Type Queuing Discipline in Queuing Discipline Type Buffer Id out Buffer Id Type Return Code out Return Code Type procedure Send Buffer 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 CHAPTER 8 POK API 79 Buffer Id in Buffer Id Type Message Addr in Message Addr Type Length in Message Size Type Time Out in System Time Type Return Code out Return Code Type procedure Receive Buffer Buffer Id in Buffer Id Type Time Out in System Time Type Message Addr in Message Addr Type The message address is passed IN although the respective message is passed OUT Length out Message Size Type Return Code out Return Code Type procedure Get Buffer Id Buffer Name in Buffer Name Type Buffer Id out Buffer Id Type Return Code out Return Code Type procedure Get
47. ODE_TYPE A error status type rE typedef struct ERROR_CODE_TYPE ERROR CODE MESSAGE SIZE TYPE LENGTH PROCESS ID TYPE FAILED PROCESS ID SYSTEM ADDRESS TYPE FAILED ADDRESS ERROR MESSAGE TYPE MESSAGE ERROR STATUS TYPE LEY ERROR MANAGEMENT SERVICES 5 ER extern void REPORT APPLICATION MESSAGE MESSAGE ADDR TYPE MESSAGE MESSAGE SIZE TYPE LENGTH RETURN CODE TYPE RETURN COD extern void CREATE ERROR HANDLER SYSTEM ADDRESS TYPE ENTRY POINT 1 56 57 58 59 60 61 62 63 65 66 67 CHAPTER 8 POK API STACK_SIZE_TYPE RETURN_CODE_TYPE extern void GET_ERROR_STATUS ERROR_STATUS_TYPE RETURN_CODE_TYPE extern void RAISE_APPLICATION_ERROR ERROR_CODE_TYPE MESSAGE_ADDR_TYPE ERROR_MESSAGE_SIZE_TYPE RETURN_CODE_TYPE endif endif 68 STACK_SIZE RETURN CODE ERROR STATUS RETURN_CODE ERROR CODE MESSAGE LENGTH RETURN_ 8 2 5 Process management ifdef POK_NEEDS_ARINC653_PROCESS include lt arinc653 types h gt ifndef APEX_PROCESS define APEX_PROCESS define MAX NUMBER OF PROCESSES SYSTEM LIMIT NUMBER OF PROCESSES define MIN PRIORITY VALUE 1 define MAX PRIORITY VALUE 63 define MAX LOCK LEVEL 16 typedef NAME TYPE PROCESS NAME TYPE typedef APEX INTEGER PROCESS ID TYPE typedef APEX INTEGER LOCK LEVEL TYPE typedef APEX UNSIGNED STACK SIZE TYPE typedef A
48. PEX INTEGER WAITING RANGE TYPE typedef APEX INTEGER PRIORITY TYPE typedef enum DORMANT 0 READY 1 RUNNING 2 WAITING 3 PROCESS_STATE_TYPE typedef enum SOFT 0 HARD 1 DEADLINE_TYPE typedef struct SYSTEM_TIME_TYPE PERIOD ODE 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 65 66 67 68 69 70 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 CHAPTER 8 POK API SYSTEM_TIME_TYPE SYSTEM_ADDRESS_T STACK_SIZE_TYPE PRIORITY_TYPE DEADLINE_TYPE PROCESS_NAME_TYP YPE E TIME_CAPACITY ENTRY_POINT STACK_SIZE BASE PRIORITY DEADLINE NAME PROCESS ATTR typedef struct SYSTEM TIME PRIORIIY TY PROCESS STA PROCESS ATT PROCESS STAT extern void CR in out out extern void SE fin el im out extern void SU in out extern void SU in out extern void RE in out extern void ST extern void ST TR hy Gut extern void ST in out extern void DE in a Ef out extern void LO out out extern void UN IBUTE TYPE _TYPE DEADLINE_TIME PE CURRENT_PRIORITY TE_TYPE PROCESS_STATE RIBUTE_TYPE ATTRIBUTES US_TYPE EATE_PROCESS PROCESS_ID_TYPE RETURN_CODE_TYPE T PRIORITY PROCESS ID TYPE PRIORITY TYPE RETURN CODE TYPE SPEND
49. POK User Guide POK Team March 17 2010 Contents 1 Introduction 3 Ll Whatis POR Yu ia A A 3 1 2 Purpose of this document 3 1 3 Supported platforms ees 3 ES Ll A Pe RE BA DOS SUR OE vert Dee TO X AER 3 1 32 PowerPC ga ti a ERR RU Re Wes eus 4 1 35 35 TEON S ts esp deb TERR CRUS AUS 4 1 4 Supportedstandards 4 1 4 1 ARINC653supportt 4 L42 MIES ia SRI xe RENE Ma SS 4 15 AboutthePOK team 0 00000004 4 2 Installation 6 2 1 Supported development platforms 6 2 2 Getmoreinformation 6 2 3 EIMUX MACOS rarai ea BS ln le ala RUE 6 2 3 1 Pre require ss comes e og 9r yo a 6 2 3 2 Running POK 54 nh Rum Ee 7 2 4 WIDAOWS 7 usse Sire erede RTA Oe pde J So Sr Rar OO TA J Ax lt 7 24 Presrequitess eR DRM ERU URS S 7 3 Getting started 8 3 1 First experience with POK 8 3 2 Development cycle ee 9 3 3 Configure POK the conf env piscript 9 3 4 Automatic and manual configuration 9 3 5 Kernel configuration with ARINC653 XML files 10 3 6 How to write my manual code 10 3 7 Using Ada for partitions 11 3 8 RunPOKonLeon3 12 CONTENTS 4 Automatic configuration and configuration with AADL models 4 1 Proposed developme
50. SELF SYSTEM TIME TYPE RETURN CODE TYPE SPEND PROCESS ID TYPE RETURN CODE TYPE SUME PROCESS ID TYPE RETURN CODE TYPE OP SELF PROCESS ATTRIBUTE TYPE ATTRIBUTES PROCESS ID RETURN CODE PROCESS ID PRIORITY RETURN CODE TIME OUT RETURN CODE PROCESS ID RETURN CODE PROCESS ID RETURN CODE OP PROCESS ID TYPE PROCESS ID RETURN CODE TYPE RETURN CODE LOCK PREEMPTION ART PROCESS ID TYPE PROCESS ID RETURN CODE TYPE RETURN CODE LAYED START PROCESS ID TYPE PROCESS ID SYSTEM TIME TYPE DELAY TIME RETURN CODE TYPE RETURN CODE CK PREEMPTION LOCK LEVEL TYPE LOCK LEVEL RETURN CODE TYPE RETURN CODE 69 99 100 101 102 103 105 106 107 108 109 110 111 112 113 114 115 116 117 CHAPTER 8 POK API 70 out LOCK_LEVEL_TYPE LOCK_LEVEL out RETURN_CODE_TYPE RETURN_CODE extern void GET MY ID out PROCESS ID TYPE PROCESS ID out RETURN CODE TYPE RETURN CODE extern void GET PROCESS ID in PROCESS NAME TYPE PROCESS NAME MAX NAME LENGTH out PROCESS ID TYPE PROCESS ID out RETURN CODE TYPE RETURN CODE extern void GET PROCESS STATUS in PROCESS ID TYPE PROCESS ID out PROCESS STATUS TYPE PROCESS STATUS out RETURN CODE TYPE RETURN CODE endif endif 8 2 6 Blackboard service intra partition
51. TATIC the static scheduling protocol is included in the ker e POK NEEDS PORTS SAMPLING the sampling ports service for inter partitions com munication is included CHAPTER 5 CONFIGURATION DIRECTIVES 25 e POK_NEEDS_PORTS_QUEUEING the queueing ports service for inter partitions com munication is included 5 3 2 General configuration Number of threads The POK_CONFIG_NB_THREADS maccro specifies the number of threads in the system This represents how many threads can be handled in the kernel The values must be computed like this number of threads in your system 2 In fact in this maccro you must add 2 additional threads the kernel thread and the idle thread Number of lockobjects The POK CONFIG NB LOCKOBJECTS maccro specifies the number of lockobjects the ker nel would manage It is the sum of potential semaphores mutexes or ARINC653 events 5 3 3 Partitions configuration 5 3 4 Number of partitions The POK CONFIG NB PARTITIONS maccro specifies the number of partitions handled in the kernel Threads allocation across partitions The POK_CONFIG_PARTITIONS_NTHREADS maccro specifies how many threads would resides in partitions This declaration is an array each value of the array corresponds to the number of threads inside a partition An example is given below In this example we consider that we have 4 partitions The first second and third partitions handle two threads while the last partition
52. Time Type Message Addr in Message Addr Type The message address is passed IN although the respective message is passed OUT ards 34 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 CHAPTER 8 POK API 78 Length out Message Size Type Return Code out Return Code Type procedure Clear Blackboard Blackboard Id in Blackboard Id Type Return Code out Return Code Type procedure Get Blackboard Id Blackboard Name in Blackboard Name Type Blackboard Id out Blackboard Id Type Return Code out Return Code Type procedure Get Blackboard Status Blackboard Id in Blackboard Id Type Blackboard Status out Blackboard Status Type Return Code out Return Code Type private type Blackboard Id Type is new APEX Integer Null Blackboard Id constant Blackboard Id Type 0 pragma Convention C Empty Indicator Type pragma Convention C Blackboard Status Type POK BINDINGS pragma Import C Create Blackboard CREATE BLACKBOARD pragma Import C Display Blackboard DISPLAY BLACKBOARD pragma Import C Read Blackboard READ BLACKBOARD pragma Import C Clear Blackboard CLEAR BLACKBOARD pragma Import C Get Blackboard Id GET BLACKBOARD ID pragma Import C Get Blackboard Status GET BLACKBOARD STATUS END OF POK BINDINGS end APEX Blackboards 8 3 3 Buffers package APEX Buffers is
53. URN CODE endif endif 8 2 9 Queuing ports service inter partition communication 8 2 10 Sampling ports service inter partition communication ifdef POK_NEEDS_ARINC653_SAMPLING include lt arinc653 types h gt EE E E N E E E E E E p ky SAMPLING PORT constant and type definitions and management services K X SS ifndef APEX SAMPLING define APEX SAMPLING define MAX NUMBER OF SAMPLING PORTS SYSTEM LIMIT NUMBER OF SAMPLING RORTS typedef NAME TYPE SAMPLING PORT NAME TYPE typedef APEX INTEGER SAMPLING PORT ID TYPE typedef enum INVALID 0 VALID 1 VALIDITY TYPE typedef struct SYSTEM_TIME_TYPE REFRESH_PERIOD MESSAGE_SIZE_TYPE MAX MESSAGE SIZE PORT DIRECTION TYPE PORT DIRECTION VALIDITY TYPE LAST MSG VALIDITY SAMPLING PORT STATUS TYPE extern void CREATE SAMPLING PORT in SAMPLING PORT NAME TYPE SAMPLING PORT NAME in MESSAGE SIZE TYPE MAX MESSAGE SIZE in PORT DIRECTION TYPE PORT DIRECTION in SYSTEM TIME TYPE REFRESH PERIOD out SAMPLING PORT ID TYPE SAMPLING PORT ID out RETURN CODE TYPE RETURN CODE 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 65 CHAPTER 8 POK API extern void WRITE_SA MPLING_MESSAGE
54. Virtual Bus Class gt classifier layers POR Criticality gt 1 y runtime_netif virtual processor partition i Provided Virtual Bus Class gt classifier layers un POK Additional Features gt libc_stdlib pci io POK Criticality gt 10 properties POK Major Frame gt 2000ms POK Scheduler gt static POK Slots gt 500ms 500ms 500ms 500ms ecret op_secret inclassified lassified classifier lay CHAPTER 10 ANNEXES 107 POK Slots_Allocation gt reference runtime_secret reference funtime_topsecret referenc end pok_kernel impl bus separation_bus end separation_bus bus implementation separation bus i subcomponents layer topsecret virtual bus layers top secret layer secret virtual bus layers secret layer unclassified virtual bus layers unclassified end separation bus i end runtime POK header The following file is a part of the POK project Any modification shquld be made according to the POK licence You CANNOT use this file or a part of a file for your own project For more information on the POK licence please see our LICENCE FILE Please follow the coding guidelines described in doc CODING GUIDELINES Copyright c 2007 2009 POK team Created by julien on Mon May 4 12 37 45 2009 package model public with runtime with partitions with memories with POK system main end main
55. X NB MESSAGE MAX MESSAGE SIZE WAITING PROCESSES BUFFER STATUS TYPE extern void A xy im Fy pim pe m Pout out extern pi f rim J m X tin out extern in f p im f Pout Pout out extern void SEND void RECEIVE CREATE BUFFER BUFFER NAME TYPE ESSAGE SIZE TYPE ESSAGE RANGE TYPE QUEUING DISCIPLINE TYPE BUFFER ID TYPE RETURN CODE TYPE BUFFER BUFFER ID TYPE ESSAGE ADDR TYPE ESSAGE SIZE TYPE SYSTEM TIME TYPE RETURN CODE TYPE BUFFER BUFFER ID TYPE SYSTEM TIME TYPE MESSAGE ADDR TYPE MESSAGE SIZE TYPE RETURN CODE TYPE BUFFER NAME MAX MESSAGE SIZE MAX NB MESSAGE QUEUING DISCIPLINE BUFFER ID RETURN CODE BUFFER ID MESSAGE ADDR LENGTH TIME OUT RETURN_CODE BUFFER ID TIME OUT MESSAGE ADDR LENGTH RETURN_CODE void GET_BUF in BUFF FER ID ER NAME TYPE out BUFFER ID TYPE out RETU extern void RN CODE TYPE GET BUFFER STATUS in BUFFER ID TYPE out BUFF out RETU endif endif RN_CODE_TYPE ER_STATUS_TYPE BUFFER_NAME BUFFER_ID RETURN_CODE BUFFER_ID BUFFER_STATUS RETURN_CODE 72 BUFFERS by refere 8 2 8 Event service intra partition communication ce 5j CHAPTER 8 POK API 73 ifdef POK_NEEDS_ARINC653_ERROR ifndef APEX ERROR define APEX ERROR ifndef POK NEEDS ARINC6
56. _global 0 nodel_partition_topsecret_outgoing_global 1 nodel_partition_unclassified_outgoing_global 2 CHAPTER 5 CONFIGURATION DIRECTIVES 29 node2_partition_secret_incoming_global 3 node2 partition topsecret incoming global 4 node2 partition unclassified incoming global pok port identifier t 5 Node identifiers The node identifiers are specified by declaring the pok node identifier t type It contains the value of each node identifier Please also note that the POK CONFIG LOCAL NODE value must be in this enum declaration This enum declaration is THE SAME on all nodes of the distributed system When you use code generation functionnalities this declaration is automatically created in the deployment h file There is an example of a such declaration typedef enum nodel 0 node2 1 pok_node_identifier_t Associate local ports with global ports We specify the global port of each local port with the pok_ports_identifiers array An example is given below uint8_t pok_ports_identifiers POK_CONFIG_NB_PORTS nodel partition secret outgoing nodel partition topsecret outgoing nodel partition unclassified outgoing Here the first local port of the current node corresponds to the nodel partition secret outgoing global port When you use code generation functionnalities this declaration is automatically created in the deployment c file Specify local ports routing local ports to global ports
57. ackboard display const pok blackboard id t id const void message const pok_port_size_t len pok ret t pok blackboard clear const pok_blackboard_id_t id pok ret t pok blackboard id char name pok blackboard id t id pok ret t pok blackboard status const pok blackboard id t id pok blackboard status t status endif endif endif Buffers ifndef POK USER BUFFER H define POK_USER_BUFFER_H ifdef POK_NEEDS_MIDDLEWARE ifdef POK_NEEDS_BUFFERS define POK_BUFFER_DISCIPLINE_FIFO 1 define POK_BUFFER_DISCIPLINE_PRIORITY 2 include lt types h gt include lt errno h gt include lt core lockobj h gt CHAPTER 8 POK API typedef struct pok_bool_t pok_bool_t pok_bool_t pok_size_t pok_size_t pok_port_size_t pok_port_size_t pok_port_size_t pok_range_t pok gueueing discipline t pok event id t pok buffer t typedef struct pok_range_t pok_range_t pok_size_t pok_range_t pok buffer status t ready empty full size index off bi off e msgsize waiting processes discipline lock nb messages max messages message size waiting processes pok ret t pok buffer create char const pok port size t const pok port size t const pok queueing discipline t pok buffer id t pok ret t pok buffer receive const pok buffer id t const uint64 t void pok port size t pok ret t pok buffer send const pok buffer id t const void const pok port size t
58. cessor compo nent we check that the major time frame is equal to the sum of partitions slots We also check that each partition has at least one time frame to execute their threads 5 Architecture correctness we check that models contain memory components with the appropriate properties We also check that process components are bound to virtual processor components CHAPTER 4 AUTOMATIC CONFIGURATION AND CONFIGURATION WITH AADL MODELS19 4 4 POK properties for the AADL The AADL can use user defined property sets to add specific properties on AADL components On our side we define our own AADL properties added to AADL com ponents to describe some specific behavior The POK property set for theAADL can be found in the annex section In addition POK and its associated AADL toolsuite Ocarina supports the AR INC653 annex of the AADL So you can use models that enforces the ARINC653 annex with POK The ARINC653 property set for the AADL is included in the annex section of this document 4 5 Modeling patterns This section describes the code generation patterns used to generate code So it explain the mapping between AADL models and generated code To understand this section you have to know the AADL You can find tutorials in the internet about this modeling language Wikipedia can be a good starting point 4 5 1 Kernel The kernel is mapped with the AADL processor component If the architecture is a partitioned architecture i
59. communication ifdef POK_NEEDS_ARINC653_BLACKBOARD i iro ae eee Sie eo A x NA BLACKBOARD constant and type definitions and management services J m Ji lat A SES x ifndef APEX_BLACKBOARD define APEX BLACKBOARD ifndef POK NEEDS ARINC653 PROCESS define POK NEEDS ARINC653 PROCESS endif include lt arinc653 types h gt include lt arinc653 process h gt define MAX_NUMBER_OF_BLACKBOARDS SYSTEM_LIMIT_NUMBER_OF_BLACKBOARDS typedef NAME_TYPE BLACKBOARD_NAME_TYPE typedef APEX_INTEGER BLACKBOARD_ID_TYPE typedef enum EMPTY 0 OCCUPIED 1 EMPTY_INDICATOR_TYPE typedef struct EMPTY INDICATOR TYPE EMPTY INDICATOR MESSAGE SIZE TYPE MAX MESSAGE SIZE WAITING RANGE TYPE WAITING PROCESSES BLACKBOARD STATUS TYPE 35 36 37 38 39 40 41 42 43 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 65 66 67 68 69 70 CHAPTER 8 POK API 71 extern void CREATE_BLACKBOARD in BLACKBOARD_NAME_TYPE BLACKBOARD_NAME tin ESSAGE_SIZE_TYPE MAX_MESSAGE_SIZE out BLACKBOARD_ID_TYPE BLACKBOARD_ID out RETURN_CODE_TYPE RETURN_CODE extern void DISPLAY BLACKBOARD in BLACKBOARD ID TYPE BLACKBOARD ID in ESSAGE ADDR TYPE MESSAGE ADDR by refere tin ESSAGE SIZE TYPE LENGTH out RETURN CODE TYPE RETURN CODE extern void READ BLA
60. communication we introduce several concepts e The node identifier is a unique number for each node e The global port identifier is a unique number for each port in the whole dis tributed system This unique identifier identifies each port of each node e The local port identifier is a unique number for each port on the local node only It identifies each inter partition communication port on the local kernel So for each node you must specify in the kernel e The node identifier of the current node e The number of nodes in the distributed system e The number of inter partitions ports in the distributed system e The number of inter partitions ports on the local node e All identifiers of global ports e All identifiers of local ports e The association between global ports and nodes e The association between global ports and local ports e The association between local ports and global ports Current node identifier The identifier of the current node is specified with the POK CONFIG LOCAL NODE mac cro When you use code generation functionnalities this declaration is automatically created in the deployment h file CHAPTER 5 CONFIGURATION DIRECTIVES 28 Number of global ports The number of global ports in the distributed system is specified with the POK CONFIG NB GLOBAL PORTS It indicates the number of global ports in the system When you use code generation functionnalities this declaration is automatically created in
61. define pok protocols des data t unsigned long long ifdef POK NEEDS PROTOCOLS DES Function that uncrypts data ay void pok_protocols_des_unmarshall void crypted data pok_size_t crypted Function that crypts data ie void pok protocols des marshall void uncrypted data pok size t uncryp The key for the DES protocol is on 8 bytes and is defined by the macro POK PROTOCOLS DES KEY oy ifndef POK_PROTOCOLS_DES_KEY define POK PROTOCOLS DES KEY 0x01 0x23 0x45 0x67 0x89 0xab 0xcd 0xef endif YA The init vector for the DES protocol is on 8 bytes defined by the macro POK_PROTOCOLS_DES_INIT MJ ifndef POK_PROTOCOLS_DES_INIT define POK PROTOCOLS DES INIT 0xfe 0xdc 0xba 0x98 0x76 0x54 0x32 0x10 endif endif endif ifndef __LIBPOK_PROTOCOLS_SSL_H__ define __LIBPOK_PROTOCOLS_SSL_H__ include lt types h gt file libpok protocols ssl h Nauthor Julien Delange date 2009 brief SSL crypto protocol More information at http en wikipedia org wiki Transport Layer Security ifdef POK NEEDS PROTOCOLS void pok protocols ssl unmarshall void crypted data pok size t crypted size void pok protocols ssl marshall void uncrypted data pok size t uncryp define pok protocols ssl data t int endif _size void ed_size ed_size void void void uncrypted_data crypted_data uncrypted_data crypted_data 25 26 23 24
62. e type Process Id Type is private constant Process Id Type Lock Level Type is APEX Integer range 0 Stack Size Type is APEX Unsigned Waiting Range Type is APEX Integer range r Of Processes Type is APEX Integer range alue Max Priority Value e Type is Dormant Ready e is Soft Hard ibute Type is record System Time Type System Time Type System Address Type Stack Size Type Priority Type Deadline Type Process Name Type us Type is record System Time Type Priority Type Process State Type Process Attribute Type ity Process in Process Attribute Type out Process Id Type out Return Code Type ority in Process Id Type in Priority Type out Return Code Type Self in System Time Type out Return Code Type in Process out Return d Type Code Type in Process out Return Tt d Type Code Type in Process Id Type out Return Code Type Running Max Lock Level Waiting 59 60 61 62 63 65 66 67 68 69 70 71 72 7 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 105 106 CHAPTER 8 POK API 84 Process Id in Process Id Type Return Code out Return Code Type procedure Delayed Start Process Id in Process Id Type Delay Time in System Time Type Return Code out Return Code Type procedure Lock Preemption Lock Level out Lock Level Type Return Code ou
63. e out Return Code Type procedure Wait Event Event Id in Event Id Type Time Out in System Time Type Return Code out Return Code Type procedure Get Event Id Event Name in Event Name Type Event Id out Event Id Type Return Code out Return Code Type procedure Get Event Status Event Id in Event Id Type Event Status out Event Status Type Return Code out Return Code Type private type Event Id Type is new APEX Integer Null Event Id constant Event Id Type 0 pragma Convention C Event State Type pragma Convention C Event Status Type POK BINDINGS pragma Import pragma Import pragma Import pragma Import C Create Event CREATE EVENT C Set Event SET EVENT C Reset Event RESET EVENT C Wait Event WAIT EVENT pragma Import C Get Event Id GET EVENT ID pragma Import C Get Event Status GET EVENT STATUS END OF POK BINDINGS end APEX Events 8 3 5 Health monitoring with APEX Processes package APEX Health Monitoring is Max Error Message Size constant 64 subtype Error Message Size Type is APEX Integer range 1 Max Error Message Size type Error Message Type is array Error Message Size Type of APEX Byte type Error Code Type is Deadline Missed Application Error Numeric Error Illegal_Request Stack Overflow Memory Violation 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
64. e POK NEEDS ARINC653 SAMPLING activate the sampling ports service of the AR INC653 layer e POK NEEDS ARINC653 ERROR activate the error service of the ARINC653 layer health monitoring functions e POK NEEDS BLACKBOARDS activate the blackboard service of POK intra partition communication e POK NEEDS SEMAPHORES activate the semaphore service of POK intra partition communication e POK NEEDS BUFFERS activate the buffer service of POK intra partition commu nication CHAPTER 5 CONFIGURATION DIRECTIVES 35 POK NEEDS ERROR HANDLING activate the error handling service in POK POK_NEEDS_DEBUG activate debug mode POK_NEEDS_LIBMATH activate the libmath functions that are available in regular service by passing the 1m flag to the compiler See libpok include libm h file for the list of functions Chapter 6 Examples 6 1 Assurance Quality At each source code change the developper must compile and check that examples compile fine on all supported architectures Consequently the available examples with the release compiles Sometimes you can experience some errors since the examples are not run If you think you find a bug please report it to the developper team 6 2 List of provided examples This section details each example and the services they use These examples are avail able in each release of POK e arinc653 blackboard test the blackboard service of the ARINC653 layer This tes
65. e cheddar events xml file For that use the menu Tool Scheduling Event Table Service Import and choose the generated cheddar events xml file Then to draw the scheduling diagram choose the menu option Tool Scheduling Event Table Service Draw Time Line 89 CHAPTER 9 INSTRUMENTATION 90 Cheddar will directly draw the scheduling diagram that corresponds to the execu tion Chapter 10 Annexes 10 1 Terms e AADL AADL stands for Architecture Analysis and Design Language It pro vides modeling facilities to represent a system with their properties and require ments e Leon3 A processor architecture developped by the European Space Agency Ocarina AADL compiler developed by TELECOM ParisTech It is used by the POK project to automatically generate configuration deployment and applica tion code PowerPC Architecture popular in the embedded domain e OEMU A general purpose emulator that runs on various platforms and emulates different processors such as INTELx86 or PowerPC 10 2 Resources e POK website http pok gunnm org e Ocarina website http aadl telecom paristech fr e QEMU website http www qemu com e Cheddar http beru univ brest fr singhoff cheddar e MacPorts http www macports org 91 O 00 109 tA fw ND CHAPTER 10 ANNEXES 92 10 3 POK property set for the AADL property set POK is Security Level aadlinteger applies to Means two things Criticality aadlinteger applie
66. e_BSP applies to processor system Available_Architectures type enumeration X86 ppc spare Architecture POK Available_Architectures applies to processor system Deployment properties Indicate which architecture we use and which bsp Source Location aadlstring applies to subprogram Indicate where is the object file that contains this subprogram MILS Verified aadlboolean applies to system process device thread processor data For verification purpose Refresh Time Time applies to data port Hw Addr aadlstring applies to device PCI Vendor Id aadlstring applies to device PCI Device ID aadlstring applies to device Device Name aadlstring applies to device Additional Features list of Supported Additional Features applies to virtual processor process 113 114 115 116 117 118 119 120 121 122 123 124 125 126 O 0 JAN RU ND CHAPTER 10 ANNEXES 94 Supported Additional Features type enumeration libmath libc stdlib libc stdio Des Key aadlstring applies to virtual bus Des Init aadlstring applies to virtual bus Blowfish Key aadlstring applies to virtual bus Blowfish Init aadlstring applies to virtual bus Supported POK Protocols type enumeration ceasar des blowfish unknown Protocol Supported POK Protocols applies to virtual bus end POK 10 4 AADL library This is not C code but an AADL library that can be used with yo
67. ecify the number of events we use for intra partition communications e POK CONFIG ALLOCATOR NB SPACES Indicate the number of spaces we should reserve in the memory allocator Since the memory allocator tries to reach deter minism the number of space is fixed So you have to specify how many spaces you want by defining this maccro e POK CONFIG ALLOCATOR MEMORY SIZE Indicate which amount of memory must be reserved for the memory allocator e POK HW ADDR Define the hardware address of the ethernet card This maccro is useful if the partition implements a device driver for a network device In POK and its libpok layer we use it for the RTL8029 device driver 5 6 Services activation To activate libpok services you must define some maccros By default you don t have any services You activate service by defining macros Thus it ensures that each partition contains only required services and avoid any memory overhead in partitions These maccros have the form POK NEEDS There is a list of these maccros e POK NEEDS RTL8029 activate the functions of the device driver that support the Realtek 8029 ethernet card e POK NEEDS STDLIB activate services of the standard library everything you can find in libpok include libc stdlib h e POK NEEDS STDIO activate the services of the standard Input Output library printf etc You can find available functions in 1ibpok include libc stdio h CHAPTER 5 CONFIGUR
68. ement 8 2 6 Blackboard service intra partition communication 8 2 7 Buffer service intra partition communication 8 2 8 Event service intra partition communication 8 2 9 Queuing ports service inter partition communication 8 2 10 Sampling ports service inter partition communication 8 3 ARINC653 Ada sa kolaa NE ems 8 3 1 APEXtypesandconstants 83 2 Blackboards o 200 000 ee eee 8 3 9 Butters AA m ts A Su MR Mea eg 5 3 4 LEVENS Ae es ac PS KIA IE AU ei ER S Be s 8 3 5 Health monitoring 8 3 6 Moduleschedules 8 3 7 Partitions ano Ros PR E KAKA Tana 53 8 V PIOCESSES oso Veg topi Sie red eO pe eee Ron X 83 9 Queuingports es 8 3 10 Sampling ports lt lt se 8 3 34 Semaphores ose ioni m RR Rr a Dini S 8 3 12 Timing su ms JR Kai RA aa CONTENTS 4 9 Instrumentation 86 9 1 Instrumentation purpose 86 9 2 Output files lt s ck EN REA Gu mm E 86 9 3 Use cheddar with produces files 86 10 Annexes 88 TOT SES Lata aa tots a de lina culete ds E 88 10 2 RESOURCES 7 202 o oue kie S b eR IRR A OR Sed O ee 88 10 3 POK property set for the AADL 89 10 4 AADLhbr ry 5 a A se eon R RR A SUK Aa 91 10 5 ARINC653 property set for the AADL 99 10 6 Network example modeling of device drivers
69. end ARINC653 10 6 Network example modeling of device drivers POK header LEVEL E CHAPTER 10 ANNEXES The following file is a part of the POK project be made according to the POK licence You CANNOT use this file or a g of a file for your own project 104 Any modification sh For more information on the POK licence please see our LICENCE FILE Please follow the coding guidelines described in doc CODING GUIDELINES Copyright c Created by julien on Mon May 18 18 44 51 2009 package rt18029 Be careful when you modify this file it is used in the annexes of the documentation public with POK with types data anydata end anydata subprogram init properties Source name gt rtl8029 init Source language gt C end init subprogram poll properties source name gt rt18029 polling Source language gt C end poll thread driver rt18029 thread features outgoing topsecret incoming topsecret outgoing secret incoming secret outgoing unclassified out data port types out data port types in data port types integer out data port types in data port types integer 2007 2009 POK team integer integer integer incoming unclassified in data port types integer properties Dispatch Protocol gt Periodic Compute Execution Time gt 0 ms 1 ms Period 1000 Ms end driver rt18029 thread thread driver rtl18029 thread poller properties
70. erated types and the names of the others type However the definitions given for these others types and the names and values given below for constants specific are all implementation All types have defining representation pragmas or clauses to ensure representation compatibility with the C and Ada 83 bindings Root package providing constant and type definitions ce CHAPTER 8 POK API 76 with System This is the Ada 95 predefined C interface package with Interfaces C package APEX is pragma Pure Domain limits Domain dependent These values define the domain limits and are implementation depen System Limit Number Of Partitions constant 32 module scope System Limit Number Of Messages constant 512 module scope System Limit Message Size constant 16410 0000454 module scope System Limit Number Of Processes constant 1024 partition scope System Limit Number Of Sampling Ports constant 1024 partition scope System Limit Number Of Queuing Ports constant 1024 partition scope System Limit Number Of Buffers constant 512 partition scope System Limit Number Of Blackboards constant 512 partition scope System Limit Number Of Semaphores constant 512 partition scope System Limit Number Of Events constant 512 partition scope The actual sizes of
71. es CHAPTER 2 INSTALLATION 10 e QEMU for x86 emulation e Ocarina for code generation only e TSIM for Leon3 emulation Note for MacOS users POK uses the ELF format to store partitions Unfortunately this binary format is not supported by Mac OS X tools To use POK you must use a development toolchain that supports the ELF format For that you can easily build an ELF cross compiler using MacPorts The name of the required packages are 1386 elf gcc and 1386 elf binutils Moreover Mac OS X does not provide necessary Perl modules but you can install them with MacPorts The package names are p5 xml xpath and p5 xml libxml 2 3 2 Running POK Ocarina is needed by POK A script is provided to automatically install the latest build sh misc get_ocarina sh You can then try to build and run some of the POK examples located in the exam ple directory cd examples partitions threads make make C generated code run A whole chapter of this documentation is dedicated to those examples and their purpose 2 4 Windows 2 4 1 Pre requires There is many pre requires to run POK on Windows To make a better user experience we provide cross development tools to build and use POK For cross development tools can be retrieved from the website of the project Then unzip the tools in a directory called crosstools at the root directory of the project Once you have this directory run the file configure bat located in th
72. et Module Schedule Status Schedule Status out Schedule Status Type Return Code out Return Code Type procedure Get Module Schedule Id System Time Type Schedule Id Type Schedule Id Type Schedule Name Schedule Id Return Code in Schedule Name Type out Schedule Id Type out Return Code Type 25 26 27 28 29 CHAPTER 8 POK API 82 private Type Schedule Id Type is new APEX Integer Null Schedule Id constant Schedule Id Type 0 pragma Convention C Schedule Status Type end APEX Module Schedules 8 3 7 Partitions with APEX Processes package APEX Partitions is Max Number Of Partitions constant System Limit Number Of Partiti type Operating Mode Type is Idle Cold Start Warm Start Normal type Partition Id Type is private Null Partition Id constant Partition Id Type type Start Condition Type is Normal Start Partition Restart Hm Module Restart Hm Partition Restart type Partition Status Type is record Period System Time Type Duration System Time Type Identifier Partition Id Type Lock Level APEX Processes Lock Level Type Operating Mode Operating Mode Type Start Condition Start Condition Type end record procedure Get Partition Status Partition Status out Partition Status Type Return Code out Return Code Type procedure Set Partition Mode Operating Mode in Operating Mode Type Return Code out Return Code Type
73. et outgoing nodel partition unclassified outgoing invalid local port invalid local port invalid local port When you use code generation functionnalities this declaration is automatically created in the deployment c file Location of each global port The location of each global port is specified with the pok ports nodes array It indi cates for each port the associated node identifier In the following example it shows that the three first global ports are located on the node 0 and the other on the node 1 uint8 t pok ports nodes POK CONFIG NB GLOBAL PORTS 0 0 0 1 1 1 When you use code generation functionnalities this declaration is automatically created in the deployment c file Specify the port type The kernel must know the kind of each port queuing or sampling We specify that requirement with the pok_ports_kind array There is an example of a such declaration below pok_port_kind_t pok_ports_kind POK_CONFIG_NB_PORTS POK PORT KIND SAMPLING POK PORT KIND SAMPLING POK PORT KIND SAMPLING Here the three local ports are sampling ports You can have three kind of ports 1 Sampling ports POK PORT KIND SAMPLING stores data but does not queue them 2 Queuing ports POK PORT KIND OUEUEING queues every new instance of the data 3 Virtual ports POK PORT KIND VIRTUAL this port is not stored in the kernel and this is a virtual port This port belongs to another machine We add it onl
74. forts When you use code generation functionnalities these declarations are automati cally created in the deployment h file e POK NEEDS PARTITIONS maccro indicates that you need partitioning services It implies that you define configuration maccros and variables for the partitioning service e POK NEEDS SCHED maccro specifies that you need the scheduler e POK NEEDS PCI maccro specifies that kernel will include services to use PCI devices e POK NEEDS IO maccro specifies that input output service must be activated so that some partitions will be allowed to perform i o e POK NEEDS DEBUG maccro specifies that debugging information are activated Additional output will be produced e POK_NEEDS_LOCKOBJECTS maccro specifies that you need the lockobject service It must be defined if you use mutexes or semaphores e POK_NEEDS_THREADS maccro that thread service must be activated e POK_NEEDS_GETTICK maccro that time service must be activated interrupt frame on timer interrupt is installed and clock is available e POK_NEEDS_SCHED_RR the Round Robin scheduling policy is included in the kernel e POK NEEDS SCHED RMS the Rate Monotonic Scheduling scheduling policy is included in the kernel e POK NEEDS SCHED EDF the Earliest Deadline First scheduling policy is included in the kernel e POK NEEDS SC the kernel ED_LLF the Last Laxity First scheduling protocol is included in e POK NEEDS SC nel ED_S
75. gzip wrapper i subcomponents 99 vbus ceasar wrapper i j 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 CHAPTER 10 ANNEXES 100 send subprogram gzip_send i receive subprogram gzip_receive i marshalling_type data gzip data i end vbus gzip wrapper i virtual bus gzip end gzip virtual bus implementation gzip i properties Implemented As end gzip i gt classifier poklib vbus gzip wrapper i virtual processor pok partition end pok partition virtual processor properties POK Scheduler gt RR end pok partition basic implementation pok partition basic virtual processor implementation pok partition driver properties POK Scheduler gt RR POK Additional Features gt pci io end pok partition driver virtual processor implementation pok partition application properties POK Scheduler RR POK Additional Features end pok partition application libe stdio libeostdlib virtual processor implementation pok partition basic for example extends properties POK Additional Features Tib stdio end pok partition basic for example gt libc stdlib s virtual processor implementation pok partition basic for example with li properties
76. has 4 threads Number of nodes The POK_CONFIG_NB_NODES specifies the number of nodes in the distributed system if you use a such architecture It is useful if you have more than one node and use network functionnalities define POK CONFIG PARTITIONS NTHREADS 2 2 2 4 CHAPTER 5 CONFIGURATION DIRECTIVES 26 Lockobjects allocation across partitions The POK CONFIG PARTITIONS NLOCKOBJECTS specifies the number of lock objects for each partition This declaration is an array each value n specifies how many lock objects we have for partition n There is an example of the use of this configuration directive Here the first parti tion will have one lockobject while the second partition will have three lockobjects define POK CONFIG PARTITIONS NLOCKOBJECTS 1 3 Scheduler of each partition level 1 of scheduling The POK CONFIG PARTITIONS SCHEDULER specifies the scheduler used in each parti tion This declaration is an array each value n corresponds to the scheduler used for partition n There is an example below Here the four partitions used the Round Robin sched uler define POK CONFIG PARTITIONS SCHEDULER POK SCHED RR POK SCHED RR POK SCHED RR POK SCHED RR Scheduler of partitions level 0 of scheduling The scheduling of partitions is specified with several maccros The POK_CONFIG_SCHEDULING_NBSLOTS specifies the number of time frames allo cated for partitions execution The POK_CONFIG_SCHEDULING_SLOTS specifies
77. hitecture is illustrated in figure 7 1 The kernel executes the parti tions each partition contains its application code Drivers are executed in partitions and don t reside inside the kernel To build a such architecture you must have e For each partition The application code The configuration code e For the kernel The configuration code Then each part of the system is compiled and integrated as depicted in figure 7 2 The kernel is compiled and each partitions is compiled Eeach part produces a binary file Since POK relies on the ELF file format each binary of each part is compiled into an ELF file Then we integrate ALL ELF files to produce a single bootable binary so that the final binary contains different binaries the code for the kernel and the code of all partitions Since POK relies on the ELF file format the final ELF file contains other ELF files The organization of the final binary is depiceted in figure 7 3 When kernel boots it loads each elf file of each partition in a different memory segment to achieve space isolation So each ELF file of each partition is loaded in a single and protected memory area of the system 72 2 Executive architecture At this time the execute architecture pattern is not finished CHAPTER 7 ARCHITECTURE 41 Kernel Partition 1 Partition N de gt 1 lt gt cs EI EA BOY A H 1 o n o o o a H 3 3 v
78. ic library service We also add mathematic functions to ease the portability of third party code These functions were imported from the NetBSD project It provides all necessary functions to perform math operations sqrt To enable the libmath functions you must define the maccro POK_NEEDS_LIBMATH To have the complete list please refer to the libpok reference manual available on each POK release A list of these functions is also available in this document in chapter 8 7 4 5 Protocols The libpok layer contains predefined protocols to marshall unmarshall application data before sending them on the network These protocols library could be used for several purposes encrypt data before sending it on an unsecure network adapt application data to constrained protocols such as CORBA These protocols can be automatically used through AADL models and appropriate properties associated to AADL data ports on AADL process components To have more information about AADL and protocol binding see section 4 At this time the libpok layer is focuses on crypto and provides the following pro tocols e Ceasar e DES e SSL For each protocol we have e A function to marshall data e A function to unmarshall data http www netbsd org CHAPTER 7 ARCHITECTURE 45 e An associated type if the protocol needs a special data type to store marshalled values Marshalling functions and types are described in their header files
79. if incomin g gt nodel netif incomiir gt nodel netif incomii e of this node g topsecret g secret g unclassified Ports of partitions of the second node are connected to the device of this second node port port port node2 netif outgoing topsecret node2 netif outgoing secret node2 netif outgoing unclassif port nodel netif outgoing topsecret Actual Connection Binding gt port nodel netif outgoing secret Actual Connection Binding gt reference reference node2 partition topsecret i node2 partition secret incomind ied node2 partition unclassi gt node2 netif incoming tops rtbus layer topsecret node2 netif incoming secret rtbus layer secret port Actual Connection Binding gt bus access rtbus bus access rtbus properti Actua ies to Actua ies to Actua Actua ies to Actua ies to Actua Actua ies to Actua ies to Actua ies to app app app app app app app ies to Actua ies to Actua ies to Actua ies to Actua ies to Actua ies to Actua ies to end main app app app app app app app end model Actual nodel netif outgoing unclassified nodel netif the bus gt node2 netif the bus es l Processor Binding reference nodel partition topsecret l Processor Binding gt reference nodel partition secret l Processor Binding gt reference 1 Processor Binding gt reference n
80. ilo gt o gt i O il O ao a o ao a n 8 A po S D lo 9 c9 oS A b pA sa ga O PD i ta a 23 lo Po 3 i S Sol 18 Sog a i o 35 2 o 352 3 i 3 n S n T os o lt o o Q o 5 i i Sd a E Binary Binary Binary Partition and kernel linking Bootable binary Figure 7 2 Build steps for a partitioned system POK Kernel Partition 1 Partition 2 Partition 3 Include symbols data code ELF format ELF format ELF format Figure 7 3 ELF file format of a POK system CHAPTER 7 ARCHITECTURE 42 7 3 Kernel services 7 3 1 Partitioning service The partitioning service of POK isolates code in time and space Each partition has one or more time slots to execute their code and they are isolated in a memory segment Using this design guideline one partition cannot access the memory of other par titions and vice versa During partitions initialization POK automatically creates a memory segment for each partition and copy its code into this protected space However partitions can communicate with other partitions using so called ports Inter partitions ports are also supervised by the kernel in order to avoid unallowed communication channel See section 7 3 4 for more information Partitions have time slots to execute their threads During this execution time they schedule their threads according to their own scheduling protocol so that partitions ca
81. ing id name id N 117 pok syscall2 POK SYSCALL MIDDLEWARE SAMPLING ID uint32 t name umint32 t id us 119 Similar to 120 pok ret t pok port sampling id char name 121 pok port id t id 122 xy 123 124 define pok port sampling status id status 125 pok syscall2 POK SYSCALL MIDDLEWARE SAMPLING STATUS uint32 t id uint32 t status 126 127 Similar to 128 pok ret t pok port sampling status const pok port id t id 129 const pok port sampling status t status 130 T 13 endif 132 133 endif 8 1 6 Intra partitions communications Configuration Blackboards 1 2 3 ifndef __POK_USER_BLACKBOARD_H__ 4 define __POK_USER_BLACKBOARD_H__ 5 6 ifdef POK_NEEDS_MIDDLEWARE 7 ifdef POK_NEEDS_BLACKBOARDS 8 9 include lt types h gt 10 include lt errno h gt 12 typedef struct 13 14 pok_size_t size 15 pok_bool_t empty eune u CHAPTER 8 POK API pok_range_t waiting_processes pok_size_t index pok_bool_t ready pok_event_id_t lock pok blackboard t typedef struct pok_port_size_t msg_size pok_bool_t empty pok_range_t waiting_processes pok blackboard status t pok ret t pok blackboard create char name const pok size t msg size pok blackboard id t id 54 pok ret t pok blackboard read const pok blackboard id t id const uint64 t timeout void data pok port size t len pok ret t pok bl
82. ipline Type is Fifo Priority pragma Convention C Queuing Discipline Type subtype System Time Type is APEX Long Integer 64 bit signed integer with 1 nanosecond LSB Infinite Time Value constant System Time Type Aperiodic constant System Time Type Zero Time Value constant System Time Type private Infinite Time Value constant System Time Type 1 Aperiodic constant System Time Type 0 Zero Time Value constant System Time Type 0 end APEX 8 3 2 Blackboards with APEX Processes package APEX Blackboards is Max Number Of Blackboards constant System Limit Number Of Blackb subtype Blackboard Name Type is Name Type type Blackboard Id Type is private Null Blackboard Id constant Blackboard Id Type type Empty Indicator Type is Empty Occupied type Blackboard Status Type is record Empty Indicator Empty Indicator Type Max Message Size Message Size Type Waiting Processes APEX Processes Waiting Range Type end record procedure Create Blackboard Blackboard Name in Blackboard Name Type Max Message Size in Message Size Type Blackboard Id out Blackboard Id Type Return Code out Return Code Type procedure Display Blackboard Blackboard Id in Blackboard Id Type Message Addr in Message Addr Type Length in Message Size Type Return Code out Return Code Type procedure Read Blackboard Blackboard Id in Blackboard Id Type Time Out in System
83. is directory Is everything is wrong a warning will be displayed on the screen For code generation you can install Ocarina for Windows All installation instruc tions are available on Ocarina website Chapter 3 Getting started 3 1 First experience with POK To build and run your first system with POK you must have the Ocarina code genera tor and all the software required by POK a list is available in the chapter 2 Then perform the following actions 1 Issue make configure at the top directory of POK Is something is missing install it 2 Enter the directory examples partitions threads by typing this command in a terminal cd examples partitions threads 3 Invoke make It will generate configuration and application code with Ocarina 4 Invoke make run in the generated code directory You can do that with the following commands make C generated code run Using this command gemu is launched and your system is being executed Now the next sections will explain how to configure the kernel and the partition layer for your own projects Available at http aadl telecom paristech fr 11 CHAPTER 3 GETTING STARTED 12 3 2 Development cycle POK has a dedicated development cycle which avoid the compilation of the kernel The development process automatically compiles the kernel the partitions with the application code and assemble them into a bootable binary you can see the illustration of this develo
84. n Code Type procedure Signal Semaphore Semaphore Id in Semaphore Id Type Return Code out Return Code Type procedure Get Semaphore Id Semaphore Name in Semaphore Name Type Semaphore Id out Semaphore Id Type Return Code out Return Code Type procedure Get Semaphore Status Semaphore Id in Semaphore Id Type Semaphore Status out Semaphore Status Type Return Code out Return Code Type private type Semaphore Id Type is new APEX Integer Null Semaphore Id constant Semaphore Id Type 0 pragma Convention C Semaphore Status Type POK BINDINGS pragma Import C Create Semaphore CREATE SEMAPHORE 49 50 51 52 53 54 Uk w P CHAPTER 8 POK API pragma Import C Wait Semaphore WAIT SEMAPHORE pragma Import C Signal Semaphore SIGNAL SEMAPHORE pragma Import C Get Semaphore Id GET SEMAPHORE ID pragma Import C Get Semaphore Status GET SEMAPHORE STATUS END OF POK BINDINGS end APEX Semaphores 88 8 3 12 Timing TIME constant and type definitions and management services package APEX Timing is procedure Timed Wait Delay Time in System Time Type Return Code out Return Code Type procedure Periodic Wait Return Code out Return Code Type procedure Get Time System Time out System Time Type Return Code out Return Code Type procedure Replenish Budget Time in System Time Type Return Code out Return Code Ty
85. n schedule their threads in an independent way This scheduling strategy is often described as a hierarchical scheduling 7 3 2 Thread service The thread service executes tasks The system is built to execute a predefined number of tasks When using partitioning services each partitions has a predefined amount of tasks The scheduler can be preemptive so that tasks can interrupt each other The thread service can start stop or pause a task sleep 7 3 3 Time service The time service provides an efficient way to manage the time on your machine It is used by the scheduler to scheduler partitions and tasks according to their timing requirements period execution time and so on 7 3 4 Communication service The kernel provides communication services It allows partitions and threads to com municate The communication service is achieved using ports Out ports ports that send data can have several destinations while in ports ports that receive data can have only one source Data are sent and received on this ports The kernel configuration specifies the owner of a port its destination and its size If you use partitioning service each port is dedicated to a partition Consequently when creating the port the kernel checks that requested port belongs to the partition Communication using network When using the network the port must be bound to a network interface so that data from to the port will be sent over the network The
86. ncurrency protocol by defining the Concurrency Control Protocol property 4 5 7 Protocols You can describe which protocol you want to use in your system using a protocol layer You specify the protocol layer using virtual bus components FIXME complete once the work around virtual bus is finalized 4 6 POK AADL library POK provides an AADL library for rapid prototyping of partitioned embedded archi tectures This library contains predefines components associated with relevant proper ties to generate a partitioned architecture The file that contains this AADL library is located in misc aadl library aadl 4 7 Examples Examples of AADL models can be found in the examples directory of the POK archive Chapter 5 Configuration directives This chapter details the different configuration directives for kernel and partitions The configuration of kernel and partitions is made using C code You must write it carefully since a mistake can have significant impacts in terms of safety or security Most of the time the C configuration code will be maccros in global variables The purpose of this chapter is to detail each variable If you use generated code the configuration code is mostly generated in deployment c and deployment h files 5 1 Automatic configuration from ARINC653 XML files You can automatically generate the configuration of your kernel using ARINC653 XML deployment files For that we designed a tool that analyzes ARIN
87. need to describe partitions in your AADL model In that case partitions are mapped with two AADL components process and virtual processor The virtual processor models the runtime of the partition its scheduler needed functionalities and so on We associate the virtual processor component partition runtime and its process component partition address space with the Actual Processor Binding property Scheduling The scheduling policy of the partition is specified with the POK Scheduler property in the virtual processor component partition runtime Memory requirements You can specify the memory requirements in two ways First with the POK Needed Memory Size property on the process partition ad dress space It will indicate the needed memory size for the process CHAPTER 4 AUTOMATIC CONFIGURATION AND CONFIGURATION WITH AADL MODELS21 You can also specify memory requirements with AADL memory components You bind a memory component to a partition process component with the Actual Memory Binding property In that case the properties Word_Size Word_Count of the memory component will be used to generate its address space Additional features You can specify which features are needed inside the partition libc libmath and so on In that case you have to specify them with the POK Additional Features property 4 5 4 Threads ARINC653 processes Threads are contained in a partition Thus these components are c
88. nt process 4 2 Use the pok toolchain for model analysis validation code generation compilation and execution the pok toolchain pl script 4 2 1 Usethe pok toolchain piscript 4 2 2 FExampleofuse NK 4 3 Model validation is di 464 ES 4 4 POK properties for the AADL 4 5 Modelingpatterms ASA Kerels m6 JA ri a A EUMD 45 2 Device drivers assa e a eee TRES 4 5 8 Partitions s ari sta sei LA As 4 54 Threads ARINC653 processes 4 5 5 Inter partitions channels 4 5 6 Intra partitions channels Az MPINA oe ico Eh le a mS 46 POKAADLIbrary AT Examples ae a Re RH doe Sd WES 5 Configuration directives 5 1 Automatic configuration from ARINC653 XML files 5 2 Common configuration 5 3 Kernel configuration ss se 5 3 1 Services activation 5 3 2 Generalconfiguration 5 3 3 Partitionsconfiguration 5 3 4 Number of partitions 5 3 5 Inter partitions ports communication 5 4 Libpok partition runtime 5 5 Configuration gt sop RS 6885 448 RU Ray eU 5 6 Services acfiValloD s oo tenendo ERR URGE UAR A 6 Examples 6 1 AssuranceQuality ee 6 2 Listofprovidederamples 7 Architecture
89. ode2 partition topsecret l Processor Binding reference node2 partition secret l Processor Binding gt reference 1 Processor Binding gt reference nodel netif l Processor Binding gt reference node2 netif Memory Binding gt reference nodel partition topsecret emory Binding reference nodel partition secret Memory Binding gt reference nodel_partition_unclassified _Memory_Binding gt reference node2_partition_topsecret _Memory_Binding gt reference node2_partition_secret _Memory_Binding gt reference node2_partition_unclassified _Memory_Binding gt reference node2_netif _Memory_Binding gt reference nodel_netif lt i reference gt node2_netif incoming_ nodel runtime_topsecret nodel runtime secret nodel node2 runtime_topsecret node2 runtime_secret node2 runtime unclassifig nodel runtime netif node2 runtime netif nodel memory topsecret nodel memory secret nodel_memory unclassified node2 memory topsecret node2 memory secret node2 memory driver node2 memory nodel memory driver runtime unclassifi d coming ied incoming ecret did i nclassified rtbus layer_unclassified applies to nodel_partit d applies to node2_partit unclassified
90. omponent models the driver by defining a process that contains threads These threads handle the device and perform function calls to access to hardware re sources However for each device POK must know which device you are actually using So you have to specify the POK Device Name property It is just a string that indicate which device driver you are using with this device component In addition for network device that represent ethernet buses you must specify the hardware address also known as the MAC address For that we have the property POK Hw_Addr This property must be associated with a device component Supported device drivers At this time we only support one device driver the realtek 8029 ethernet controller This device is simulated by QEMU and thus can be easily tested and simulated on every computer that uses QEMU However implementing other device driver can be easily achieved by changing the Device_Name property in the model and adding some functions in the 1ibpok layer of POK Case study that defines a device driver You can find an example of an implementation of a device driver in the examples network directory of each POK release It defines two ARINC653 module that communicate across an ethernet network Each module contains one partition that communicate over the network You can have more information by browsing the examples network directory 4 5 3 Partitions In case of a partitioned architecture we
91. ontained in a process component which models a partition There is the supported properties for threads declaration e Source Stack Size the stack size of the thread e Period the actual period of the thread execution rate e Deadline the actual deadline of the thread when the job should finish e Compute Exeution Time the execution time needed to execute the application code of the threads 4 5 5 Inter partitions channels Queuing ports Queuing ports are mapped using AADL event data ports connected between AADL processes This ports are also connected to thread components to send receive data Sampling ports Queuing ports are mapped using AADL data ports connected between AADL pro cesses This ports are also connected to thread components to send receive data 4 5 6 Intra partitions channels Buffers Buffers are mapped using AADL event data ports connected between AADL threads This ports must not be connected outside the process Blackboards Buffers are mapped using AADL data ports connected between AADL threads This ports must not be connected outside the process CHAPTER 4 AUTOMATIC CONFIGURATION AND CONFIGURATION WITH AADL MODELS22 Events Buffers are mapped using AADL event ports connected between AADL threads This ports must not be connected outside the process Semaphores Semaphores are mapped using a shared AADL data component between several AADL thread components The shared data component must use a co
92. otocol gt blowfish 167 end blowfish i 168 169 DES virtual bus 170 171 subprogram des send 172 features 173 datain in parameter poklib pointed_void 174 count in in parameter poklib integer 175 dataout out parameter poklib pointed void 176 count out out parameter poklib integer 177 end des send 178 179 subprogram implementation des send i 180 properties 181 Source Name pok protocols des marshall 182 end des send i 183 184 subprogram des receive 185 features 186 datain in parameter poklib pointed_void 187 countin in parameter poklib integer 188 dataout out parameter poklib pointed_void 189 countout out parameter poklib integer 190 end des receive 191 192 subprogram implementation des receive i 193 properties 194 Source Name gt pok protocols des unmarshall 195 end des receive i 196 197 data des data 198 end des data 199 200 data implementation des data i 201 properties 202 Type Source Name gt pok protocols des data t 203 end des data i 204 205 abstract vbus des wrapper 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 233 254 255 256 257 258 259 260 261 262 CHAPTER 10 ANNEXES 98 end vbus_des_wrapper
93. pe POK BINDINGS pragma Import C Timed Wait TIMED WAIT pragma Import C Periodic Wait PERIODIC WAIT pragma Import C Get Time GET TIME pragma Import C Replenish REPLENISH END OF POK BINDINGS end Apex Timing Chapter 9 Instrumentation You can automatically instrument POK using the with instrumentation option when you configure the build system see section 3 3 for more information In con sequence when you use this mode more output is produced and additional files are automatically created when the system stops This section details the files that are automatically produced in this mode and how to use them 9 1 Instrumentation purpose At this time the instrumentation functionnality was done to observe scheduling of partitions and tasks in the Cheddar scheduling analysis tool If you want to use this functionnality you have to install Cheddar see 10 2 for information about Cheddar 9 2 Output files When you run your system using the make run command and if the instrumentation configuration flag was set the following files are automatically produced e cheddar archi xml contains the architecture used with the POK kernel e cheddar events xml contains the scheduling events that are registered during POK execution 9 3 Use cheddar with produces files Start Cheddar Then load the XML file cheddar archi xml You can also use Ched dar with this file as an argument Then load th
94. pment process in figure 7 2 Due to the tedious configuration efforts of each layer a tool that automatically con figures the kernel and the partitions from AADL descriptions is available the Ocarina code generator You can also configure each part by yourself by writing C configura tion code 3 3 Configure POK the conf env pl script POK distribution can be configured so reach different goals The basic configuration 1s automatically performed However in some cases you want to use some additional options At first the configuration of POK is made with the conf env pl script located in the misc directory So issue misc conf env pl to use the default configura tion The configuration is automatically produced by this script and written in the misc mk config mk file Then the conf env p1 script can be used with additional switches to enable some options of POK There is a list of these switches e help print help menu e with xcov use xcov from the coverage project With this option when you invoke make run after building a system the emulator will be stopped after 40 seconds of execution and analyses the code coverage of the system e with floppy add an additional rule so that you can automatically install the POK binary into a bootable floppy In consequence you can invoke make install in the generated directory to create this floppy disk image e with instrumentation automatically insrument kernel and par
95. r is JULIEN DELANGE who did his PhD on partitioned architectures http www telecom paristech fr 2http www lip6 fr CHAPTER 1 INTRODUCTION 8 However several students from the EPITA school joined the project and improve for several purposes projects exercises fun In addition other people contributed to the project for several reasons There is a list of the people involved in the project alphabetical order e Fabien Chouteau LEON port e Tristan Gingold PowerPC port e Franois Goudal initial version known as the Gunther project e Laurent Lec Realtek 8029 driver kernel IPC and so on e Pierre Olivier Haye memory protection e Julian Pidancer initial work on partition isolation Hope the team will grow up in a near future 3http www epita fr Chapter 2 Installation 2 1 Supported development platforms e Linux e MacOS X e Windows 2 2 Get more information The following information are the standard procedures It may be out of date or miss something In that case you will find updated information on the POK website http pok gunnm org and its wiki section In addition there are some tutorials and information about the installation of re quired tools 2 3 Linux MacOS 2 3 1 Pre requires e The GNU C Compiler aka GCC version 3 x or 4 x e GNU binutils e GNU Zip aka gzip e Mtools MS DOS disk utilities e AWK e Perl with XML XPath XMLParser and XML LibXML modul
96. rovide the application level code This application level code can be traditional code Ada C or application models Simulink Scade etc Our code generator was integrated in the Ocarina AADL toolsuite It is a popu lar toolsuite for AADL models handling It provides several functionnalities such as models analysis verification and code generation In the context of POK we rely on these functionnalities to verify and automatically implement the system The development process is illustrated in the figure 4 1 the developper provides AADL models the code generator creates code that configures kernel and libpok lay ers Compilation and integration is automatically achieved by the toolchain and creates final binary runnable on embedded hardware 16 CHAPTER 4 AUTOMATIC CONFIGURATION AND CONFIGURATION WITH AADL MODELS17 4 2 Security 8 Safety AADL Model verifications 1 C User code Code generation 2 Generated code Partitioned ernel amp middleware Compilation 3 Figure 4 1 Model Based development process Use the pok toolchain for model analysis valida tion code generation compilation and execution the pok toolchain pl script We provide a toolchain that provides the following functionnalities 1 2 3 4 Model analysis check that your AADL model is correct Model validation validate the requirements specified in the model Code generation automatically generate the code for its e
97. s to Handler aadlstring applies to Topics list of aadlstring applies to Means two things Needed Memory Size Size applies to process We apply it to process component because we don t Available Schedulers type enumeration Timeslice Time applies to virtual processor Major_Frame Time applies to processor Scheduler Available_Schedulers Slots list of Time applies to processor Slots_Allocation list of reference virtual processor applies to p virtual processor virtual bus process bus event data port security level that a partition is allowed to access security level provided by a virtual bus ensure that the virtual bus can transport data from and or to partitions that have this security level virtual processor Represent the criticality level of a partition virtual processor Error handler for each partition By default the code generator can create a function which name derives from the partition name Instead the model can provide the name of the handler with this property virtual processor virtual bus The topics allowed on a specific virtual processor Topics allowed on a virtual bus Specify the amount of memory needed for a partition isolate virtual processor only processes RMS EDF LLF RR TIMESLICE STATIC DEPRECATED at this time applies to processor virtual processor List available schedulers When we u
98. se the STATIC scheduler in the virtual processor The Slots and Slots_Allocation properties are used to determine whd event port ocessor data port 56 57 59 60 6l 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 CHAPTER 10 ANNEXES 93 partitions are activated and the timeslice they have for their exe Supported Error Code type enumeration Deadline Missed Application Er Recovery Errors list of Supported Error Code applies to processor y Supported Recovery Action type enumeration Ignore Confirm Recovery Actions list of Supported Recovery Action applies to There is two properties that handle errors and their recovery at the These two properties must be declared both in the component For example we declare the properties like that Recovery Errors gt Deadline Missed Memory Violation Thread Restart procegsor ution ror Numeric_Error Illegal virtual processor thread Thread_Stop_And_Star virtual processor thr processor and virtual proc Recovery Actions gt Ignore Partition Restart It means that if we have a missed deadline we ignore the error But if we get a memory violation error we restart the partition Available BSP type enumeration x86 gemu prep leon3 BSP POK Availabl
99. status t status endif endif id current vd max value discipling lue is u PUN o 0 41 o W RO OU P CHAPTER 8 POK API 8 1 7 C library Standard Input Output 57 ifndef POK_LIBC_STDIO_H define POK_LIBC_STDIO_H include lt stdarg h gt int vprintf const char format va_list args int printf const char format endif POK LIBC STDIO H Standard Lib ifndef POK_STDLIB_H define POK_STDLIB_H include lt types h gt define RAND_MAX 256 int rand void calloc size_t count size_t size void malloc size_t size void free void ptr endif String functions tifndef POK LIBC STRING H define POK_LIBC_STRING_H include lt types h gt Char itoa int value char buff int radix void memcpy void dest const void src size_t count void memset void dest unsigned char val size_t count int strcmp const char s1 const char s2 int strncmp const char sl const char s2 size t size size_t strlen const char s char strcpy char dest const char str char strncpy char dest const char str size_t size int memcmp const void vl const void v2 size t n CHAPTER 8 POK API XXX int TO REMOVE streq char s1 char s2 endif r 58 8 1 8 Math functions ifdef POK_NEEDS_LIBMATH ifndef define __POK_LIBM_H_
100. t Return Code Type procedure Unlock Preemption Lock Level out Lock Level Type Return Code out Return Code Type procedure Get My Id Process Id out Process Id Type Return Code out Return Code Type procedure Get Process Id Process Name in Process Name Type Process_Id out Process_Id_Type Return_Code out Return_Code_Type procedure Get_Process_Status Process_Id in Process_Id_Type Process_Status out Process_Status_Type Return_Code out Return_Code_Type private type Process_ID_Type is new APEX_Integer Null Process Id constant Process Id Type 0 pragma Convention C Process State Type pragma Convention C Deadline Type pragma Convention C Process Attribute Type pragma Convention C Process Status Type POK BINDINGS pragma Import C Create Process CREATE PROCESS pragma Import C Set Priority SET PRIORITY pragma Import C Suspend Self SUSPEND SELF pragma Import C Suspend SUSPEND pragma Import C Resume SUSPEND pragma Import C Stop Self STOP SELF pragma Import C Stop STOP pragma Import C Start START pragma Import C Delayed Start DELAYED START pragma Import C Lock Preemption LOCK PREEMPTION pragma Import C Unlock Preemption UNLOCK PREEMPTION pragma Import C Get My Id GET MY ID pragma Import C Get Process Id GET PROCESS ID pragma Import C Get Process Status GET PROCESS STATUS END OF
101. t Status Type POK BINDINGS pragma Import C Create Sampling Port CREATE SAMPLING PORT pragma Import C Write Sampling Message WRITE SAMPLING MESSAGE 56 57 58 59 60 CHAPTER 8 POK API 87 pragma Import C Read_Sampling_Message READ_SAMPLING_MESSAGE pragma Import C Get Sampling Port Id GET SAMPLING PORT ID pragma Import C Get Sampling Port Status GET SAMPLING PORT STATUS END OF POK BINDINGS end APEX Sampling Ports 8 3 11 Semaphores with APEX Processes package APEX Semaphores is Max Number Of Semaphores constant System Limit Number Of Semaphoi Max Semaphore Value constant 32 767 subtype Semaphore Name Type is Name Type type Semaphore Id Type is private Null Semaphore Id constant Semaphore Id Type type Semaphore Value Type is new APEX Integer range 0 Max Semaphore Value type Semaphore Status Type is record Current Value Semaphore Value Type Maximum Value Semaphore Value Type Waiting Processes APEX Processes Waiting Range Type end record procedure Create Semaphore Semaphore Name in Semaphore Name Type Current Value in Semaphore Value Type Maximum Value in Semaphore Value Type Queuing Discipline in Queuing Discipline Type Semaphore Id out Semaphore Id Type Return Code out Return Code Type procedure Wait Semaphore Semaphore Id in Semaphore Id Type Time Out in System Time Type Return Code out Retur
102. t contains partitions runtime AADL virtual processor components Scheduling The scheduling requirements are specified in process components properties The POK Slots and POK Slots_Allocation properties indicate the different time slots for partitions execution in case of a partitioned architecture In addition the POK Scheduler is used to describe the scheduler of the processor If we implement an ARINC653 architecture the scheduler would be static 4 5 2 Device drivers In POK device drivers are executed in partitions It means that you must embedds your code in partitions and drivers are isolated in terms of time and space Consequently drivers rely on the kernel to gain access to hardware resources I O DMA and so on To do that AADL components are considered as partitions So when your model contains an AADL device the underlying code generator consider that it is a partition So you have to associate device components with virtual processor components to indicate the partition runtime of your driver However the device driver cannot describe the actual implementation of the driver For that we use the Implemented As property This property points to an abstract com ponent that contains the implementation of our driver Annexes of the current document provide an example of the modeling of a driver see section the driver rt18029 CHAPTER 4 AUTOMATIC CONFIGURATION AND CONFIGURATION WITH AADL MODELS20 abstract c
103. t outgoing deployment destinations nodel partition unclassified outgoing deployment destinations Convert local port to global ports The association conversion between each local and global ports is given with the pok local ports to global ports array For each local port identifier we specify the associated global port value An example is given below Here the first local port corresponds to the global port identifier nodel partition secret outgoing global uint8 t pok local ports to global ports POK CONFIG NB PORTS nodel partition secret outgoing global nodel partition topsecret outgoing global nodel partition unclassified outgoing global When you use code generation functionnalities this declaration is automatically created in the deployment c file Convert global port to local port It is sometimes needed to convert a global port value to a local port You can have this information with the pok global ports to local ports The definition of this array is different on all nodes It specifies the local port identifier on the current node with each global port If the global port is not on the current node we specify the invalid port value An example is given below We can see that the three last ports are not located on the current node CHAPTER 5 CONFIGURATION DIRECTIVES 31 uint8_t pok_global_ports_to_local_ports POK_CONFIG_NB_GLOBAL PORTS nodel partition secret outgoing nodel partition topsecr
104. t relies on an AADL model that describe a blackboards between two tasks arinc653 buffer test the buffer service of ARINC653 It uses AADL models arinc653 queueing test ARINC653 queuing ports with AADL arinc653 sampling test ARINC653 sampling ports with AADL arinc653 threads test ARINC653 processes instanciation Uses AADL mod els case study aerotech09 An ARINC653 examples case study for the AEROTECHO9 conference It uses two partitions that communication temperature across inter partitions communications case study sigada09 a system that contain three partitions with different de sign patterns non preemptive scheduler ravenscar partition queued buffers This example was used as use case for a publication in the SIGAda conference SIGAda09 36 CHAPTER 6 EXAMPLES 37 case study mils a distributed with two nodes that communicate data at differ ent security levels Data are encrypted using cipher algorithms provided by the libpok layer case study ardupilot a case study made from application code found in the ardupilot project See http code google com p ardupilot for docu mentation about this application code case study integrated a case study that shows we can use POK for real avion ics architecture For that we define an avionics architecture using AADL and generates code for POK using Ocarina The initial model is defined by the Soft ware Engineering Instute SEI See http www aadl info aadl
105. tanf float x atan2 double y double x atan2f float y float x atanh double x atanhf float x cbrt double x cbrtf float x ceil double x ceilf float x copysign double x double y copysignf float x float y cos double x cosf float x cosh double x coshf float x drem double x double y dremf float x float y erf double x erff float x exp double x expf float x expml double x expmlf float x fabs double x fabsf float x finite double x finitef float x floor double x floorf float x frexp double x int eptr frexpf float x int eptr gamma double x gammaf float x gamma_r double x int signgamp gammaf_r float x int signgamp hypot double x double y hypotf float x float y ilogb double x ilogbf float x isinf double x isinff float x isnan double x isnanf float x j0 double x jOf float x 31 double x jJif float x jn int n double x jnf int n float x ldexp double value int exp0 ldexpf float value int exp0 lgamma double x lgammaf float x lgamma_r double x int signgamp lgammaf r float x int signgamp log double x 59 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 145 146 147
106. the deployment h file Number of local ports The number of local ports in the current node is specified using the POK CONFIG NB PORTS maccro It specifies the number of ports on the local node When you use code generation functionnalities this declaration is automatically created in the deployment h file Local ports identifiers The local ports identifiers are specified in an enum with the identifier pok port local identifier t In this enum you must ALWAYS add an identifier for an invalid identifier called invalid identifier Note that this enum declaration specifies the local ports of the current node and consequently it is dependent on each node communication re quirements When you use code generation functionnalities this declaration is automatically created in the deployment h file There is an example of a such enum declaration typedef enum nodel_partition_secret_outgoing 0 nodel partition topsecret outgoing nodel partition unclassified outgoing invalid local port 3 pok port local identifier t 1 25 Global ports identifiers The global ports identifiers is specified using an enum called pok port identifier t This enum declaration must be THE SAME on all node of the distributed system When you use code generation functionnalities this declaration is automatically created in the deployment h file There is an example of a such enum declaration typedef enum nodel_partition_secret_outgoing
107. the size in milliseconds of each slot The POK CONFIG SCHEDULING SLOTS ALLOCATION specified the allocation of each slot In other words which partition is scheduling at which slot The declaration is an array and the value n specifies which partition uses the slot n The POK_CONFIG_MAJOR_FRAME specifies the major frame the time when inter partitions ports are flushed It corresponds to the end of a scheduling cycle An example is provided below Here we have four partitions We declare 4 slots of 500ms The first slot is for the first partition the second slot for the second partition and so on The major frame time when scheduling slots are repeated is 2s 2000ms define POK CONFIG SCHEDULING SLOTS 500 500 500 500 define POK CONFIG SCHEDULING SLOTS ALLOCATION 0 1 2 3 define POK CONFIG SCHEDULING NBSLOTS 4 define POK CONFIG SCHEDULING MAJOR FRAME 2000 CHAPTER 5 CONFIGURATION DIRECTIVES 27 Partitions size The POK CONFIG PARTITIONS SIZE maccro specifies an array with partitions size in bytes The declaration is an array each value n represent the size of partition n There is an example of a such declaration below Here we have 4 partitions The three first partition have a size of 80000 bytes while the last one has a size of 85000 bytes define POK CONFIG PARTITIONS SIZE 80000 80000 80000 85000 5 3 5 Inter partitions ports communication For inter partitions
108. these base types are system specific and must match those of the underlying Operating System type APEX Byte is new Interfaces C unsigned char type APEX Integer is new Interfaces C long type APEX Unsigned is new Interfaces C unsigned long type APEX Long Integer is new Interfaces Integer 64 If Integer 64 is not provided in package Interfaces any implementa defined alternative 64 bit signed integer type may be used No Error request valid and operation performed No Action status of system unaffected by request Not Available resource required by request unavailable Invalid Param invalid parameter specified in request Invalid Config parameter incompatible with configuration Invalid Mode request incompatible with current mode Timed Out time out tied up with request has expired pragma Convention C Return Code Type Max Name Length constant 30 subtype Name Type is String 1 Max Name Length dent tion 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 CHAPTER 8 POK API 77 subtype System_Address_Type is System Address subtype Message_Addr_Type is System Address subtype Message_Size_Type is APEX_Integer range 1 System Limit Message Size subtype Message Range Type is APEX Integer range 0 System Limit Number Of Messages type Port Direction Type is Source Destination pragma Convention C Port Direction Type type Queuing Disc
109. tions virtual processor poklib pok_partition basic_for_examplg virtual processor poklib pok partition basic Fror example Frame 1000ms ler gt static 500ms 500ms Allocation gt reference partitionl reference partiti x86 qemu two partitions extends pok kernel x86 gemu n2 processor implementation pok kernel x86 gemu three partitions extends pok_kernel x86_qemu subcomponents partitionl partition2 partition3 properties POK Major_ POK Schedu POK Slots POK Slots end pok_kernel processor impl subcomponents partitionl partition2 partition3 partition4 properties POK Major_ POK Schedu POK Slots PORK 33 Slotsu end pok_kernel processor impl subcomponents partitionl partition2 partition3 virtual processor poklib pok_partition basic_for_examplg virtual processor poklib pok_partition basic_for_examplg virtual processor poklib pok_partition basic_for_examplg Frame gt 1500ms ler gt static gt 500ms 500ms 500ms Allocation gt reference partitionl reference partiti x86_qemu_three_partitions ementation pok_kernel x86_qemu_four_partitions extends pok virtual processor poklib pok_partition basic_for_exampl virtual processor poklib pok partition basic for example virtual processor poklib pok_partition basic_for_examplg virtual processor poklib pok partition basic for exampl Frame 2000ms ler gt static
110. tition code and produce additional output to trace system activity This functionnality pro duces additional files to trace and analze POK behavior with third party tools such as Cheddar10 2 3 4 Automatic and manual configuration The automatic code generation finely configure the kernel and enable only required functionnalities If is especially efficient for embedded systems when you have to avoid useless features and reduce the memory footprint In addition it avoids all po tential errors introduced by the code produced by human developers The automatic configuration process is detailed in chapter 4 2see http forge open do org projects couverture CHAPTER 3 GETTING STARTED 13 On the other hand you can also configure the kernel and the partitions by yourself In this case the configuration will be very difficult since POK has many configuration directives This configuration process is detailed in the next section 3 5 Kernel configuration with ARINC653 XML files You can also configure the kernel with an ARINC653 XML file The tool is available in POK releases in the misc directory More information can be found in section 5 1 3 6 How to write my manual code At this time if you try to write the configuration code by yourself you have to read the configuration directives of POK The fact is that you need to write the configuration code by yourself and make your own build system that supports POK the automatic config
111. tures datain in parameter poklib pointed void countin in parameter poklib integer dataout out parameter poklib pointed void countout out parameter poklib integer properties Source Name gt end blowfish send pok protocols blowfish marshall subprogram implementation blowfish send i end blowfish send i subprogram blowfish receive features datain in parameter poklib pointed void countin in parameter poklib integer dataout out parameter poklib pointed void countout out parameter poklib integer properties Source Name pok protocols blowfish unmarshall end blowfish receive subprogram implementation blowfish receive i end blowfish receive i data blowfish data end blowfish data data implementation blowfish data i properties Type Source Name gt end blowfish data i pok protocols blowfish data t partitign2 reference partition3 CHAPTER 10 ANNEXES 97 149 150 abstract vbus_blowfish_wrapper 151 end vbus_blowfish_wrapper 152 153 abstract implementation vbus blowfish wrapper i 154 subcomponents 155 send subprogram blowfish_send i 156 receive subprogram blowfish_receive i 157 marshalling type data blowfish data i 158 end vbus blowfish wrapper i 159 160 virtual bus blowfish 161 end blowfish 162 163 virtual bus implementation blowfish i 164 properties 165 Implemented_As gt classifier poklib vbus blowfish wrapper 1 166 POK Pr
112. ulien on Mon May 4 12 37 45 2009 package runtime public with POK with layers with types modification sh this file or a y uld art CHAPTER 10 ANNEXES 106 virtual processor partition properties POK Scheduler gt RR POK Additional_Features gt libc_stdio console end partition virtual processor implementation partition i end partition i processor pok kernel properties POK Architecture gt x86 POK BSP gt x86 gemu end pok kernel device separation netif features the bus requires bus access separation bus i outgoing topsecret out data port types integer incoming topsecret in data port types integer outgoing secret out data port types integer incoming secret in data port types integer outgoing unclassified out data port types integer incoming unclassified in data port types integer properties Initialize Entrypoint gt classifier rt18029 init POK Device Name gt rt18029 end separation netif device implementation separation netif i end separation netif i processor implementation pok kernel impl subcomponents runtime secret i virtual processor partition i Provided Virtual Bus Class classifier layers POK Criticality gt 10 i runtime topsecret virtual processor partition i Provided Virtual Bus Class gt classifier layers POK Criticality gt 5 i runtime unclassified virtual processor partition i Provided
113. ur own models When you use this library you don t have to specify all your components and properties just use predefined components to generate your application POK header The following file is a part of the POK project Any modification should be made according to the POK licence You CANNOT use this file or a part of a file for your own project For more information on the POK licence please see our LICENCE FILE Please follow the coding guidelines described in doc CODING_GUIDELINHS gt Copyright c 2007 2009 POK team Created by julien on Wed Oct 14 12 42 24 2009 package poklib public with POK with Data Model processor pok kernel properties POK Scheduler gt static end pok kernel processor implementation pok kernel x86 qemu properties POK Scheduler gt static libe_ String CHAPTER 10 ANNEXES POK Archit POK BSP gt end pok_kerne processor imp properties POK Archit POK BSP gt end pok_kerne processor imp properties POK Archit POK BSP gt end pok_kerne processor imp subcomponents partitionl partition2 properties PORK 2 Major POK Schedu POK Slots PUR Slots end pok_kernel 95 ecture gt x86 x86_qemu x86_qemu ementation pok_kernel ppc_prep ecture gt ppc prep Ppc_prep ementation pok_kernel sparc_leon3 ecture leon3 Sparc leon3 gt sparc ementation pok kernel x86 gemu two parti
114. uration process output code and automatically create the build system for you In that case the best is to start from a working example Try to take the generated code from the examples directory It could be efficient since they are many examples that use various services of the runtime Finally the POK team plans to release a tool that would help the developper in the configuration of the kernel and partitions Such a tool would be graphic like the well known make menuconfig of the Linux kernel and would propose to configure kernel and partitions DIO NP NAND N C Oo aan RU r2 Oo CHAPTER 3 GETTING STARTED 14 3 7 Using Ada for partitions Both C and Ada can be used for partitions Ada will nevertheless require some tuning to run into POK only a GCC toolchain that handles Ada is needed Since POK partitions are loaded by executing their main function one of the Ada packages must export a function as main Moreover the runtime should be disabled using pragma No Run Time The following piece of code is an example of how to proceed main ads pragma No Run Time with Interfaces C package Main is procedure Main pragma Export C Main main end Main main adb package body Main is procedure Printf String in Interfaces C char array pragma Import C Printf printf procedure Main is begin Printf Hello world end Main end Main An ARIN
115. xecution with POK Compilation automatically compile and create binaries 4 2 1 Use the pok toolchain pl script The toolchain is implemented in a script called pok toolchain pl This script is used to perform the different actions of the development process This script has the following options models is a REQUIRED option It specifies the AADL models you use for this system For example you can specify models modell aadl model2 aadl This is the list of your models nogenerate do not generate the code By default the toolchain generates the code from AADL models norun do not run the generated systems By default the toolchain generates code and run generated systems nocheck do not validate the architecture root system name Specify the root system of your architecture If your mod els contain several system components you need to specify what is the AADL root system component arinc653 use ARINC653 code generation patterns CHAPTER 4 AUTOMATIC CONFIGURATION AND CONFIGURATION WITH AADL MODELS18 4 2 2 Example of use The following line will generate ARINC653 compliant code from mode11 aadl model pok toolchain pl models modell aadl arinc653 The following line will generate code and compile it but will not run generated system pok toolchain pl models modell aadl no run 4 3 Model validation Our toolchain automatically validates models requirements before generate code It was made to help system
116. y to create the routing policy in the distributed network You cannot write or read data on from virtual ports only get the port identifier associated with them When you use code generation functionnalities this declaration is automatically created in the deployment c file CHAPTER 5 CONFIGURATION DIRECTIVES 32 Specify ports names When the developer calls ports instanciation he can specify a port name For that reason the kernel must know the name associated with each port This information is provided by the pok ports names declaration It contains the name of each local port There is an example of a such declaration char pok ports names POK CONFIG NB PORTS nodel partition secret outgoing nodel partition topsecret outgoing nodel partition unclassified outgoing When you use code generation functionnalities this declaration is automatically created in the deployment c file Specify port usage for each partition The inter partition ports are dedicated to some partitions Consequently we have to specify in the configuration code which partition is allowed to read write which port We do that with two arrays pok ports nb ports by partitionand pok ports by partition The pok ports nb ports by partition indicates for each partition the number of ports allocated In the same manner the pok ports by partition indicate an array that contains the global ports identifiers allowed for this partition An example is
117. y Allocation include lt types h gt include lt core dependencies h gt ifdef POK NEEDS ALLOCATOR This file contains memory allocation functionnalities You can tweak tune the memory allocator with the following macros POK CONFIG ALLOCATOR NB SPACES the number of memory spaces that can be allocated It can corresponds to the successive is call of malloc or calloc or pok allocator allocate POK CONFIG ALLOCATOR MEMORY SIZE the amount of memory the allocator can allocate s void pok allocator allocate size t needed size This function allocates memory The argument is the amount of memory the user needs This function is called by libc functions malloc and calloc wi void pok allocator free void ptr This function frees memory The argument is a previously allocated memory chunk Be careful the time required to free the memory is indeterministic you should not free memory if your program has strong timing requirements 30 31 32 eune u CHAPTER 8 POK API 48 i endif 8 1 3 Threads include lt core dependencies h gt ifndef POK_THREAD_H define POK_THREAD_H ifdef POK_NEEDS_THREADS include lt types h gt include lt errno h gt include lt core syscall h gt define POK_THREAD_DEFAULT_PRIORITY 42 define POK_DEFAULT_STACK_SIZE 2048 typedef struct uint8_t priority void entry uint6
118. ystem_Time_Type Max_Message_Size Message_Size_Type Port_Direction Port_Direction_Type Last_Msg_Validity Validity Type end record procedure Create Sampling Port Sampling Port Name in Sampling Port Name Type Max Message Size in Message Size Type Port Direction in Port Direction Type Refresh Period in System Time Type Sampling Port Id out Sampling Port Id Type Return Code out Return Code Type procedure Write Sampling Message Sampling Port Id in Sampling Port Id Type Message Addr in Message Addr Type Length in Message Size Type Return Code out Return Code Type procedure Read Sampling Message Sampling Port Id in Sampling Port Id Type Message Addr in Message Addr Type The message address is passed IN although the respective message is passed OUT Length out Message Size Type Validity out Validity Type Return Code out Return Code Type procedure Get Sampling Port Id Sampling Port Name in Sampling Port Name Type Sampling Port Id out Sampling Port Id Type Return Code out Return Code Type procedure Get Sampling Port Status Sampling Port Id in Sampling Port Id Type Sampling Port Status out Sampling Port Status Type Return Code out Return Code Type private type Sampling Port Id Type is new APEX Integer Null Sampling Port Id constant Sampling Port Id Type 0 pragma Convention C Validity Type pragma Convention C Sampling Por

POK User Guide

Contents

Download Pdf Manuals

Related Search

Related Contents