Commit graph

2980 commits

Author SHA1 Message Date
Tobias Reinhard
8ca47345d4 Added script to rewrite preprocessed source file into a format VeriFast understands. 2022-10-14 16:19:50 -04:00
Tobias Reinhard
95440b41be Added preprocessing log directory to .gitignore. 2022-10-14 15:25:17 -04:00
Tobias Reinhard
cf9b1e9aae Preprocessing script replaces comments out line/file pragmas. 2022-10-14 15:22:57 -04:00
Tobias Reinhard
24130f5334 Added VF startup script for preprocessed tasks.c.
The script preprocesses task.c according to the RP2040 configuration and launches verifast.
2022-10-14 13:37:30 -04:00
Tobias Reinhard
7d029778bf Added scripts to build kernel and to preprocess tasks.c.
The scripts use the demo configuration for RP2040.
2022-10-14 13:23:37 -04:00
Tobias Reinhard
d7fff36a2b Update SMP demo submodule. 2022-10-14 13:10:53 -04:00
Tobias Reinhard
ee70a7815d Resolved VF parse error. Deleted functions involving inline assembler. 2022-10-13 12:52:57 -04:00
Tobias Reinhard
997d39d894 Added temporary work-around for VF's define_name bug.
For bug description, see minimal example `define_name`.
2022-10-13 12:40:50 -04:00
Tobias Reinhard
8aa7af3fd5 Resolved VF parser error: VF does not support attribute used. 2022-10-13 12:36:18 -04:00
Tobias Reinhard
6129726501 Resolved VF preprocessor error.
VF's preprocessor cannot handle context-sensitive macro expansion.
2022-10-13 12:21:36 -04:00
Tobias Reinhard
50c5b21a59 Resolved VF preprocessor error.
VF's preprocessor cannot handle expansion of `PRIVILEGED_FUNCTION` macro because the normal and the context-free preprocessor consume different numbers of tokens. We resolved this temporarily by deleting the macro.
2022-10-13 11:34:24 -04:00
Tobias Reinhard
a1a16c7dba Dumped new version of pico sdk submodule. 2022-10-13 10:02:31 -04:00
Tobias Reinhard
f7316a77f0 Added temporary work-around for VF's define_name bug.
For bug description, see minimal example `define_name`.
2022-10-13 10:01:34 -04:00
Tobias Reinhard
4431a1f5d6 Resolved VF parse error: VF does not support local static variables.
Removed problematic function definition for now.
2022-10-13 09:52:20 -04:00
Tobias Reinhard
21f9a95a10 Fixed proof setup include path
The include path contained some directories within the SMP demos FreeRTOS source tree (which is the official unaltered FreeRTOS repo). Updated the include path such that it points to our forked version of the FreeRTOS kernel repo.
2022-10-13 09:48:11 -04:00
Tobias Reinhard
c71025fda0 Added minimal example for VF bug involving testing for macro defines in headers. 2022-10-13 09:16:54 -04:00
Tobias Reinhard
8ef03612b5 Update pico sdk submodule to resolve VF parse errors. 2022-10-12 11:07:19 -04:00
Tobias Reinhard
497a23d2eb Renamed VERIFAST_PROOF define into VERIFAST. 2022-10-11 15:32:57 -04:00
Tobias Reinhard
7f69232893 Resolved VF parse error in pico sdk's platform.h and deleted stub. 2022-10-11 15:26:00 -04:00
Tobias Reinhard
e652475628 vf start script now now uses pico sdk submodule for includes instead of system-wider pico sdk installation. 2022-10-11 15:14:03 -04:00
Tobias Reinhard
21457b6611 Added missing include flag in vf start script. 2022-10-11 15:10:20 -04:00
Tobias Reinhard
80651ca320 Switched submodules to verifast branch. 2022-10-11 14:50:43 -04:00
Tobias Reinhard
eec276d0a3 Replaced Pico SDK submodule by fork. 2022-10-11 14:39:57 -04:00
Tobias Reinhard
5995eb2ac4 Added Pico SDK repo as submodule. 2022-10-11 14:34:41 -04:00
Tobias Reinhard
bcde498313 Added FreeRTOS-SMP-Demos repo as submodule. 2022-10-11 14:32:14 -04:00
Tobias Reinhard
0c3f65d8ad Setup environment for VeriFast proof and start script for vfide. 2022-10-11 12:20:41 -04:00
Tobias Reinhard
143e76755e Added FreeRTOS-SMP-Demos repo as submodule. 2022-10-11 11:54:32 -04:00
Tobias Reinhard
b3af566a7d Added .DS_Store files to .gitignore. 2022-10-11 11:54:15 -04:00
Graham Sanderson
13f034eb74
RP2040: Fix compiler warning and comment (#509)
Co-authored-by: graham sanderson <graham.sanderson@raspeberryi.com>
2022-06-24 17:23:51 +05:30
Gaurav-Aggarwal-AWS
b3918c7f38
Remove ThirdParty from core checker in smp branch (#512)
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
2022-06-24 17:22:15 +05:30
graham sanderson
b87dfa3e97 RP2040: Allow FreeRTOS to be added to the parent CMake project post initialization of the Pico SDK 2022-06-23 11:32:40 -07:00
Sudeep Mohanty
2eff037080
Update prvYieldCore() compile warning for single core targets (#505)
When configNUM_CORES is 1, prvYieldCore() generates an array subscript
outofbound error (-Warray-bounds) when compiled with GCC with space
optimization enabled (-Os).

This commit updates the code flow in prvYieldCore() to compile out
the part where yield is needed on the other core which is unnecessary
for single-core targets.
2022-06-22 10:03:44 +05:30
Graham Sanderson
45dd83a8e3
Fix RP2040 assertion due to yield spin lock info being wrongly shared between multiple cores (#501)
Co-authored-by: graham sanderson <graham.sanderson@raspeberryi.com>
2022-06-09 10:59:35 -07:00
Darian
34b8e24d7c
Add support for newlib dynamic reentrancy (#496)
Previously, newlib's _impure_ptr was updated on every context switch
to point to the current task's _reent structure.

However, this behavior is no longer valid on multi-core systems due
to the fact that multiple cores can switch contexts at the same time,
thus leading to the corruption of the _impure_ptr.

However, Newlib can be compiled with __DYNAMIC_REENT__ enabled which
will cause newlib functions to call __getreent() instead in order to
obtain the required reent struct.

This commit adds dynamic reentrancy support to FreeRTOS:

- Added a configNEWLIB_REENTRANT_IS_DYNAMIC to enable dynamic reentrancy support
- _impure_ptr is no longer updated with reentrancy is dynamic
- Port must provide their own __getreent() that returns the current task's reent struct
2022-05-31 16:11:02 -07:00
Darian
a97741a08d
Add task creation with affinity functions (#470)
This commit adds the functions listed below. These functions allow
tasks to be created with their core affinity already set.

- xTaskCreateAffinitySet()
- xTaskCreateStaticAffinitySet()
- xTaskCreateRestrictedAffinitySet()
- xTaskCreateRestrictedStaticAffinitySet()
2022-03-18 10:16:21 -07:00
Darian
4446c8f0ea
Fix pxPreviousTCB compile warning (#464)
When compiling with configNUM_CORES == 1 and configUSE_CORE_AFFINITY == 1,
pxPreviousTCB will generate a "set but unused" warning.
2022-03-06 14:21:39 -08:00
Timo Sandmann
4832377117
smp branch: bugfix for race condition on RP2040 (#431)
* Bugfix for race condition on RP2040 in vPortEnableInterrupts()

RP2040 SMP port: Since spin_unlock() re-enables interrupts, pxYieldSpinLock has to be updated first to avoid a possible race condition.

* Bugfix for invalid sanity checks on RP2040

RP2040 SMP port: Testing pxYieldSpinLock for NULL does not work reliable in these places, because another/new lock might already be set when configASSERT() is executed.
2021-12-28 12:30:03 -08:00
Graham Sanderson
7d11089624
Rp2040 fixes smp (#425)
* RP2040: malloc needs to be thread safe for FreeRTOS whether both cores are used or not

* RP2040: CMake file had broken left over test code
2021-12-17 15:06:35 -08:00
Gaurav-Aggarwal-AWS
2b0fdf2a71
Add SMP in the License Header (#402)
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
2021-10-13 18:38:24 -07:00
Gaurav-Aggarwal-AWS
970b678a0b
SMP version (#401)
* Update version number for SMP

Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
2021-10-13 18:23:03 -07:00
Gaurav-Aggarwal-AWS
7ce8266bc5
Update SMP docs (#400)
This commit adds the docs for newly added SMP APIs.

Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
2021-10-10 23:16:16 -07:00
N3xed
fa6982c99a
Update xSTATIC_TCB layout in line with tskTCB (#375) 2021-08-09 15:14:10 -07:00
N3xed
a2c8db1089
Move uxCoreAffinityMask after xMPUSettings (#372)
Allows for much easier assembly access to the field.
2021-07-29 23:58:47 -07:00
Graham Sanderson
35b95d2a4d
Rp2040 smp (#342)
* Add RP2040 support (#341)

* Add RP2040 support

* remove spurious tab/spaces comments

* add .cmake to ignored kernel checks

* Apply suggestions from code review

Co-authored-by: Paul Bartell <paul.bartell@gmail.com>

* license and end of file newline fixes

* Rename LICENSE.TXT to LICENSE.md

Co-authored-by: Paul Bartell <paul.bartell@gmail.com>
Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>

* RP2040 updates for SMP

* whitepsace fix

Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>

* whitespace fix

Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>

Co-authored-by: Paul Bartell <paul.bartell@gmail.com>
Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
2021-07-06 10:53:49 -07:00
Michael Bruno
a7092d400c
Fix XCore DP/CP register corruption bug (#352)
The kernel code that runs within RTOS ISRs requires that DP and CP not
be changed from their initial values. If a task changes them and is
interrupted while they are changed, then they must be restored for the
ISR. This commit implements this.

This relies on a corresponding change to the xcore lib_rtos_support.
2021-06-28 08:44:24 -07:00
Michael Bruno
a9754a8fdd
Change XCC to xClang for XCore ports (#332) 2021-05-21 14:59:03 -07:00
Joseph Julicher
3231d08be4
fixed CI repo branch (#330) 2021-05-19 17:01:54 -07:00
Joseph Julicher
b515641e0a
adding a minimal idle hook to the SMP port (#329)
* adjusting the kernel checks repo

* Added a minimal idle hook for all idle tasks
2021-05-19 16:19:57 -07:00
Joseph Julicher
0c1381311b
Merge branch 'smp' into smp 2021-05-19 10:10:36 -07:00
Joseph Julicher
d58750f5f9 Updated from upstream 2021-05-19 10:02:49 -07:00