Skip to content

Highly enhanced EwoK version, in full Ada, including more SPARK, cleaner and faster code

Latest
Compare
Choose a tag to compare
@PThierry PThierry released this 29 Aug 08:53
· 102 commits to master since this release

(HEAD -> master, tag: v0.9.9, m/master, github/master) [update] add production defconfig autotest to travis
[bugfix] support for clean reboot/wipe on panic. Allows task fault on userspace exception
[bugfix] add missing unmap flag set. typo for harden (not freezing) modes
[enhancement] More proofs
[enhancement] Proving some parts of the kernel with gnatprove
Removed file added by mistake
[enhancement] using a generic memory interface - Replacing ewok.mpu invocations by the more generic ewok.memory package
[enhancement] Inlining some subprograms for slightly improving performances
Removing get_current procedure
Completed fault handler with extra informations
Removing ewok.sched.get_current procedure (not useful)
SoftIRQ: simplifying isr_queue entries
[enhancement] More portable code
[bugfix] Protecting some critical resources
Adding SCB register
Indenting
[bugfix] add missing RCC activation for kernel serial
(pthierry/master) [bugfix] comment typo
[bugfix] corrected device addr check for pure IO devices
[update] support for configurable reentrancy support (kernel experimental mode)
[enhancement] add support for rentrancy in EwoK handler mode
[bugfix] updated travis cross-refs check
[performance] MPU update only when it's needed * MPU update is performed only when: - a task switch occurs - task's mode is changing
[design] Removing syscall management from SoftIRQ * Every syscalls are managed synchronously * SoftIRQ is simplified and manage only ISRs
[enhancement] Removing privileges from the SoftIRQ kernel task * MPU imposes some new constraints that forbid access to user tasks' memory space
[bugfix] add missing export
[enhancement] initial implementation of cross-project PR dependencies markup
[bugfix] corrected device size check for pure IO devices (e.g. LED or buttons)
[bugfix] deactivate USART RX for kernel console
[enhancement] MPU layer is abstracted - Kernel modules (tasks, sched...) do not need to "understand" how the MPU work anymore. The invocated methods are more simple. - The benefit is that it lead to a better decoupling packages and to an increase simplification - The major drawback is currently a performance penalty (about 3%). The explanation is that previous implementation use lot of hardcoded value.
Removed doxygen tags
Do some cleaning - Reformating some comments - Reformating some 'with' clauses - Lightening ewok.sleep package
[bugfix] Resolved Ada circular elaboration problems - 2019 GNAT compiler was ok but 2018 version didn't managed correctly dependencies - Root cause was that ewok.ads top package had a related body
Adding default values to records * Cleaning task and device initialization * Adding some default values to avoid unitilized values that lead to undefined behaviors
[enhancement] Misc. * Cleaning tools (removing unused variables) * Fixing some missing preprocessing directives: FISR and FIPC
[enhancement] cleaning build process, reducing makefiles to single one, using gprbuild instead
[enhancement] Removed the last remaing C file and cleaning startup.s
[enhancement] Cleaning * Removed unused files * Simplifications
[enhancement] Moved Ada entry point from ewok.init.main to ewok.main
[enhancement] Cleaning MPU management
[update] Removed useless code * RNG interface for C code is not used anymore * Directives KERNEL_ENABLE_DMA are removed where not usefull * Added KERNEL_ENABLE_DMA directives in src/ewok-syscalls-handler.adb to return DENIED when doing a related DMA syscall when it's not available
[enhancement] Cleaner serial management by the kernel for debugging purpose
[enhancement] Cleaner serial management by the kernel for debugging purpose
[bugfix] Remove unicode character unsupported by latex
[bugfix] Remove unicode character unsupported by latex
[update] EwoK description
[update] Cleaning, fixing minor things...
[bugfix] Removed useless file.
[bugfix] Minor. Fixed mkdir directive.
[enhancement] Removed unused code and added some few comments
Merge pull request #15 from PThierry/only_ada
[bugfix] add placeholder for generated root dir
[bugfix] add missing files during directory move
(pthierry/only_ada) [bugfix] create dir if it does not exists before generating header
[bugfix] add missing config.def links
add placeolder for generated dir
[update] removed Ada subdir of SoC and core dirs, as Ada is the single kernel language
moved src/Ada to src
Merge pull request #16 from arnauldm/master
[bugfix] Fixed some few errors in libgnat GPR build file * -O2 must be in Compiler package * Removed some redundant directives
[update] Removed unused files
Merge pull request #14 from arnauldm/ami/cleaning
[bugfix] Minor update in Makefile
[enhancement] Removed unused code * Stack protection (SSP) is no more useful for hardening the kernel, as its fully implemented in Ada * FPU is not used
(types, portable_types) Merge pull request #13 from PThierry/exit_handling
(pthierry/exit_handling, exit_handling) [update] add sys_exit initial documentation
[update] move exit handling to dedicated syscall
[bugfix] Updated broken URL in README.md
[bugfix] Fixed markdown formatting
[updated] Documentation
Merge pull request #12 from arnauldm/ami/master
[enhancement] Removed useless code
Merge pull request #11 from arnauldm/ami/c_to_ada
[bugfix] Updated soc-rcc.adb for disco407 board
[enhancement] soc-rng in Ada
[enhancement] SOC initialization in Ada
Merge pull request #10 from arnauldm/ami/adaification
[enhancement] Migrated C code to Ada * last_chance_handle in Ada * init.c do nothing more than calling ewok.init.main procedure * debug.c and debug.h are removed * removed some unused files
Merge pull request #9 from arnauldm/ami/sparkification
Merge pull request #7 from PThierry/prove_spark2019
[enhancement] Code simplification
[update] removing useless local access type after rebasing master
[update] add clean prove target inside kernel dir
[update] replacing global access type in tasks interface with local types
[bugfix] keeping t_task_access as rw pointer by now. the task accessor should be updated later on to support SPARK proof
[update] passing local task's IPC endpoint list from pointer array to id array
[enhancement] starting SPARK'19 integration, with pointers support
Merge pull request #8 from arnauldm/ami/usart
(refs/pull/8/head) [bugfix] Minor fixes for stm32f407 architecture
[bugfix] Missing symbolic links for stm32f407 and stm32f429 architectures
[bugfix] Updated Makefile.objs
[update] Replaced usart and debugging C code with Ada code * Added support to RCC with soc.rcc and soc.rcc.default Ada packages * Added (incomplete but functionnal) support to USART with soc.usart Ada package * Put debugging serial initialization in ewok.debug Ada package
Merge pull request #6 from PThierry/prove
(pthierry/prove) [bugfix] add missing new dir to prove target GPR file
Merge pull request #5 from arnauldm/ami/c_to_ada
[bugfix] BSP files adapted for stm32f407 board * Created stm32f407/Ada/generated * Adapted stm32f407/Ada/soc-rcc.adb to fulfill soc devices constraints
Merge pull request #4 from arnauldm/ami/syscalls
(refs/pull/5/head) [update] Replaced devmap C code with Ada code
[update] Big update in order to get rid of C code * Replaced devmap C code with Ada code /!\ Not working /!
(refs/pull/4/head) [update] Cleaning syscalls * Replacing SVC_TASK_DONE and SVC_ISR_DONE by SVC_EXIT * Renaming some syscalls so their name is more self-explanatory
[bugfix] Added missing checks in syscalls SVC_TASK_DONE and SVC_ISR_DONE
[update] SVC handler simplified
[update] Modified syscalls mechanism
Merge pull request #3 from PThierry/kernel_full_ada
(pthierry/kernel_full_ada) [enhancement] passing to full Ada kernel; removing the unused C code from the Ada version of EwoK